Intellectics Group: Technical Report 99-05
Connection-based Theorem Proving in Classical and Non-classical Logics.
Christoph Kreitz and Jens Otten
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.