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

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. 1 Introduction Classical and non-classical logics are used extensively in various branches of Artificial Intelligence and Computer Science as logics of knowledge and belief, logics of programs, logics of action and change, and for the specification of distributed and concurrent systems. In many of these applications there is a need for deductive systems that can simulate mathematical reasoning. Proof assistants like NuPRL [11], Coq [12], Alf [2], Isabelle [37] were developed to supp...