In P. Miglioli, U. Moscato et. al., ed., Proc. 5^{th} Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 1071, pp. 244–260, Springer Verlag, 1996.

T-String-Unification:

Unifying Prefixes in Non-Classical Proof Methods

Jens Otten^{⋆} Christoph Kreitz

Fachgebiet Intellektik, Fachbereich Informatik Technische Hochschule Darmstadt Alexanderstr. 10, 64283 Darmstadt, Germany

          {jeotten,kreitz}@intellektik.informatik.th-darmstadt.de

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.

1 Introduction

Unification is one of the key operations which are used to guide an efficient search for a proof of a theorem in classical predicate logic. Within theorem provers based on the connection method [5, 6, 8, 4], resolution [17, 20], the tableaux calculus [3, 2], and others unification is required for making certain atomic formulae complementary. Complementarity is a key concept in the characterization of logical validity. In classical logic two atomic formulae (or atoms) are called complementary if they have the same predicate symbol but different polarities (or signs) and if their sub-terms can be made identical by some (first-order- or quantifier-) substitution. This substitution encodes the fact that certain quantified variables occurring in the formula to be proven have to be instantiated by terms in order to complete the proof. It can be computed by well-known algorithms for term-unification such as the algorithm of Herbrand & Robinson [7, 17] or Martelli-Montanari [11].

If proof methods like the above shall be extended to non-classical logics such as modal logics or intuitionistic logic it is not sufficient to consider only the terms occurring in atomic formulae. In his matrix characterization of non-classical validity Wallen [19] has shown that in addition the prefixes of atomic formulae need to be unified in order to make them complementary where a prefix of an atom essentially describes its position in the formula tree. Similarly Ohlbach’s resolution calculi for modal logics [12, 13] require a unification of world-paths which characterize the modal context of an atom in a formula. Both conditions are nearly identical^{2} and

⋆ Supported by the Adolf Messer Stiftung 2 In the rest of this paper we shall follow the Wallen’s terminology and notation.

express the peculiarities and restrictions of these logics. In addition to the usual term unification, therefore, proof procedures for non-classical logics will have to incorporate a prefix unification algorithm.

Formally, a prefix of an atomic formula is a string over some alphabet A consisting of variables and constants. Two prefix strings s and t can be unified if there is a morphism σ which assigns a string to each variable such that σ(s)=σ(t). In contrast to the usual term substitution Wallen [19] calls this morphism σ a modal or intuitionistic substitution.

Consider, for instance, the strings tabUlAR and taST eF uL where capital letters indicate variables and small letters refer to constants. These two strings can be unified by applying the substitution^{3} σ = {U\ε, A\ea, R\ux, S\b, T \l, F \a, L\x} which yields the string tableaux in both cases.

In general, unification with respect to some equational theory E can be considered as the following problem: given a set of equations Γ = {s_{1}=t_{1}, …, s_{n}=t_{n}} one has to find a substitution σ which solves all these equations w.r.t. the theory E, i.e. σ(s_{i}) =_{E} σ(t_{i}) must hold for all i. The substitution σ is called a unifier of Γ. It is a most general unifier,shortly σ^{∈} mgu(Γ), if it is not an instance of some other unifier τ of Γ.

The theory E itself is defined by some set of axioms which have to hold in addition to the usual laws of reflexivity, symmetry, and transitivity. In the case of string unification (the monoid problem or resolution problem for word equations) the only axiom is the associativity of string concatenation. An algorithm for enumerating the most general unifiers of a set of string equations has first been presented by Plotkin [16] whereas Makanin [9, 10, 1] showed that it is possible to decide whether a set of string equations has a unifier or not. In general, however, the number of most general unifiers of a set of string equations is infinite. For Γ = {aX=Xa}, for instance, the set of most general unifiers is {σ | σ(X) = a^{i}, i^{∈} IN_{0}}.

Fortunately, there are certain restrictions on the prefixes of atomic formulae which drastically simplify the unification problem for prefix strings. Prefixes are strings without duplicates and in two prefixes (corresponding to atoms of the same formula) equal characters can occur only within a common substring at the beginning of the two prefixes. These requirements, which we shall call T-string property, will allow us to write a much more efficient algorithm for unifying prefix strings. Since two prefixes contain no common variables (except for some identical substring at their beginning) one only has to unify the variables occurring in one string with substrings of the second and vice versa. The number of most general unifiers will become finite, although it may still grow exponentially with the length of the prefixes.

During T-string unification it may become necessary to consider additional variables. The strings aX and Y b, for instance, can be unified by σ_{1} = {Y \a, X\b} but also by σ_{2} = {Y \ac, X\cb}, σ_{3} = {Y \acd, X\cdb}, σ_{4} = {Y \acde, X\cdeb}, etc. None of these substitutions can be considered most general since they are all instances of σ = {Y \aZ, X\Zb} where Z is a new variable. This fact is illustrated by the following diagram and has to be taken into account when developing an algorithm for T-string unification.

3 As usual we denote a substitution σ by the set {x\t | σ(x)=t ∧ x≠t}.

^{Z}

\begin{aligned}a & & X \\ & Y & & b \end{aligned}

_{Z}

The unification algorithm which we shall present in this paper computes for any set of equations Γ = {s_{1}=t_{1}, …, s_{n}=t_{n}} (where all possible pairs of strings satisfy the T-string property) a minimal set of most general unifiers. The algorithm proceeds by transforming a set of equations in a way similar to the algorithm of Martelli & Montanari [11] for term-unification. For this purpose it uses transformation rules which step-wisely convert the set of equations into a set of substitutions which eventually will become the set of most general unifiers. This makes it possible to give an elegant description of our procedure and to adopt it to different modal logics by simple modifications of its transformation rules.

In the following section we shall briefly introduce all the mathematical preliminaries of T-string unification. Section 3 describes a general unification algorithm which can be used in proof procedures for intuitionistic logic and the modal logic S4. We shall present its transformation rules and investigate its computational complexity. In section 4 we shall then study T-string unification for various other modal logics. We conclude with a brief comparison with other approaches and a few remarks on applications and further investigations.

