# 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.