A Uniform Proof Procedure for Classical and Non-classical Logics

Abstract. We present a proof procedure for classical and non-classical logics. The proof search is based on the matrix-characterization of validity where an emphasis on paths and connections avoids redundancies occurring in sequent or tableaux calculi. Our uniform path-checking algorithm operates on arbitrary (non-normal form) formulae and generalizes Bibel’s connection method for classical logic and formulae in clause-form. It can be applied to intuitionistic and modal logics by modifying the component for testing complementarity of connected atoms. Besides a short and elegant path-checking procedure we present a specialized string-unification algorithm which is necessary for dealing with non-classical logics.