Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 5 / Issue 3

available in:   PDF (436 kB) PS (171 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-005-03-0088


Connection-Based Theorem Proving in Classical and Non-Classical Logics

Christoph Kreitz (Department of Computer Science, Cornell-University, USA)

Jens Otten (FG Intellektik, FB Informatik, Darmstadt University of Technology, Germany)

Abstract: We present a uniform procedure for proof search in classical logic, intuitionistic logic, various modal logics, and fragments of linear logic. It is based on matrix characterizations of validity in these logics and extends Bibel's connection method, originally developed for classical logic, accordingly. Besides combining a variety of different logics it can also be used to guide the development of proofs in interactive proof assistants and shows how to integrate automated and interactive theorem proving.