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 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" }