2 Preliminaries

In this section we shall briefly describe the basic concepts which are necessary for describing and investigating our T-string unification procedure.

Definition 1 (Strings). Let V be a set of variables and C a set of constants (with V ∩ C = ∅). A string is a word over the alphabet A = V ∪ C. The empty string is denoted by ε. The set of strings over the alphabet A is denoted by A^{∗}. The length of a string s is denoted by |s|. For a string s the character at position i is denoted by s_{i}. The concatenation of the strings s and t is denoted by s ∘ t (or briefly st).

Example 1. Let V = {A, B, C, …, Z} and C = {a, b, c, …, z}. Then tabUlAR and taST eF uL are strings over V ∪ C.

The strings we intend to unify shall be used to represent the positions of atomic formulae within a formula tree. As such they satisfy certain restrictions which we call the T-string property (i.e. ‘formula tree string’-property). Two strings s and t have the T-string property, iff

1. no character is repeated either in s nor in t, and

2. equal characters occur only at the beginning of s and t. A set of strings S has the T-string property iff each pair of strings in S has the T-string property.

Definition 2 (T-string property). Let s and t be two strings over an alphabet A. s and t have the T-string property iff

1. ∀_{1≤i,j≤|s|}: i ≠ j ⇒ s_{i} ≠ s_{j} and ∀_{1≤i,j≤|t|}: i ≠ j ⇒ t_{i} ≠ t_{j}, and

2. ∃_{0≤j≤min(|s|,|t|)} : (∀_{1≤i≤j}:s_{i}=t_{i} and ∀_{i_{1},i_{2}}:(j<i_{1}≤|s| and j<i_{2}≤|t|) ⇒ s_{i_{1}}≠t_{i_{2}}).

Let S = {s_{1}, …, s_{m}} (m ≥ 2) be a set of strings. S has the T-string property iff ∀_{1≤i,j≤m} : s_{i} and s_{j} have the T-string property. We call the strings in S T-strings.

Remark. The prefixes in Wallen’s matrix characterization have exactly these attributes, since they are defined as branches in a formula tree.

Example 2. The strings tabUlAR and taST eF uL have the T-string property.

Definition 3 (Substitution). A substitution σ : V → (V ∪C)^{∗} is a mapping from the set of variables to the set of strings over V ∪ C, which is almost everywhere (i.e. except for finitely many elements) the identity mapping. A substitution σ can be represented by a set of variable string pairs, i.e. by {x\s | σ(x)=s and x≠s}. The application σ(t) of a substitution σ to a string t leads to the string t′ where the variables in t are replaced by their values under σ.

Example 3. Let V and C defined as above. Then σ = {U\ε, A\ea, R\Ux} is a substitution. Its application to the string tabUlAR yields σ(tabUlAR) = tableaUx.

Definition 4 (Composition). The composition τ(σ) of two substitutions σ and τ is the combination of the corresponding functions, i.e. this yields the substitution {x\τ(t) | x\t^{∈} σ and x≠τ(t)} ∪ {x\s | x\s^{∈} τ and not x\t^{∈} σ for some t}. A substitution σ is called idempotent if σ(σ) = σ.

Example 4. Let σ = {U\ε, A\ea, R\Ux} and τ = {U\v, A\b, C\De}. The composition ρ = τ(σ) results in ρ = {U\ε, A\ea, R\vx, C\De}. The substitution τ is idempotent but σ is not since σ(σ) = {U\ε, A\ea, R\x}

Remark. From now on we shall always deal with idempotent substitutions.

Definition 5 (Instance). A substitution ρ is called an instance of a substitution σ (or σ is more general than ρ), iff there is substitution τ with ρ = τ(σ).^{4}

Example 5. In example 4 the substitution ρ is an instance of σ, since ρ = τ(σ).

With the above notions we can now define unifiers and most general unifiers. Our definitions correspond to concepts introduced e.g. in [19, 12, 18].

Definition 6 (T-Unifier). Let Γ = {s_{i}=t_{i} | i = 1, …, n} be a system of equations for T-strings such that the set S = {s_{i} | i = 1, …, n} ∪ {t_{i} | i = 1, …, n} has the T-string property. A substitution σ T-unifies Γ iff for every equation s_{i}=t_{i} in Γ we have σ(s_{i})=σ(t_{i}). σ is called a T-unifier for Γ.

Example 6. σ = {U\ε, A\ea, R\ux, S\b, T \l, F \a, L\x} is a T-unifier for the set Γ = {tabUlAR=taST eF uL} since σ(tabUlAR) = σ(taST eF uL) = tableaux.

Definition 7 (Most General T-Unifiers). Let Γ = {s_{i}=t_{i} | i = 1, .., n} be a system of equations of T-strings. A set Σ of substitutions is called a (minimal) set of most general T-unifiers for Γ, denoted mgu(Γ), if the following properties hold:

4 Note that every substitution σ is an instance of itself, since σ = τ(σ) for τ = ∅.

1. Every substitution σ^{∈} Σ is a T-unifier for Γ. (Correctness)

2. Every T-unifier τ for Γ is an instance of some σ^{∈} Σ. (Completeness)

3. No σ^{∈} Σ is an instance of another substitution σ′ ^{∈} Σ. (Minimality) An element of mgu(Γ) is called a most general T-unifier for Γ.

3 T-String-Unification for Intuitionistic Logic

In this section we present a general method for computing the set of most general T-unifiers. It can be used to unify prefixes in proof methods for the intuitionistic logic J or the modal logic S4 (see [19, 14]).^{5} The method is general in the sense that there are no restrictions for the computed unifier: variables may be instantiated by arbitrary strings including the empty string.^{6}

After examining the decidability of T-string-unification we shall give an intuitive graphical explanation of a method for computing T-unifiers. We shall then present a formal description of our technique which operates by transforming systems of equations according to given transformation rules. We proof correctness, completeness, minimality, and termination of our unification procedure, investigate its complexity and finally present an implementation of the algorithm.

3.1 Decidability

For two T-strings s and t, i.e. for the equation system {s=t}, there is a simple way for deciding whether there exists a T-unifier or not.

Lemma 8 (Decidability). Let s′ and t′ be two strings over the alphabet V ∪ C which have the T-string property. Furthermore let u be the common string at the beginning of s and t, i.e. s′=us and t′=ut. There is a T-unifier for the equation {s′=t′} if and only if

1. s = ε and t = ε, or

2. s_{1} ^{∈} V and t_{|t|} ^{∈} V, or

3. s_{|s|} ^{∈} V and t_{1} ^{∈} V, or

4. s_{1} ^{∈} V and s_{|s|} ^{∈} V and if s_{i} ^{∈} C for some i then t_{j} ^{∈} V for some j, or

5. t_{1} ^{∈} V and t_{|t|} ^{∈} V and if t_{i} ^{∈} C for some i then s_{j} ^{∈} V for some j.

Proof of lemma. Analyze all possible combinations of variables and constants within the strings s and t. The five cases describe all the combinations where unification is possible. In all other cases s and t cannot be unified. ⊓ ⊔

Theorem 9 (Complexity of Decidability). The existence of a T-unifier for the equation s=t, where s and t are T-strings, can be decided in time O(|s|+|t|).

Proof of theorem. The five cases mentioned in lemma 8 can be checked in linear time with respect to the length of s and t. ⊓ ⊔

5 There is a close relationship between these logics since J can be embedded into S4. 6 This property follows from the fact that the accessibility relation of the modal logic S4

is reflexive and transitive.

3.2 A Graphical Representation

Before we give a detailed description of our unification procedure, we first want to introduce a graphical method for representing the set of most general T-unifiers for a given equation of T-strings. It is somewhat similar to Makanin’s notion of an equation with scheme [9, 10].

Example 7. The strings s=aBcDEf and t=aBGhiJ fulfill the T-string property. If we want to unify them (i.e. find a most general T-unifier for {s=t}) we have to look for a mapping which assigns a substring of t to each variable in s and vice versa. We can represent this mapping by the following scheme:

\begin{matrix}a & B & c & & & D & & E & f \\ a & B & & G & h & & i & J \end{matrix}

_{X′}  _{Y′}

The T-unifier derived from this scheme is σ_{1} = {G\cX′, D\X′hiY′, J\Y′Ef} where X′ and Y′ are new variables which do not occur in the strings s or t. It is necessary to introduce these variables in order to obtain a most general T-unifier.^{7} To get all T-unifiers we just have to consider all possible correct schemes.

In general we have to perform the following steps in order to get a scheme representation of the most general T-unifiers for a T-string equation s=t: We start by writing down the first string s in a way such that constants will receive a small slot and variables will receive a large slot.^{8} In the row below we write down the second string t such that

1. equal characters at the beginning of s and t appear in the same column,

2. a constant occurs only within the range of a variable (except for constants in the common substring at the beginning) and

3. the range of each variable may be stretched arbitrarily so that it may overlap with a variable of the first string.

In the first row (of the second string) we begin by stretching the variables as little as possible. Below we will then systematically enumerate all the possibilities for extending the range of one or more variables. Each of these rows (except the one representing the first string) represents a most general T-unifier and each most general T-unifier is represented by one row of the scheme.

Example 8. Continuing our previous example and applying this technique to unify the strings s=aBcDEf and t=aBGhiJ we get the following scheme:

\begin{matrix}a & B & c & & & & D & & & & & E & & & & f \\ a & B & & & G & & & & h & i & & & & J \\ a & B & & G & & h & & i & & & & J \\ a & B & & & & & G & & & & h & & i & & J \end{matrix}

7 σ′ = {G\c, D\hi, J\Ef} is not a most general T-unifier since it is an instance of σ_{1}. 8 Technically it suffices to reserve a slot of the size of the second string t.

Given such a graphical scheme the unifier of s and t implicitly contained in each row can easily be computed:

1. Constants and variables occuring in the range of a variable will assigned to this variable and

2. new variables will have to be generated and assigned accordingly if two variables of s and t overlap.

Performing this final step will lead to the desired set of most general T-unifiers for the equation {s=t}.

Example 9. According to the scheme in example 8 we compute the following set of most general unifiers for the T-strings s=aBcDEf and t=aBGhiJ:

σ_{0} = {G\cX′, D\X′h, E\iY′, J\Y′f} (first row),

σ_{1} = {G\cX′, D\X′hiY′, J\Y′Ef} (second row), and
σ_{2} = {G\cDX′, E\X′hiY′, J\Y′f} (third row)

where X′ and Y′ are new variables.

3.3 Transforming Equations

The intuitive graphical technique given above should be sufficient to understand the following formalized method for T-string-unification. Rather than by giving a recursive algorithm we consider the process of unification as a sequence of transformations on systems of equations. This concept is similar to the ideas of Martelli & Montanari ([11], see also [12, 18]).

To keep our notation simple we divide our system of equations into an unsolved part Γ that initially contains the equations to be solved, and into a solved part σ which represents a substitution. We start with a given system Γ = {s_{i}=t_{i} | i = 1, .., n} of equations and an empty substitution σ = ∅ and stop with an empty system of equations Γ = ∅ and a substitution σ = {x_{j}\t_{j} | j = 1, .., m} representing an idempotent most general T-unifier. Each transformation step replaces a system Γ, σ by a modified system Γ′, σ′.

The algorithm is described by transformation rules which can be applied nondeterministically to the actual equation system. A sequence of transformations is successful if it transforms Γ into an empty set of equations. Each successful chain of transformations corresponds to one most general T-unifier for Γ. For technical reasons we divide the right part t of each equation into two parts t^{1} and t^{2}, i.e. we consider equations of the form s_{i}=t_{i}^{1}|t_{i}^{2}.^{9} Hence we will start with the slightly modified equation system Γ = {s_{i}=ε|t_{i} | i = 1, .., n}.

We shall first formalize the transformation algorithm and specify the transformation rules afterwards.

9 As in the graphical representation of our method the vertical bar represents the end of a substring which will be assigned to a variable. Some transformation rules (e.g. R5, R7, and R9 in table 1) will perform this assignment while others (e.g. R10) move the vertical bar in order to create alternatives.

Definition 10 (Transformation Algorithm). Let Γ = {s_{i}=ε|t_{i} | i = 1, .., n} be a system of equations where the s_{i}, t_{i} are T-strings over an alphabet V ∪ C. Let σ=∅ and let T = {Π_{i}→Δ_{i}, Θ_{i} | i = 1, .., k} be a set of transformation rules. The following (nondeterministic) transformation algorithm computes a set of most general T-unifiers for Γ. while Γ ≠ ∅ do

a. select the leftmost equation s=t from Γ

b. set Γ to Γ \ {s=t}

c. select a transformation rule Π→Δ, Θ from T which is applicable to {s=t};

if no rule is applicable then stop with failure d. apply the rule Π→Δ, Θ to {s=t}

let Δ′, Θ′ be the result of this transformation e. apply the substitution Θ′ to Γ and σ (compute Γ:=Θ′(Γ) and σ:=Θ′(σ)) f. set Γ to Δ′ ∪ Γ; set σ to σ ∪ Θ′

stop with success and return σ. The set of most general T-unifiers consists of the results of all successfully finished transformations. In each case σ represents an idempotent most general T-unifier.

Remark. The selection of an equation in step a. can be done arbitrarily. The algorithm will, however, be more comprehensible if we make this choice systematically and first solve one equation before considering the next one.

Definition 11 (Transformation Rules for J). Let V be a set of Variables, C a set of Constants and V′ a set of auxiliary variables with V ∩ V′=∅. The set T of transformation rules for the intuitionistic logic J consists of the following 10 rules:

R1. {ε = ε|ε}  → {}, {}
R2. {ε = ε|t^{+}}  → {t^{+} = ε|ε}, {}
R3. {Xs = ε|Xt}  → {s = ε|t}, {}
R4. {Cs = ε|V t}  → {V t = ε|Cs}, {}
R5. {V s = z|ε}  → {s = ε|ε}, {V \z}
R6. {V s = ε|C_{1}t} → {s = ε|C_{1}t}, {V \ε}
R7. {V s = z|C_{1}C_{2}t} → {s = ε|C_{2}t}, {V \zC_{1}}
R8. {V s^{+} = ε|V_{1}t} → {V_{1}t = V |s^{+}}, {}
R9. {V s^{+} = z^{+}|V_{1}t} → {V_{1}t = V′|s^{+}}, {V \z^{+}V′}
R10. {V s = z|Xt}  → {V s = zX|t}, {}, where V ≠X, and s=ε or t≠ε or X^{∈} C

s, t and z denote (arbitrary) strings and s^{+}, t^{+}, z^{+} non-empty strings. X, V, V_{1}, C, C_{1} and C_{2} denote single characters with X^{∈} V ∪ C ∪ V′, V, V_{1} ^{∈} V ∪ V′ (with V ≠V_{1}), and C, C_{1}, C_{2} ^{∈} C. V′ ^{∈} V′ is a new variable which does not occur in the substitution σ computed so far.

Table 1. Transformation Rules for Intuitionistic Logic

Example 10. Consider our previous example, i.e. let Γ = {aBcDEf=ε|aBGhiJ}, σ=∅, and X′, Y′ auxiliary variables. We explain the unification algorithm by a successive application of transformation rules starting with the equation system Γ and the empty substitution σ. According to our algorithm we always select the first equation of Γ. We shall write Γ, σ ⟶^{Ri} Γ′, σ′ to denote that applying rule Ri to Γ (and σ) leads to the modified system Γ′ and the modified substitution σ′.

During the first three steps the transformation is straightforward.

{aBcDEf=ε|aBGhiJ}, {}

⟶^{R3} {BcDEf=ε|BGhiJ}, {}

⟶^{R3} {cDEf=ε|GhiJ}, {}

⟶^{R4} {GhiJ=ε|cDEf}, {}

Now two rules (R6 and R10) are applicable. We first consider R6 and then R10.

1. ⟶^{R6} {hiJ=ε|cDEf}, {G\ε} ⟶ ⊥ (no transformation rule applicable)

2. ⟶^{R10} {GhiJ=c|DEf}, {}

Again there are two possibilities (R9 and R10):

(a) ⟶^{R9} {DEf=X′|hiJ}, {G\cX′}

i. ⟶^{R7} {Ef=ε|iJ}, {G\cX′, D\X′h}

A. ⟶^{R6} {f=ε|iJ}, {G\cX′, D\X′h, E\ε} ⟶ ⊥

B. ⟶^{R10} {Ef=i|J}, {G\cX′, D\X′h}

⟶^{R9} {J=Y′|f}, {G\cX′, D\X′h, E\iY′}

⟶^{R10} {J=Y′f|ε}, {G\cX′, D\X′h, E\iY′}

⟶^{R5} {ε=ε|ε}, {G\cX′, D\X′h, E\iY′, J\Y′f}

⟶^{R1} \{\}, \underline{\{G\cX′, D\X′h, E\iY′, J\Y′f\}} σ_{0}

ii. ⟶^{R10} {DEf=X′h|iJ}, {G\cX′}

⟶^{R10} {DEf=X′hi|J}, {G\cX′}

⟶^{R9} {J=Y′|Ef}, {G\cX′, D\X′hiY′}

⟶^{R10} {J=Y′E|f}, {G\cX′, D\X′hiY′}

⟶^{R10} {J=Y′Ef|ε}, {G\cX′, D\X′hiY′}

⟶^{R5} {ε=ε|ε}, {G\cX′, D\X′hiY′, J\Y′Ef}

⟶^{R1} \{\}, \underline{\{G\cX′, D\X′hiY′, J\Y′Ef\}}  σ_{1}

(b) ⟶^{R10} {GhiJ=cD|Ef}, {}

i. ⟶^{R9} {Ef=X′|hiJ}, {G\cDX′}

A. ⟶^{R7} {f=ε|iJ}, {G\cDX′, E\X′h} ⟶ ⊥

B. ⟶^{R10} {Ef = X′h|iJ}, {G\cDX′}

⟶^{R10} {Ef=X′hi|J}, {G\cDX′}

⟶^{R9} {J=Y′|f}, {G\cDX′, E\X′hiY′}

⟶^{R10} {J=Y′f|ε}, {G\cDX′, E\X′hiY′}

⟶^{R5} {ε=ε|ε}, {G\cDX′, E\X′hiY′, J\Y′f}

⟶^{R1} \{\}, \underline{\{G\cDX′, E\X′hiY′, J\Y′f\}} σ_{2}

ii. ⟶^{R10} {GhiJ=cDE|f}, {}

⟶^{R10} {GhiJ=cDEf|ε}, {}

⟶^{R5} {hiJ=ε|ε}, {G\cDEf} ⟶ ⊥

As a result we get three most general T-unifiers σ_{0}, σ_{1}, σ_{2} which are identical with the ones evaluated with the graphical method in the previous subsection.

Remark. If we use a T-string-unification algorithm within a proof procedure we can replace the auxiliary variables by the empty string after unification, i.e. we apply the substitution {V′\ε | V′ ^{∈} V′} to each calculated most general T-unifier.

3.4 Correctness, Termination, Minimality and Completeness

In the following we prove correctness, termination, minimality and completeness of T-string-unification (or briefly T-unification).

Lemma 12 (T-String Preserving). Let Γ = {s_{1}=t_{1}, …, s_{n}=t_{n}} be a system of equations where S={s_{i} | i=1, …, n}∪{t_{i} | i=1, …, n} has the T-string property and let σ be a most general T-unifier for {s_{1}=t_{1}}. Then the set σ(S):={σ(u) | u^{∈} S} also fulfills the T-string property.

Proof of lemma. We can represent the elements of S as branches of a tree which splits if the elements become different. If we unify the two branches corresponding to s_{1} and t_{1}, the result will still be a tree since all the additional variables we may insert are unique. ⊓ ⊔

Because of lemma 12 we can restrict ourselves to unifying systems containing only a single equation s=t instead of having to unify a larger system Γ all at once. After solving the first equation we may choose the next equation and so on since the strings of each equation fulfill the T-string property under the computed substitution. This insight will drastically simplify the proofs of correctness, minimality, termination, and completeness.

Definition 13 (Result mgu_{T} of T-String-Unification). Let Γ be a system of equations. mgu_{T}(Γ) denotes the set of substitutions computed by the specified algorithm for T-string-unification.

Theorem 14 (Correctness of T-Unification). Let Γ ={s=ε|t} be an equation of T-strings. Then mgu_{T}(Γ) is correct, i.e. each σ^{∈} mgu_{T}(Γ) is a T-unifier for Γ.

Proof of theorem. Let Γ = {s=z|t} be an equation and k(Γ) be the number of rule applications necessary for computing a T-unifier for Γ. We prove the theorem by induction on k(Γ) and show that σ^{∈} mgu_{T}(Γ) is correct for n=k(Γ). For n=1 we have Γ = {ε=ε|ε}. Applying rule R1 we obtain Γ ={} and the substitution σ={} which is a correct T-unifier for Γ. Let Γ = {s=z|t} with k(Γ) = n+1 and Ri be a transformation rule which is applicable to {s=z|t}. Let Δ′, Θ′ be the result of this application. By the induction hypothesis σ^{∈} mgu_{T}(Δ′) is a correct T-unifier for Δ′ (if some σ exists), since k(Δ′) = n. Then Θ′∪σ is a correct T-unifier for Γ, since (Θ′∪σ)(s) = (Θ′∪σ)(z t) if σ is a correct T-unifier for Δ′. ⊓ ⊔

Theorem 15 (Termination of T-Unification). Let Γ ={s=ε|t} be an equation of T-strings. Then the specified T-string-unification terminates on Γ.

Proof of theorem. Let Γ ={s=z|t}. We define a well-ordered relation <_{Γ} between systems of equations and show that after applying at most two transformation rules to Γ the property Γ′<_{Γ} Γ holds between Γ and the resulting system Γ′. This property is defined as follows:

Let Γ_{1} = {s_{1}=z_{1}|t_{1}} and Γ_{2} = {s_{2}=z_{2}|t_{2}}. The system ordering <_{Γ} is a relation on system equations in the following way:

Γ_{1}<_{Γ} Γ_{2} ⇔ \{ \begin{matrix}|s_{1}z_{1}t_{1}| < |s_{2}z_{2}t_{2}|, or \\ |s_{1}z_{1}t_{1}| = |s_{2}z_{2}t_{2}| and |z_{1}| > |z_{2}|, or \\ Γ_{1}=\{\} and Γ_{2}=\{ε=ε|ε\}. \end{matrix}

Let Γ ={s=z|t} be a system of equations and Ri a transformation rule which is applicable to Γ. Let Δ′, Θ′ denote the result of this transformation. We distinguish three cases:

1. Applying one of the rules R1, R3, R5,R6, R7, R8, R9, or R10 we get Δ′<_{Γ} Γ.

2. After applying rule R2, the only applicable rule to the resulting system Δ′ would be R5. Let this application yield the system Δ′′. From 1. we conclude that Δ′′<_{Γ} Γ.

3. After applying rule R4 the only applicable rules to the result Δ′ could be R6, R7 or R10. Let this application yield Δ′′. From 1. we conclude that Δ′′<_{Γ} Γ.

Since there are only finitely many transformation rules applicable to a system Γ and the relation <_{Γ} is well-ordered, every transformation chain will be finite. ⊓ ⊔

Theorem 16 (Minimality of T-Unification). Let Γ ={s=ε|t} be an equation of T-strings. Then mgu_{T}(Γ) is minimal, i.e. no substitution σ^{∈} mgu_{T}(Γ) is an instance of another substitution σ′ ^{∈} mgu_{T}(Γ).

Proof of theorem (sketch). We show that the application of different rules to a system Γ = {s=z|t} yields different assignments to at least one variable such that the assignments are not an instance of each other.

If one of the rules R1 to R5 is applicable to Γ then no other rule will be applicable to Γ. If one of the rules R6 to R10 is applicable to {V s=z|t} there may be another rule which is also applicable. By a lengthy case analysis it can be verified that the application of different rules assigns different strings to the variable V. Therefore none of the computed substitutions are instances of each other. ⊓ ⊔

Theorem 17 (Completeness of T-Unification). Let Γ ={s=ε|t} be an equation of T-strings. Then mgu_{T}(Γ) is complete, i.e. each T-unifier of Γ is an instance of some σ^{∈} mgu_{T}(Γ).

Proof of theorem (sketch). If we investigate the pattern of a string assigned to a variable we can determine that they must have a certain form. For example auxiliary variables may only occur at the beginning or at the end of such a string. By examining all these possibilities we can verify that each such assignment is calculated by the algorithm. ⊓ ⊔ 3.5 Complexity

Since the complexity of the unification process is determined by the number of computed unifiers, we will now investigate the number of most general T-unifiers. As mentioned before this number is finite but can be extremely large.

Theorem 18 (Complexity of T-Unification). In the worst case the number of most general T-unifiers for s and t grows exponentially w.r.t. the length of s and t: The number of mgu’s can be up to \frac{1}{2} \frac{(2n)!}{(n!)^{2}} ^{∈} O(\frac{2^{2n}}{\sqrt{n}}) where n = max(|s|, |t|).

Proof of theorem. In the worst case one string contains only variables and the other only constants. In this case unification is the same as matching and we have to consider every possible assignment of constant strings to variables. This number is equal to the number of possibilities to select n elements out of 2n−1 where n is the length of the two unified strings. Hence we get ( \begin{matrix}2n−1 \\ n \end{matrix} ) = \frac{(2n−1)!}{n!(n−1)!} = \frac{1}{2} \frac{(2n)!}{(n!)^{2}}

most general T-unifiers. Using the approximation n! ≈ \sqrt{n} · n^{n} we get for large n:

\frac{1}{2} ^{\frac{\sqrt{2n}(2n)^{2n}}{(\sqrt{n}n^{n})^{2}}} = \frac{1}{\sqrt{2n}}(\frac{2n}{n})^{2n} = \frac{1}{\sqrt{2n}}2^{2n} ^{∈}O(\frac{2^{2n}}{\sqrt{n}}) ⊓ ⊔

Example 11. Consider the strings AB and cd where A, B are variables and c, d are constants. The most general T-unifiers can be represented by the following scheme:

\begin{aligned}& A & & & B \\ c & & d & & ε \\ & c & & & d \\ & ε & & c & & d \end{aligned}

The number of most general T-unifiers is \frac{1}{2} \frac{4!}{(2!)^{2}} = 3.

3.6 Implementation of T-String-Unification

The implementation of our unification procedure has been written in Prolog but may easily be translated into a functional or an imperative programming language.

Strings are represented as Prolog lists, i.e. the string w=v_{1}v_{2} … v_{n} is represented by the list W=[v1,v2,...,vN]. As usual variables are written in capitals whereas constants are written in small letters. The predicate tunify(S,[],T) succeeds if the T-strings S and T can be unified. In this case the instantiated variables represent a most general T-unifier for S and T. All other most general T-unifiers will be computed via backtracking. Each clause of the predicate tunify corresponds to exactly one transformation rule as defined in table 1.

To solve a set of string equations the predicate t_string_unify(G) is used. G is a set of equations, i.e. a set whose elements have the form S=T, where S and T are strings. Once again the set of most general T-unifiers is calculated via backtracking.^{10}

10 The variables may be instantiated with nested lists. Therefore the predicate flatten is necessary which can be implemented as follows:

  flatten(A,[A|B],B) :- (var(A); atom(A)) -> A\==[], !.   flatten([],A,A).
  flatten([A|B],C,D) :- flatten(A,C,E), flatten(B,E,D).

t_string_unify([]).
t_string_unify([S=T|G])  :- flatten(S,S1,[]), flatten(T,T1,[]),
                            tunify(S1,[],T1), t_string_unify(G).
tunify([],[],[]).
tunify([],[],[X|T])      :- tunify([X|T],[],[]).
tunify([X1|S],[],[X2|T]) :- X1==X2, !, tunify(S,[],T).
tunify([C|S],[],[V|T])   :- atom(C),!,var(V),tunify([V|T],[],[C|S]).
tunify([V|S],Z,[])       :- V=Z, tunify(S,[],[]).
tunify([V|S],[],[C1|T])  :- atom(C1), V=[], tunify(S,[],[C1|T]).
tunify([V|S],Z,[C1,C2|T]):- atom(C1), atom(C2), append(Z,[C1],V),
                            tunify(S,[],[C2|T]).
tunify([V,X|S],[],[V1|T])    :- var(V1), tunify([V1|T],[V],[X|S]).
tunify([V,X|S],[Z1|Z],[V1|T]):- var(V1), append([Z1|Z],[Vnew],V),
                                tunify([V1|T],[Vnew],[X|S]).
tunify([V|S],Z,[X|T])    :- (S=[]; t\=[]; atom(X)) ->
                            append(Z,[X],Z1), tunify([V|S],Z1,T).

Remark. Note that the entered strings have to fulfill the T-string property. Otherwise no sensible output will be given.

4 T-String-Unification for Modal Logics

If we want to apply T-string-unification to the modal logics, we have to respect the accessibility relation for these logics. This means that we are not allowed to assign arbitrary strings to variables but only strings with certain restrictions on their length.

In the following we will treat the modal logics D, K, D4, K4, S4, S5 and T. For each logic we shall define the essential restrictions, specify the transformation rules and investigate the complexity of the corresponding unification process.

4.1 The Modal Logics D and K

The modal logics D and K, together with S5, are the simplest. Variables may only be instantiated with exact one single character, i.e. for every T-unifier σ the following property must hold: |σ(V)| = 1 for all V ^{∈} V. This restriction (see [19]) follows from the fact that the accessibility relation for D and K has no special properties which can be guaranteed. Accordingly we only need the transformation rules R1, R3, R4 of table 1 and have to add one new rule (R2):

R1. {ε = ε|ε}  → {}, {}
R2. {V s = ε|Xt} → {s = ε|t}, {V \X}, where V ≠X
R3. {Xs = ε|Xt} → {s = ε|t}, {}
R4. {Cs = ε|V t} → {V t = ε|Cs}, {}

s and t denote arbitrary strings, X, V and C denote a single character, constant, or variable, respectively, i.e. X^{∈} V∪C, V ^{∈} V and C^{∈} C.

Table 2. Transformation Rules for the Modal Logics D and K

Example 12. Consider the well known strings aBcDEf and aBGhiJ. The following scheme represents the graphical unification:

\begin{matrix}a & B & c & D & E & f \\ a & B & G & h & i & J \end{matrix}

The only most general T-unifier is σ = {G\c, D\h, E\i, J\f}.

In general there is at most one most general unifier for every unification problem in the modal logics K and D.^{11}

4.2 The Modal Logics D4 and K4

In the modal logic D4 and K4 variables may only be instantiated with non-empty strings since the accessibility relation for D4 and K4 is transitive (see [19]). Thus for every T-unifier σ the property |σ(V)| ≥ 1 must hold for all V ^{∈} V. The rules R1 to R4 and R7 to R10 are identical with those for intuitionistic logic in table 1. For the rules R5 and R6 we need an additional restriction. This results in the following rules:

R1. – R4. see transformation rules for J

R5. {V s = z|ε} → {s = ε|ε}, {V \z}, where z≠ε or (V ^{∈} V′ and R_{V}^{(σ)})
R6. {V s = ε|C_{1}t} → {s = ε|C_{1}t}, {V \ε}, where V ^{∈} V′ and R_{V}^{(σ)}

R7. – R10. see transformation rules for J

s, t and z denote arbitrary strings, V ^{∈} V∪V′, C_{1} ^{∈} C and the restriction R_{V}^{(σ)} is defined as

R_{V}^{(σ)}:= \{ \begin{matrix}false & , if Ṽ \V ^{∈} σ for some Ṽ ^{∈} V \\ true & , otherwise \end{matrix} , where σ is the substitution computed so far.

Table 3. Transformation Rules for the Modal Logics D4 and K4

Remark. The auxiliary variables may be removed from the most general T-unifiers after unification so that the property above is respected.

Example 13. Consider the strings aBCDeF and aghIj. The most general T-unifier can be calculated using the following scheme:

a  B  C  D  e  F
a  g  h  I  j
a g h  I  j

The most general T-unifiers are σ_{0} = {B\g, C\hX′, I\X′DeY′, F \Y′j} and σ_{1} = {B\ghX′, I\X′CDeY′, F \Y′j}.

As in the intuitionistic case the number of computed most general T-unifiers is finite but may grow exponentially with respect to the length of the strings.

11 We want to point out that the existence of a T-unifier is not sufficient for the complementarity of two atoms in the modal logics K or K4. An additional criterion has to be fulfilled in these cases (see [19]).

4.3 The Modal Logics S4 and S5

The modal logic S4, where the accessibility relation is reflexive and transitive, can be treated in the same way as the intuitionistic logic. We can use the general T-string-unification algorithm (see section 3) without any additional restrictions.

The modal logic S5 is trivial since the strings we want to unify simply consist of a single character which is either a variable or a constant. This follows from the fact that the accessibility relation for S5 is an equivalence relation (see [19]). Therefore the set of most general T-unifiers is a singleton set and we only need three transformation rules:

R1. {V = ε|X} → {}, {V \X}, where V ≠X
R2. {X = ε|X} → {}, {}
R3. {C = ε|V } → {V = ε|C}, {}

X, V and C denote single characters with X^{∈} V∪C, V ^{∈} V and C^{∈} C.

Table 4. Transformation Rules for the Modal Logic S5

4.4 The Modal Logic T

In the modal logic T strings may only be instantiated with at most one character since the accessibility relation for T is reflexive (see [19]). Thus for every T-unifier σ the following property must hold: |σ(V)| ≤ 1 for all V ^{∈} V. Whereas the transformation rules R1 to R3 can be taken unchanged from table 1 for intuitionistic logic we slightly have to modify the rules R5 and R8 to R10 and add new rules R6 and R7. This results in the following transformation rules:

R1. – R3. see transformation rules for J

R5. {V s = z_{v}|ε}  → {s = ε|ε}, {V \z_{v}}
R6. {s_{1}V s_{2} = z|Ct} → {s_{1} = ε|z, s_{2} = ε|t}, {V \C} ∪ σ_{V}^{(σ)}
R7. {s_{c}^{+} = ε|t_{v}^{+}}  → {t_{v}^{+} = ε|s_{c}^{+}}, {}
R8. {V s_{v}^{+} = ε|V_{1}t_{v}} → {V_{1}t_{v} = V |s_{v}^{+}}, {}
R9. {V s_{v}^{+} = z^{+}|V_{1}t_{v}} → {V_{1}t_{v} = V′|s_{v}^{+}}, {V \z^{+}V′}
R10. {Xs = z|V t}  → {Xs = zV |t}, {}, where X≠V, and s=ε or t≠ε

s, t and z denote arbitrary strings, s^{+}, t^{+}, z^{+} non-empty strings; strings indexed with a v may only contain variables, strings indexed with a c must contain at least one constant; X^{∈} V∪C∪V′, V, V_{1} ^{∈} V∪V′ (with V ≠V_{1}), V′ ^{∈} V′ and C^{∈} C; the substitution σ_{V}^{(σ)} is defined as σ_{V}^{(σ)}:={Ṽ \ε | X\t^{∈} σ where t contains V and Ṽ for some X, Ṽ ^{∈} V∪V′ with V ≠Ṽ } where σ is the substitution computed so far.

Table 5. Transformation Rules for the Modal Logic T

Remark. To ensure the above property variables which are not assigned to nonempty strings may be replaced by the empty string after the unification process, i.e. we apply the substitution {V \ε | V ^{∈} (V∪V′)} to every calculated most general T-unifier.

Example 14. Consider the strings aBCDeF, aGhiJ and the following scheme representing the most general T-unifiers:

\begin{matrix}a & B & C & D & e & F \\ a & h & i & ε & J & ε \\ a & h & ε & i & J & ε \\ a & G & h & i & J & ε \end{matrix}

The most general T-unifiers are σ_{0} = {G\ε, B\h, C\i, D\ε, J\e, F \ε}, σ_{1} = {G\ε, B\h, C\ε, D\i, J\e, F \ε} and σ_{2} = {B\G, C\h, D\i, J\e, F \ε}.

Once again the number of most general unifiers is finite but may grow exponentially with respect to the length of the unified strings.

5 Conclusion

We have developed an efficient algorithm for unifying strings which correspond to prefixes of atomic formulae in a formula tree. It can be used to guide the search for a proof in various non-classical logics and plays a fundamental role within efficient proof procedures for these logics. Our method has been described following the terminology of Wallen [19] but it can be applied directly to Ohlbach’s world-paths [12, 13] as well.

Our generic algorithm is based on a small set of transformation rules which encode the peculiarities and restrictions of a particular logic. By modifying this set of transformation rules we were able to adopt it to a variety of non-classical logics such as intuitionistic logic J and the modal logics D, K, D4, K4, S4, S5, and T. In the future we shall investigate how our algorithm can be extended to some subset of linear logic and other important non-classical logics. For these logics, however, a characterization for validity and the notion of a prefix still has to be developed.

Our algorithm is much simpler and considerably more efficient than other string unification algorithms developed so far. The algorithms described in [9, 10, 1] are developed for general string unification and do not take advantage of the special properties of prefix strings. Ohlbach’s algorithm [13] does not compute a minimal set of unifiers and thus wastes computation time. Besides this one of the main advantages of our algorithm is that it generates unifiers step by step instead of computing them all at once. This will become particularly important when using the algorithm within a proof procedure since it will seldomly be the case that all possible unifiers have to be investigated during a proof search. Our algorithm will therefore lead to the implementation of a very efficient proof search procedure for non-classical logics.

Our unification algorithm has been implemented in Prolog and tested within a prototypical theorem prover for intuitionistic logic (see [15]). In the future we shall integrate it into a general proof procedure for non-classical logics (see e.g. [14]) and investigate the practical efficiency of the resulting proof technique. In particular we intend to compare it with a method which first translates these logics into classical logic and then uses one of the existing classical theorem provers.

References

1. H. Abdulrab and J.-P. Pecuchet. Solving word equations. In C. Kirchner, editor, Unification, pages 353–375. Academic Press, London, 1990.

2. B. Beckert and J. Posegga. leanTAP: Lean tableau-based theorem proving. In Alan Bundy, editor, Proceedings of the 12^{th} Conference on Automated Deduction, LNAI 814, Springer Verlag, 1994.

3. E. W. Beth. The foundations of mathematics. North–Holland, 1959.

4. W. Bibel, S. Brüning, U. Egly, T. Rath. Komet. In Alan Bundy, editor, Proceedings of the 12^{th} Conference on Automated Deduction, LNAI 814, pages 783–787. Springer Verlag, 1994.

5. W. Bibel. On matrices with connections. Jour. of the ACM, 28, p. 633–645, 1981.

6. W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987.

7. J. J. Herbrand. Recherches sur la théorie de la démonstration. Travaux Soc. Sciences et Lettres Varsovie, Cl. 3 (Mathem., Phys.), page 128 pp., 1930. Engl. transl. in W. D. Goldfarb, ed. J.J. Herbrand — Logical writings, Reidel, 1971.

8. R. Letz, J. Schumann, S. Bayerl, W. Bibel. Setheo: A high-performance theorem prover. Journal of Automated Reasoning, 8:183–212, 1992.

9. G. S. Makanin. The problem of solvability of equations in a free semigroup. Math. Sb., 103(145):147–236, 1977. English translation: Math. USSR Sb. 32.

10. G. S. Makanin. Algorithmic decidability of the rank of constant free equations in a free semigroup. Dokl. Akad. Nauk, SSSR, 243, 1978.

11. A. Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems (TOPLAS), 4:258–282, 1982.

12. H. J. Ohlbach. A resolution calculus for modal logics. Ph.D. Thesis (SEKI Report SR-88-08), Universität Kaiserslautern, 1988.

13. H. J. Ohlbach. A resolution calculus for modal logics. In E. Lusk and R. Overbeek, editors, Proceedings of the 9^{t}^{h} Conference on Automated Deduction, LNCS 310, pages 500–515. Springer Verlag, 1988.

14. J. Otten, C. Kreitz. A connection based proof method for intuitionistic logic. In Proceedings of the 4^{th} Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918, pp. 122–137, Springer Verlag, 1995.

15. J. Otten. Ein konnektionenorientiertes Beweisverfahren für intuitionistische Logik. Master’s thesis, TH Darmstadt, 1995.

16. G. Plotkin. Building-in Equational Theories. Machine Intelligence, 7:73–90, Edinburgh University Press, 1972.

17. J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery, 12(1):23–41, January 1965.

18. M. Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories. In E. Lusk and R. Overbeek, editors, Proceedings of the 9^{t}^{h} Conference on Automated Deduction, LNCS 310, pages 378–392. Springer Verlag, 1988.

19. L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990.

20. L. Wos et. al. Automated reasoning contributes to mathematics and logic. In Proceedings of the 10^{t}^{h} Conference on Automated Deduction, LNCS 449, pages 485– 499. Springer Verlag 1990.

This article was processed using the LaTEX macro package with LLNCS style