T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods.
Jens Otten, Christoph Kreitz.
In P. Miglioli, U. Moscato, D. Mundici, M. Ornaghi, eds., 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'96), LNAI 1071, pp. 244-260, Springer Verlag, 1996.
Abstract
	For an efficient proof search in non-classical logics, particular in intuitionistic and modal logics, two similar approaches have been established: Wallen's matrix characterization and Ohlbach's resolution calculus. Beside the usual term-unification both methods require a specialized string-unification to unify the so-called prefixes of atomic formulae (in Wallen's notation) or world-paths (in Ohlbach's notation). For this purpose we present an efficient algorithm, called T-String-Unification, which computes a minimal set of most general unifiers. By transforming systems of equations we obtain an elegant unification procedure, which is applicable to the intuitionistic logic J and the modal logic S4. With some modifications we are able to treat the modal logics D, K, D4, K4, S5, and T. We explain our method by an intuitive graphical presentation, prove correctness, completeness, minimality, and termination and investigate its complexity.

		Paper is available in postscript and pdf format		Slides of the conference presentation are available in compressed postscript and pdf format (Presentation: Jens Otten)
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:OttenKreitz96a, author = "Jens Otten and Christoph Kreitz", title = "T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods", booktitle = "5$^{th}$ Workshop on Theorem Proving with Analytic Tableaux and Related Methods", year = 1996, editor = "U. Moscato", volume = "1071", series = "Lecture Notes in Artificial Intelligence", pages = "244--260", publisher = "Springer Verlag" }