Minimal and Complete Prefix Unification for NonClassical Theorem
Proving.


Jens Otten, Christoph Kreitz.  
Technical Report, TU Darmstadt, 1997. 

Abstract 

For theorem proving in nonclassical logics two similar approaches
have been established: a matrix characterization of Wallen and
Ohlbach's resolution calculus. In both cases the essential
extension of the classical calculi is a need for unifying the
socalled prefixes of atomic formulae or socalled worldpaths
respectively.
We present a specialized stringunification algorithm which computes a minimal set of most general unifiers. By transforming systems of equations we obtain an elegant and efficient procedure which applies to intuitionistic logic and the modal logic S4. With some modifications it also applies to the modal logics D, K, D4, K4, S5, and T. We explain our method by an intuitive graphical illustration, prove termination, correctness, completeness, and minimality, and investigate its complexity. 
Back to overview of papers 

Bibtex Entry 

@TechReport{tr:OttenKreitz97a, author = "Jens Otten and Christoph Kreitz", title = "Minimal and Complete Prefix Unification for NonClassical Theorem Proving", institution = "FG Intellektik, TU Darmstadt" year = "1997" } 