A Uniform Proof Procedure for Classical and Non-classical Logics.

Jens Otten, Christoph Kreitz.

In G. Görz & S. Hölldobler, eds., KI-96: Advances in Artificial Intelligence,
LNAI 1137, pp. 307-319, Springer Verlag, 1996.


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.


Paper is available in
postscript and pdf format
  Slides of the conference presentation are available in compressed postscript and pdf format




Bibtex Entry


BACK
Back to overview of papers
@InProceedings{inp:OttenKreitz96b, author = "Jens Otten and Christoph Kreitz", title = "A Uniform Proof Procedure for Classical and Non-classical Logics", booktitle = "KI-96: Advances in Artificial Intelligence", year = 1996, editor = "G. G{\"o}rz and S. H{\"o}lldobler", volume = 1137, series = "Lecture Notes in Artificial Intelligence", pages = "307--319", publisher = "Springer Verlag" }