TStringUnification: Unifying Prefixes in NonClassical 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. 244260, Springer Verlag, 1996. 

Abstract 

For an efficient proof search in nonclassical 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 termunification both methods
require a specialized stringunification to unify the socalled
prefixes of atomic formulae (in Wallen's notation) or worldpaths
(in Ohlbach's notation). For this purpose we present an efficient
algorithm, called TStringUnification, 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 = "TStringUnification: Unifying Prefixes in NonClassical 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 = "244260", publisher = "Springer Verlag" } 