JUCS - Journal of Universal Computer Science 5(3): 88-112, doi: 10.3217/jucs-005-03-0088
Connection-Based Theorem Proving in Classical and Non-Classical Logics
expand article infoChristoph Kreitz‡, Jens Otten§
‡ Department of Computer Science, Cornell-University, Ithaca, NY, United States of America§ FG Intellektik, FB Informatik, Darmstadt University of Technology, Darmstadt, Germany

Corresponding author: Christoph Kreitz ( kreitz@cs.cornell.edu )

© Christoph Kreitz, Jens Otten.
This article is freely available under the J.UCS Open Content License.
Citation: Kreitz C, Otten J (1999) Connection-Based Theorem Proving in Classical and Non-Classical Logics. JUCS - Journal of Universal Computer Science 5(3): 88-112. https://doi.org/10.3217/jucs-005-03-0088
Open Access
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.