Previous: AIDA-96-01 Next: AIDA-96-03 Index 1996


Intellectics Group: Technical Report 96-02

A Uniform Proof Procedure for Classical and Non-classical Logics

Jens Otten and Christoph Kreitz

We present an efficient proof procedure for classical and non-classical logics. The proof search is based on the matrix-characterization of validity where the emphasis on paths and connections avoids redundancies occurring in sequent or tableaux calculi. Our uniform technique of path-checking is applicable to arbitrary formulae and a generalization of Bibel's connection method for classical logic and formulae in clause-form. This makes it suitable for intuitionistic logic and modal logics by simply modifying a component testing complementarity of two connected atoms. Since we avoid increasing the length of formulae by transforming them to any normal form, we reduce the search space even in comparison to the classical case. Besides a short and elegant algorithm for path-checking we present details of a specialized string-unification algorithm which is necessary for dealing with the non-classical logics under consideration.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry