Intellektik: Technical report 95-09

T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods

Jens Otten and Christoph Kreitz

For an efficient proof search in non-classical logics, particu lar 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 $\cal J$ and the modal logic S4. With some modifications we are also 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.