Unification in Sort Theories

and its Applications

Christoph Weidenbach

MPI–I–94–211 March 1994 Author’s Address

Max-Planck-Institut für Informatik, Im Stadtwald, W-6600 Saarbrücken 11, Germany. Email: weidenb@mpi-sb.mpg.de

Publication Notes

Submitted to the Journal “Annals of Mathematics and Artificial Intelligence”.

Acknowledgements

This work was supported by the ESPRIT project 6471 MEDLAR of the European Community.

I would like to thank my colleages at the Max-Planck-Institut for many helpful comments on this paper.

Abstract

In this article I investigate the properties of unification in sort theories. The usual notion of a sort consisting of a sort symbol is extended to a set of sort symbols. In this language sorted unification in elementary sort theories is of unification type finitary. The rules of standard unification with the addition of four sorted rules form the new sorted unification algorithm. The algorithm is proved sound and complete. The rule based form of the algorithm is not suitable for an implementation because there is no control and the used data structures are weak. Therefore we transform the algorithm into a deterministic sorted unification procedure. For the procedure sorted unification in pseudo-linear sort theories is proved decidable.

The notions of a sort and a sort theory are developed in a way such that a standard calculus can be turned into a sorted calculus by replacing standard unification with sorted unification. To this end sorts may denote the empty set. Sort theories may contain clauses with more than one declaration and may change dynamically during the deduction process. The applicability of the approach is exemplified for the resolution and the tableau calculus.

Keywords

Sorts, Sorted Unification, Sorted Resolution, Sorted Tableau

1 Introduction

The advantages of sorts in automated reasoning are well known [15, 21, 18, 4, 27, 10, 14, 22, 31, 1, 5, 12, 29]. The difference between standard first-order calculi and their sorted counterparts amounts to an extended language and special reasoning mechanisms for sorts, monadic predicates. The language is extended by attaching sorts to variables, i.e. the domain of variables can be restricted to subsets (the interpretation of sorts) of the domain (the interpretation of the top sort). This additional information is exploited in the sorted unification algorithm which replaces standard unification. Sorted unification is performed with respect to a sort theory (a set of formulae containing sorts).

In the standard setting [27, 10, 22, 1] a sort theory L consists of a set of unit clauses each containing a declaration (atoms with monadic predicate as top symbol). An example for such a sort theory is

L = {S(a), S(f(x_{S})), T (a), T (f(y_{T}))}

Now to solve the unification problem [23]

Γ = {x_{S} = y_{T} }

the unification problem must be standard solved and variables have to be weakened (instantiated by appropriate terms) until the components of the corresponding unifier are well-sorted. A component x_{S} ↦ t is well-sorted if in every model of L we have S(t). As L has a special structure there exists always a free model for L, the free term algebra T of well-sorted terms. Computations in this algebra are efficient. Following the above example, well-sorted terms of sort S and T are

\begin{aligned}T_{S} & = & \{x_{1}, x_{2}, …, a, f(a), f(f(a)), …\} \\ T_{T} & = & \{y_{1}, y_{2}, …, a, f(a), f(f(a)), …\} \end{aligned}

where all x_{j} have sort S (this is written S(x_{j}) = S), S(y_{j}) = T, and there are infinitely many variables in each set. As neither x_{S} ∈ T_{T} nor y_{T} ∈ T_{S} the unification problem Γ is not sorted solved. At least one of the variables must be weakened. The sort theory allows weakening using the declarations S(a), T (a), and S(f(x_{S})), T (f(y_{T})), respectively. Using the first two declarations we get the well-sorted unifier

σ_{1} = {x_{S} ↦ a, y_{T} ↦ a}

The second two declarations lead to the still unsolved unification problem

Γ′ = {x_{S} = f(x′_{S}), y_{T} = f(y′_{T}), x′_{S} = y′_{T} }

Again the four declarations selected before must be applied to x′_{S} = y′_{T} resulting in infinitely many well-sorted mgu’s

σ_{2} = {x_{S} ↦ f(a), y_{T} ↦ f(a)}
σ_{3} = {x_{S} ↦ f(f(a)), y_{T} ↦ f(f(a))}
⋮

The first extension I make to this standard setting allows the domain of variables to be restricted to a set of sorts, interpreted as the intersection of the sorts. For the example the free algebra then is

\begin{aligned}T_{S} & = & \{x_{1}, x_{2}, …, z_{1}, z_{2}, …, a, f(a), f(f(a)), …\} \\ T_{T} & = & \{y_{1}, y_{2}, …, z_{1}, z_{2}, …, a, f(a), f(f(a)), …\} \\ T_{\{S,T \}} & = & \{z_{1}, z_{2}, …, a, f(a), f(f(a)), …\} \end{aligned}

where S(x_{j}) = S, S(y_{j}) = T, and S(z_{j}) = {S, T }. Instead of the set {S} we simply write the sort symbol S. Having the extended sort language the solution to Γ is one single most general well-sorted unifier

σ = {x_{S} ↦ z_{{S,T }}, y_{T} ↦ z_{{S,T }}}

The new notion allows a finite set of unifiers in cases where previous approaches [27, 22, 1, 5] lead to infinite sets.

The second extension investigated in this article needs further motivation. The idea of sorted unification is to provide a sorted unification algorithm and a notion of a sort theory such that a standard calculus using unification can be turned into a sorted calculus by replacing standard unification with sorted unification. In addition, I don’t want to impose any restrictions on the sort theory, i.e. any monadic predicate can be used as a sort. In my previous work [28, 30] the problem is solved for the resolution calculus. It turned out not sufficient to consider unit clauses consisting of one single declaration as sort theories. All clauses consisting of declarations form the sort theory. From every clause in the sort theory exactly one declaration is selected for the construction of well-sorted terms, hence for sorted unification. The other declarations are attached to the selected declaration as a condition. Using this notion of a sort theory standard resolution can be extended to sorted resolution by replacing standard unification with sorted unification. The new notion of a sort theory makes it necessary to extend the notion of well-sortedness to a notion of conditional well-sortedness. For example having the unsatisfiable clause database Δ

Δ:

(1) S(a) ∨ R(a)
(2) S(f(x_{1}))
(3) Q(y_{1}, y_{1})
(4) ¬Q(a, y_{2})
(5) P (x_{2}, f(a))
(6) ¬P (a, x_{3})

where S(x_{i}) = S, S(y_{i}) = R. If the first clause S(a)∨R(a) is not included in the sort theory no sorted resolution step is possible. Thus one of the following sort theories must be chosen

\begin{aligned}L_{1} & = & \{(S(a), \{R(a)\}), S(f(x_{1}))\} \\ L_{2} & = & \{(S(a), \{R(a)\}), S(f(x_{1}))\} \end{aligned}

In L_{1} the declaration S(a) is selected for the generation of well-sorted terms and R(a) is attached as a condition. The sets of conditional well-sorted terms for L_{1} are:

\begin{aligned}T_{S} & = & \{x_{i}, z_{i}, (a, \{R(a)\}), (f(a), \{R(a)\}), (f(f(a)), \{R(a)\}), …\} \\ T_{R} & = & \{y_{i}, z_{i}\} \\ T_{\{S,R\}} & = & \{z_{i}\} \end{aligned}

where S(z_{i}) = {S, R}. Now solving the unification problem

Γ = {x_{3} = f(a), x_{2} = a}

the result is the conditional well-sorted mgu

σ = ({x_{3} ↦ f(a), x_{2} ↦ a}, {R(a)})

Thus choosing L_{1} sorted resolution between the clauses (5) and (6) is possible with resolvent R(a). If we choose L_{2} sorted resolution between the clauses (3) and (4) is possible with resolvent S(a). Sorted resolution is described in full detail in Section 6.

An outline of the article is this. We start with a small section on foundations (Section 2), where the syntax, semantics of the logic and some technical notions needed later on are explained. The section on standard unification (Section 3) introduces the general notions for standard unification and a rule based version of the Robinson [20] unification algorithm. These notions are then extended in the section on sorted unification (Section 4) to their sorted counterparts. The notion of conditional expressions and conditional well-sortedness are introduced. The sorted unification algorithm, an algorithm for deciding conditional well-sortedness and an algorithm for the computation of empty sorts are given. Upper bounds for the time complexity of these algorithms are established.

As a result of the extended sort language it is shown that unification in elementary sort theories is decidable and of unification type finitary. In Section 5 the sorted unification algorithm given by a set of non-deterministic rules in Section 4 is transformed into a deterministic sorted unification procedure. To this end the notion of a unification problem is extended. This makes it possible to prove sorted unification decidable for pseudo-linear sort theories, the most general result known to date for a decidable class. The section on applications (Section 6) demonstrates that the previously developed notions and algorithms make sense. Sorted unification is applied to the standard resolution calculus and the standard tableau calculus. The article is finished with a discussion on the achieved results and related work, Section 7.

2 Foundations

Preliminaries: A reflexive and transitive relation ≤ on a set A is called a quasiordering. A quasi-ordering ≤ naturally generates an equivalence relation ≡, such that a ≡ b iff a ≤ b and b ≤ a. The equivalence class in A with respect to ≡ is denoted as [a]_{≡}. We use a < b to denote that a ≤ b but not a ≡ b.

An element a is minimal in A iff for all b ∈ A: b ≤ a implies a ≤ b. A quasiordering is linear, iff a ≤ b or b ≤ a for all elements. It is well-founded, iff every chain has a minimal element. A quasi-ordering satisfying a ≤ b and b ≤ a implies a = b (antisymetrie) is called a partial ordering.

A multiset over a set A is a function M from A to the natural numbers. Intuitively, M(a) specifies the number of occurrences of a in M. We say that a is an element of M if M(a) > 0. The union, intersection, and difference of multisets are defined by the identities M_{1} ∪M_{2} = M_{1}(x)+M_{2}(x), M_{1} ∩M_{2} = min(M_{1}(x), M_{2}(x)), and M_{1} \ M_{2} = max(0, M_{1}(x) − M_{2}(x)). We often use a set-like notation to describe multisets. If we have a well-founded partial ordering on the elements of a multiset M, then we can construct recursively a well-founded multiset-ordering on multisets as follows: M > N if for some a ∈ M and b_{i} ∈ N i = 1, …, n: a > b_{i} and M \ {a} > N \ {b_{1}, …, b_{n}} (e.g. see Dershowitz [8]).

Syntax: The standard first-order signature Σ = (V_{Σ}, F_{Σ}, P_{Σ}) where V_{Σ}, F_{Σ} are infinite sets of variable and function symbols, respectively and P_{Σ} is a finite set of predicate symbols is generalized in the following way. Monadic predicates are also called base sorts. S_{Σ} is the set of all base sorts (S_{Σ} ⊆ P_{Σ}). A sorts is an element of 2^{S_{Σ}}. For ∅ ∈ 2^{S_{Σ}} we write ⊤ the usual sort attached to standard variables, ⊤ ∉ Σ and mean the top sort. As S_{Σ} is finite, 2^{S_{Σ}} is finite too. The function S, S: V_{Σ} → 2^{S_{Σ}} maps variables to sorts such that for each sort S ∈ 2^{S_{Σ}} there are infinitely many variables x with S(x) = S. In examples it is indicated that a variable x has sort S by writing x_{S}. If S is the singleton set S = {T } we often write x_{T} instead of x_{{T }}. If not stated otherwise variables not annotated with a sort have sort ⊤, the top sort.

Terms, literals, clauses, formulae, and substitutions are defined in the usual (standard) way. With ∀(F) the universal closure of a formula F is denoted. Literals built from base sorts are called sort literals. Positive sort literals are called declarations. A clause only consisting of declarations is called a declaration clause. A declaration S(t) is called a subsort declaration if t is a variable. Otherwise it is called a term declaration. If t has the form f(x_{1}, …, x_{n}) then S(t) is called a function declaration.

With DOM(σ): = {x | xσ ≠ x} we denote the finite domain of a substitution σ and COD(σ): = {xσ | x ∈ DOM(σ)}. Specific substitutions are described by their variable-term pairs, e.g. {x ↦ a} denotes the substitution x maps to a.

The function V maps terms, formulae and sets of such expressions to their variables. In order to select subterms of a given term t we use occurrences [16]. An occurrence is a word over IN. Let Λ denote the empty word. Then we define the set of occurrences Occ(t) of a term t as follows: (i) the empty word Λ is in Occ(t) (ii) i.π is in Occ(t) iff t = f(t_{1}, …, t_{n}) and π ∈ Occ(t_{i}). The depth of a term t denoted by Depth(t) is defined as the maximal length of an occurrence in Occ(t). The size of a term is the number of symbols in it, or equivalently the number of occurrences in Occ(t), Size(t): = |Occ(t)|.

A term t is called pseudo-linear if every occurrence of a variable x in t has the same length. A term t is called semi-linear [26] if for every two occurrences i_{1}...i_{k}, j_{1}...j_{k} of a variable x in t the top symbols of the terms t\i_{1}...i_{l} and t\j_{1}...j_{l} are the same for 1 ≤ l ≤ k.

Semantics: As the only extension of standard syntax are sorted variables it is sufficient to present the semantics for these variables. The semantics of sorted variables is given by the two relativization rules

\begin{aligned}∀x F & → & ∀y ((S_{1}(y) ∧ … ∧ S_{n}(y)) ⇒ F\{x ↦ y\}) \\ ∃x F & → & ∃y (S_{1}(y) ∧ … ∧ S_{n}(y) ∧ F\{x ↦ y\}) \end{aligned}

where S(x) ≠ ⊤, S(x) = {S_{1}, …, S_{n}}, S(y) = ⊤ and y does not occur in the formula F. Variables of sort ⊤ (the top sort) have the same semantics than standard variables.

An alternative semantics would be to extend standard interpretations ℑ to sorted interpretations ℑ_{S} by modifying the rules for the quantifiers. A sorted interpretation ℑ_{S} is like a standard interpretation ℑ except that:

ℑ_{S} ⊧ ∀x F iff for all a ∈ ⋂_{T ∈S(x)}ℑ_{S}(T) we have ℑ_{S}[x/a] ⊧ F
ℑ_{S} ⊧ ∃x F iff there is an a ∈ ⋂_{T ∈S(x)}ℑ_{S}(T) with ℑ_{S}[x/a] ⊧ F

where ℑ_{S}[x/a] is like ℑ_{S} except that it maps x to a. It should be clear that the sorted semantics and the semantics given by the relativization rules are equivalent with respect to sentences.

3 Standard Unification

For the standard case a lot of efficient unification procedures are known, e.g. [19, 17, 2]. For reasons of simplicity we will present a rule based version of the Robinson [20] unification procedure following [17]. We use the standard notions for unification [23].

Definition 3.1 (Notions for Unification) A substitution σ is called a matcher from s to t if sσ = t, where s and t are two expressions (terms, atoms, literals). t and s are called unifiable, iff there exists a substitution σ such that tσ = sσ. In this case the substitution σ is called a unifier of t and s. A unifier σ of two expressions t and s is called an mgu (most general unifier), iff for every unifier λ of t and s there exists a substitution τ, such that στ = λ. If t and s are two expressions, then Γ = {t = s} is called the unification problem for t and s. A substitution σ solves

Tautology  \frac{x = x ∪ Γ}{Γ}

Decomposition \frac{\{f(t_{1}, …, t_{n}) = f(s_{1}, …, s_{n})\} ∪ Γ}{\{t_{1} = s_{1}, …, t_{n} = s_{n}\} ∪ Γ}

Application \frac{\{x = t\} ∪ Γ}{\{x = t\} ∪ Γ\{x ↦ t\}}

if x is a variable, x ∉ V(t), and x ∈ V(Γ)

Orientation \frac{\{t = x\} ∪ Γ}{\{x = t\} ∪ Γ}

if x is a variable and t a non-variable term

Clash \frac{\{f(t_{1}, …, t_{n}) = g(s_{1}, …, s_{m})\} ∪ Γ}{STOP.FAIL}

if f ≠ g

Cycle

\frac{\{x = t\} ∪ Γ}{STOP.FAIL}

if x ∈ V(t)

Table 1: The Rules of Standard Unification

a unification problem Γ = {t_{1} = s_{1}, …, t_{n} = s_{n}}, iff t_{1}σ = s_{1}σ, …, t_{n}σ = s_{n}σ. A unification problem Γ is called solved, iff Γ = {x_{1} = t_{1}, …, x_{n} = t_{n}} where the x_{i} are variables, x_{i} ∉ V(t_{j}) and x_{i} ≠ x_{j} for every i and j.

Algorithm 3.2 (A Standard Unification Algorithm) The input of the algorithm is a unification problem Γ, which is changed by the following six rules until it is solved or the problem is found to be unsolvable:

If Γ = {t_{1} = s_{1}, …, t_{n} = s_{n}} is a unification problem, then the above unification algorithm always terminates on Γ. If the algorithm stops with failure there is no substitution σ solving Γ. Otherwise Γ is solved and the corresponding substitution σ is an idempotent mgu of the term pairs (t_{1}, s_{1}), …, (t_{n}, s_{n}).

Lemma 3.3 Let t, s be two unifiable, pseudo-linear terms. If s and t share variables, we assume that occurrences of common variables also have the same length. If σ is the mgu of s and t, then Depth(tσ) = max(Depth(s), Depth(t)). Proof: By induction on the number n of different variables occurring in s or t.

The base cases n = 0, n = 1 and n = 2 can be easily proved. Now assume n + 1 different variables. We apply exhaustively the rules Tautology, Decomposition, and Orientation to the unification problem Γ = {s = t} resulting in Γ′ = {x_{1} = t_{1}, …, x_{n} = t_{n}}. Let λ = {x_{1} ↦ t_{1}}, t′ = tλ, and s′ = sλ. Then max(Depth(s), Depth(t)) = max(Depth(s′), Depth(t′)) because s and t are pseudo-linear. In addition s′ and t′ are also pseudo-linear and contain n different variables. By induction hypothesis for the mgu τ of s′ and t′ we have Depth(t′τ) = max(Depth(s′), Depth(t′)). Thus from λτ = σ and the above we have Depth(tσ) = max(Depth(s), Depth(t)). □

4 Unification in Sort Theories

4.1 Conditional Well-Sorted Expressions

Definition 4.1 (Conditional Expressions) A pair (S(t), C) is called a conditional declaration (conditional term, conditional substitution) if C is a finite set of literals and S(t) a declaration (term, substitution). A conditional expression (t, C) is called ground if t is ground.

We always assume that the set L of conditional declarations is finite and all conditional declarations are variable disjoint. The set L is called a sort theory. All following notions and definitions refer to a fixed sort theory L.

Definition 4.2 (Conditional Well-Sorted Terms) The set of conditional wellsorted terms (abbreviated by cws. terms) T_{S} of sort S is recursively defined by:

(i) For every variable x ∈ V_{Σ} and every sort S ⊆ S(x), (x, ∅) ∈ T_{S}.

(ii) For every conditional declaration (S(t), C) ∈ L, (t, C) ∈ T_{S}. Note that there are only declarations for base sorts.

(iii) For every cws. term (t, C) ∈ T_{S} (S ≠ ⊤), substitution σ: = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}}, with (t_{i}, C_{i}) ∈ T_{S(x_{i})} for all i, (⋃_{i} C_{i}) ⊆ D for some finite set of literals D, (tσ, Cσ ∪ D) ∈ T_{S}.

(iv) For cws. terms (t, C_{i}) ∈ T_{S_{i}} (1 ≤ i ≤ n), finite set of literals D, (⋃_{i} C_{i}) ⊆ D, (t, D) ∈ T_{{S_{1},...,S_{n}}}.

(v) For every term t and finite set of literals D we have (t, D) ∈ T_{⊤}.

We define T_{S}^{∅}: = {(t, ∅) | (t, ∅) ∈ T_{S}}. T_{S,gr} is the restriction of T_{S} to ground terms. A sort S is called empty if there is no cws. ground term (t, C) ∈ T_{S}, or equivalently if T_{S,gr} = ∅. We always have T_{S}^{∅} ⊆ T_{S} and T_{S,gr} ⊂ T_{S}.

For the unification algorithm it is useful to define a binary relation ⊑ which denotes the subsort relationship. If S and T are sorts, then we define S ⊑ T iff there exists a variable x with S(x) = S and x ∈ T_{T}. Note that if there exists one variable x ∈ T_{T} there are infinitely many variables of sort S in T_{T}. The relation S ⊑ T implies T_{S} ⊆ T_{T}. In addition, we have t ∈ T_{{S,T }} iff t ∈ T_{S} and t ∈ T_{T} for two arbitrary sorts S, T.

Sometimes we are not interested in the condition part of a conditional expression. We say that t ∈ T_{S} if there is a set of literals C such that (t, C) ∈ T_{S}. Similarly we say that a declaration S(t) ∈ L if there is a set of literals C such that (S(t), C) ∈ L. If not necessary or if the conditional part is the empty set we do not mention the conditional part of a conditional expression.

Example 4.3 (Conditional Well-Sorted Terms) Consider the sort theory

L = {(S(a), {P (a)}), (S(y), {Q(y)}), T (a), T (f(x))}

If a conditional declaration (term) has an empty conditional part only the term is written. It is assumed throughout this example that S(x_{i}) = S and S(y_{i}) = T. Now Definition 4.2 is applied. The case (i) gives

\begin{aligned}T_{S} & ⊃ & \{x_{1}, x_{2}, …, z_{1}, z_{2}, …\} \\ T_{T} & ⊃ & \{y_{1}, y_{2}, …, z_{1}, z_{2}, …\} \\ T_{\{S,T \}} & ⊃ & \{z_{1}, z_{2}, …\} \end{aligned}

with S(z_{i}) = {S, T }. Case (ii) of Definition 4.2 extends the sets by terms occurring in the declarations:

\begin{aligned}T_{S} & ⊃ & \{(a, \{P (a)\}), (y, \{Q(y)\})\} \\ T_{T} & ⊃ & \{a, f(x)\} \end{aligned}

Now case (iii) can be applied. We have (y, {Q(y)}) ∈ T_{S}. For both substitutions σ = {y ↦ a} and τ = {y ↦ f(x)} the components are well-sorted, i.e. a ∈ T_{T} and f(x) ∈ T_{T}. T_{S} is extended by the new terms (yσ, {Q(y)σ}) and (yτ, {Q(y)τ}) :

T_{S} ⊃ {(a, {Q(a)}), (f(x), {Q(f(x))})}

Now all terms in T_{S} can be substituted for x in f(x) ∈ T_{T}:

T_{T} ⊃ {(f(a), {P (a)}), (f(a), {Q(a)}), (f(y), {Q(y)})}

This process can be continued infinitely many times. Applying case (iv) using the occurrences of f(a) in T_{S} and T_{T} we get:

T_{{S,T }} ⊃ {(f(a), {P (a), Q(a), Q(f(a))}), (f(a), {Q(a), Q(f(a))})}

Case (v) means that an arbitrary conditional term is included in T_{⊤}. The sorts S, T and {S, T } are not empty and

\begin{aligned}T_{S}^{∅} & = & \{x_{i}, z_{i}\} \\ T_{T}^{∅} & = & \{y_{i}, z_{i}, a, f(x_{i})\} \end{aligned}

Depending on the declarations occurring in L the following theories are distinguished. L is called elementary if every term declaration is a function declaration. L is called semi-linear if every term occurring in a term declaration is semi-linear and there are no cycles with respect to ⊑. L is called pseudo-linear if every term occurring in a term declaration is pseudo-linear. L is called regular if all subsort declarations have an empty condition part, ⊑ is a partial ordering and every term t has a unique least sort with respect to ⊑. Note that this notion is called preregular by Goguen and Meseguer [14].

Lemma 4.4 (Soundness of Cws. Terms) Let L = {(S_{1}(t_{1}), {K_{1,1}, …, K_{1,n_{1}}}), …, (S_{m}(t_{m}), {K_{m,1}, …, K_{m,n_{m}}})} be a sort theory. For every interpretation ℑ_{S} with ℑ_{S} ⊧ ∀(S_{1}(t_{1}) ∨ K_{1,1} ∨ … ∨ K_{1,n_{1}}) ∧ … ∧ ∀(S_{m}(t_{m}) ∨ K_{m,1} ∨ … ∨ K_{m,n_{m}}) and every cws. term (t, {L_{1}, …, L_{k}}) ∈ T_{S}, S ≠ ⊤, S = {S_{1}, …, S_{n}}, we have ℑ_{S} ⊧ ∀((S_{1}(t) ∧ … ∧ S_{n}(t)) ∨ L_{1} … ∨ L_{k}). Proof: By structural induction according to Definition 4.2. □

Lemma 4.5 (Completeness of Cws. Terms) Let L be a sort theory where all declarations have an empty condition part, whence T_{S} = T_{S}^{∅} for every sort S. Then ℑ_{S}^{gr} given by ℑ_{S}^{gr}(S) = T_{S,gr} for all base sorts S is the initial model in the family of all L models and ℑ_{S}^{fr} given by ℑ_{S}^{fr}(S) = T_{S} is the free model in the family of all L models. Proof: Straightforward extension of the proof given by Schmidt-Schauß [22]. □

Definition 4.6 (Conditional Well-Sorted Substitutions) A conditional substitution σ^{c} = (σ, C) is called conditional well-sorted if for every x_{i} ∈ DOM(σ), there is a cws. term (x_{i}σ, C_{i}) ∈ T_{S(x_{i})} and (⋃_{i} C_{i}) ⊆ C.

A cws. renaming σ^{c} = (σ, ∅) is a cws. substitution such that COD(σ) consists of variables only, σ is injective on DOM(σ) and S(x) = S(xσ) for all x ∈ DOM(σ).

The composition of two well-sorted substitutions can be computed by τ^{c}σ^{c}: = (τσ, Kσ∪C), where σ^{c} = (σ, C), τ^{c} = (τ, K). The result of the composition is again a cws. substitution. Thus the set of all cws. substitutions builds a monoid. The set of all conditional well-sorted substitutions is denoted by SUB. A cws. substitution σ^{c} ∈ SUB is called empty iff there exists no λ^{c} ∈ SUB such that σ^{c}λ^{c} is a ground substitution.

Example 4.7 (Conditional Well-Sorted Substitutions) Again we consider the sort theory of Example 4.3, S(x_{i}) = S, S(y_{i}) = T:

L = {(S(a), {P (a)}), (S(y), {Q(y)}), T (a), T (f(x))}

The two substitutions σ and τ are cws. substitutions:

\begin{aligned}σ^{c} & = & \{y_{1} ↦ a\} \\ τ^{c} & = & (\{y ↦ f(y_{1})\}, \{Q(y_{1})\}) \end{aligned}

Note that these substitutions would be also cws. if the conditional part is extended by additional literals. The composition τσ is

τ^{c}σ^{c} = ({y ↦ f(a), y_{1} ↦ a}, {Q(a)})

Definition 4.8 Let s^{c} = (s, C), t^{c} = (t, K) be two cws. terms. Then

(i) s^{c} ≥_{L} t^{c} iff there exists (σ, D) ∈ SUB such that s = tσ and (Kσ ∪ D) ⊆ C. In this case we call (σ, D) an instantiating substitution of t^{c} to s^{c} and we call s^{c} an L-instance of t^{c}.

(ii) s^{c} ≡_{L} t^{c} iff s^{c} ≥_{L} t^{c} and t^{c} ≥_{L} s^{c}.

As ≥_{L} is a quasi-ordering on cws. terms the relation ≡_{L} is an equivalence relation.

Lemma 4.9 For every sort S ∈ 2^{S_{Σ}}, S ≠ ⊤, S = {S_{1}, …, S_{n}}, and every nonvariable term s^{c} ∈ T_{S} there exist term declarations (S′_{i}(t_{i}), C_{i}) ∈ L with S′_{i} ⊑ S_{i} and a cws. substitution (σ, D) ∈ SUB such that (t_{i}σ, (⋃ C_{i})σ ∪ D ∪ Eσ) ≤_{L} s^{c} for all i, where E is the set of conditions coming from the subsort declarations which establish S′_{i} ⊑ S_{i}. Proof: By structural induction using Definition 4.2 and the fact that SUB is a monoid. □

Lemma 4.10 Let t be a term and let S ≠ ⊤ be a sort.

(i) There exists a finite set of cws. terms Cond(t, S) = {(t, C_{1}), …, (t, C_{n})} with (t, C_{i}) ∈ T_{S} for all i and for each cws. term (t, C) ∈ T_{S} there is a term (t, C_{i}) ∈ Cond(t, S) with (t, C) ≥_{L} (t, C_{i}).

(ii) There exists a finite set of cws. ground terms Cond(S) = {(t_{1}, C_{1}), …, (t_{n}, C_{n})} with (t_{i}, C_{i}) ∈ T_{S} for all i and for each cws. ground term (t, C) ∈ T_{S} there is a ground term (t_{i}, C_{i}) ∈ Cond(S) and a cws. renaming σ^{c} = (σ, ∅) with C_{i}σ ⊆ C.

Proof:

(i) By induction on the structure of terms. If t is a constant and (t, C) ∈ T_{S}, for an arbitrary set of literals C, then by Lemma 4.9 there are term declarations in L which can be used to build a more general term than (t, C). As L is finite there are only finitely many different terms. If t is a variable, then S(t) ⊑ S. As there are only finitely many subsort declarations in L the set Cond(t, S) is finite. If t is a compound term, Lemma 4.9 and fact that L is finite can be used again and the induction hypothesis is applied to the components of σ (see Lemma 4.9). (ii) The set exists because L is finite, the sets of ground terms are recursively enumerable and the subset ordering modulo renaming is well founded on finite sets of literals. □

There exists no effective algorithm for the computation of common ground terms for two base sorts. The question whether two base sorts share a common ground term is undecidable in general [22]. The set Cond(S) is effectively computable for base sorts if the sorts of all variables occurring in {x | x ∈ V(t), (S(t), C) ∈ L} are base sorts. In this case the time complexity of computing Cond(S) for all base sorts is at most O(m^{3} ∗ k) where m = |L| and k = max({|C| | (S(t), C) ∈ L}). The idea is to start with all ground declarations and collect the conditions and ground terms for the respective sorts. These sorts are non-empty with respect to the conditions. Then this result is propagated recursively to all declarations where all sorts attached to the variables in the declaration are already known non-empty. The corresponding conditions are collected, ground terms built, and using the subset relationship redundant sets of conditions can be removed. The cardinality of the maximal non-redundant set of conditions is bound by m ∗ k and for the search and propagation we need at most m^{2} steps.

As every term has top sort ⊤, Cond(t, ⊤) = {t} and Cond(⊤) = {a} for an arbitrary constant a. In addition, sort computation is trivial for sort ⊤.

Example 4.11 Again we consider the sort theory of Example 4.3,

L = {(S(a), {P (a)}), (S(y), {Q(y)}), T (a), T (f(x))}

Then examples for Cond(t, S) are

Cond(f(a), T) = {(f(a), {Q(a)}), (f(a), {P (a)})}
Cond(f(x), T) = {f(x)}
Cond(f(x), S) = {(f(x), {Q(f(x))})}

and the sets Cond(S) and Cond(T) are

Cond(T) = {a}
Cond(S) = {(a, {P (a)}), (a, {Q(a)})}

Algorithm 4.12 (Sort Computation) Let t be a term and S ≠ ⊤ a sort. Then t ∈ T_{S} with S = {S_{1}, …, S_{n}} iff there exist sorts T_{i} ∈ Sorts(t) with T_{i} ⊑ S_{i} for all i. The function Sorts can be computed as follows:

(i) if t is a variable, then Sorts(t) = {S(t)}

(ii) if t is a constant, then Sorts(t) = {S | S(t) ∈ L}

(iii) if t is a compound term f(t_{1}, …, t_{n}), then Sorts(t) = {S | S(f(s_{1}, …, s_{n})) ∈ L, there exists a standard matcher σ with f(s_{1}, …, s_{n})σ = f(t_{1}, …, t_{n}) and for each component x_{i} ↦ t′_{i} of σ, S(x_{i}) = {S_{1}, …, S_{n}} there are sorts T_{i} ∈ Sorts(t′_{i}) with T_{i} ⊑ S_{i}}

The above algorithm can also be used to answer queries of the form t ∈ T_{S}^{∅} by only considering declarations with empty condition part.

The time complexity of the algorithm for a query t ∈ T_{S} is at most O(n^{2} ∗ m) where n = Size(t) and m = |L|. The idea is to start with the computation of the sorts of subterms of depth 0 and then successively continue for subterms with depth greater 0. Schmidt-Schauß [22] proved that sort computation is quasi-linear. His result doesn’t subsume our result because Schmidt-Schauß considered constant time for all operations concerning the sort theory. This was reasonable because his sort theory is a static part of the signature. In the approach presented here the theory typically changes during deduction, if sorted unification is applied to a calculus (see Section 6).

Example 4.13 (Sort Computation) The query f(f(x_{1})) ∈ T_{S} is answered with respect to the sort theory of Example 4.3 (S(x_{i}) = S, S(y_{i}) = T):

L = {(S(a), {P (a)}), (S(y), {Q(y)}), T (a), T (f(x))}

Depth(x_{1}) = 0 thus the sort computation is started with x_{1}. As we have S(x_{1}) = S the result for x_{1} is

Sorts(x_{1}) = {S}

Following case (i) of Definition 4.12 the term f(x_{1}) is the only term of depth 1. The only applicable declaration (case (iii)) is T (f(x)) with standard matcher σ = {x ↦ x_{1}}. Of course we have S ∈ Sorts(x), whence

Sorts(f(x_{1})) = {T }

For f(f(x_{1})) again declaration T (f(x)) with standard matcher σ = {x ↦ f(x_{1})} can be used. We have T ∈ Sorts(f(x_{1})) and T ⊑ S, because (S(y), {Q(y)}) ∈ L.

Sorts(f(f(x_{1}))) = {T }

Now we know that f(f(x_{1})) ∈ T_{S} because T ⊑ S.

Definition 4.14 Let W ⊆ V_{Σ} and σ^{c} = (σ, C), τ^{c} = (τ, K), σ^{c}, τ^{c} ∈ SUB

(i) σ^{c} ≥_{L} τ^{c}[W] iff there exists a λ^{c} = (λ, D) ∈ SUB with xσ = xτλ for all x ∈ W and (Kλ ∪ D) ⊆ C In this case we call λ^{c} an instantiating substitution of τ^{c} to σ^{c} and we call σ^{c} an L-instance of τ^{c} modulo W.

(ii) σ^{c} ≡_{L} τ^{c} iff σ^{c} ≥_{L} τ^{c} and τ^{c} ≥_{L} σ^{c}.

4.2 Unification Theory

We shortly recall the basic notions of unification theory [23] for the case of sort theories. Let Γ be a unification problem. A cws. substitution σ^{c} = (σ, C) solves Γ iff for every equation (s = t) ∈ Γ we have sσ = tσ. σ^{c} is called a cws. unifier of Γ. The set of all unifiers of Γ is written U_{L}(Γ), which is a left ideal in the substitution monoid SUB, since U_{L}(Γ) = SUB ∘ U_{L}(Γ).

We define the complete set of unifiers called cU_{L}(Γ) of a unification problem Γ as a set of cws. unifiers satisfying

(i) cU_{L}(Γ) ⊆ U_{L}(Γ) (correctness)

(ii) ∀δ^{c} ∈ U_{L}(Γ) ∃σ^{c} ∈ cU_{L}(Γ) : δ^{c} ≥ σ^{c}[V(Γ)] (completeness)

The base set μU_{L}(Γ), called the set of most general unifiers, is defined as a complete set of unifiers satisfying in addition

(iii) ∀σ^{c}, τ^{c} ∈ cU_{L}(Γ) : if σ^{c} ≥ τ^{c}[V(Γ)] then σ^{c} = τ^{c} (minimality)

Based on the cardinality of μU, we can classify sort theories according to the following unification hierarchy. A sort theory L is of type:

unitary if μU_{L}(Γ) exists and has at most one element for

all unification problems Γ

finitary if μU_{L}(Γ) exists and is finite for all unification

problems Γ

infinitary if μU_{L}(Γ) exists and is infinite for some unification

problem Γ

nullary if μU_{L}(Γ) does not exist for some unification problem Γ

4.3 The Sorted Unification Algorithm

Definition 4.15 (Notions for Sorted Unification) In order to define sorted unification, we have to extend Definition 3.1. A unification problem Γ = {x_{1} = t_{1}, …, x_{n} = t_{n}} is called sorted solved if Γ is solved and for every variable x_{i} we have t_{i} ∈ T_{S(x_{i})}.

Lemma 4.16 The ordering ≥_{L} [W] is well founded on SUB for a finite set of variables W. Proof: We have to show that there are no infinite chains of cws. substitutions (σ_{1}, C_{1}) >_{L} (σ_{2}, C_{2}) >_{L} … Choose a weight function w: Σ → IN such that w(S) > w(T) if S ⊏ T or S ⊏^{∅} T for sorts S, T ∈ 2^{S_{Σ}}, w(x): = w(S(x)) for all variables x ∈ V_{Σ}, w(f): = max{w(S) | S ∈ 2^{S_{Σ}}} + 1 for all f ∈ F_{Σ}. The relation ⊏^{∅} is the restriction of ⊏ to subsort declarations with an empty condition part. Note that S ⊏^{∅} T implies S ⊏ T or S ≡ T. As L and 2^{S_{Σ}} are finite the relation ⊏ is well founded, therefore the function w always exists. w may assign arbitrary natural numbers to predicate symbols. w can be extended to terms, literals, and sets of such expressions by w(f(t_{1}, …, t_{n})): = w(f) + ∑_{i} w(t_{i}) and w({E_{1}, …, E_{n}}): = ∑_{i} w(E_{i}). The weight of a cws. substitution is defined as w((σ, C)): = w(DOM(σ)) + w(COD(σ)) + w(C).

Now we show (σ, C) >_{L} (τ, D) implies w((σ, C)) > w((τ, D)). Wlog. we assume DOM(σ) ⊆ W, DOM(τ) ⊆ W and thus DOM(σ) = DOM(τ). If (σ, C) >_{L} (τ, D) either |C| > |D| or some subterms in C or COD(σ) are replaced by variables in D or COD(τ), respectively, or some variables in C or COD(σ) are replaced by more general variables in D or COD(τ), respectively. All these cases imply w((σ, C)) > w((τ, D)). As the sets COD(σ), COD(τ), C, D, W are all finite, we conclude ≥_{L} [W] is well founded. □

As a consequence of Lemma 4.16 we have that for every finite set Γ of equations, there exists a minimal, complete set of unifiers μU_{L}(Γ).

Algorithm 4.17 (The Sorted Unification Algorithm) The input of the algorithm is a unification problem Γ, which is changed by four sorted rules (see Table 2) and the six standard rules of Algorithm 3.2 (see Table 1) until it is sorted solved or no rule is applicable or the problem is found to be unsolvable.

In order to compute a cws. substitution from a sorted solved unification problem, we have to do the following. Let Γ = {x_{1} = t_{1}, …, x_{n} = t_{n}} be the sorted solved unification problem, then σ: = {x_{1} ↦ t_{1}, …, x_{n} ↦ t_{n}} is the corresponding unifier. σ^{c}: = (σ, C) is a cws. mgu if we have (t_{i}, C_{i}) ∈ T_{S(x_{i})} for all i and C = ⋃_{i} C_{i}. Thus from a sorted solved unification problem we may compute several (but only finitely many, see Lemma 4.10) cws. mgu’s.

As the sorted unification algorithm is an extension of the standard unification algorithm with the sorted rules, every sorted unifier is a standard instance of the standard unifier. This was pointed out by Schmidt-Schauß [22] already. Frisch and Cohn used this insight for a more abstract presentation of sorted unification [12].

Note that the unification algorithm unifies terms with respect to all cws. substitutions, including empty substitutions. Thus the problem of empty sorts is separated from the unification problem.

Lemma 4.18 (Soundness of the Unification Algorithm) If the unification algorithm computes a cws. mgu σ^{c} for a unification problem Γ, then σ^{c} solves Γ. Proof: Can be easily proved for the rules. The proof is done by showing that every cws. substitution solving the problem after the application of a rule solves the original problem. □

Lemma 4.19 (Completeness of the Unification Algorithm) If λ^{c} is a cws. substitution which solves Γ, then the unification algorithm computes a cws. mgu σ^{c} which solves Γ and λ^{c} ≥_{L} σ^{c}[V(Γ)].

Sorted Fail \frac{\{x = f(t_{1}, …, t_{n})\} ∪ Γ}{STOP.FAIL}

if x ∉ V(f(t_{1}, …, t_{n})), f(t_{1}, …, t_{n}) ∉ T_{S(x)}, S(x) = {S_{1}, …, S_{n}} and there are no conditional declarations S′_{i}(f(s_{i,1}, …, s_{i,n})) ∈ L, S′_{i} ⊑ S_{i}

Subsort  \frac{\{x = y\} ∪ Γ}{\{y = x\} ∪ Γ} ; if x ∈ T_{S(y)} and y ∉ T_{S(x)}^{∅}

Common Subsort

\frac{\{x = y\} ∪ Γ}{\{x = z\} ∪ \{y = z\} ∪ Γ} ; if x ∉ T_{S(y)}^{∅}, y ∉ T_{S(x)}^{∅}, and S(z) = S(x) ∪ S(y)

Weakening \frac{\{x = f(t_{1}, …, t_{n})\} ∪ Γ}{\{x = f(s_{1,1}, …, s_{1,n})\} ∪ \{t_{1} = s_{i,1}, …, t_{n} = s_{i,n}\} ∪ Γ}

if x ∉ V(f(t_{1}, …, t_{n})), f(t_{1}, …, t_{n}) ∉ T_{S(x)}^{∅}, S(x) = {S_{1}, …, S_{n}} and for each S_{i} there is a conditional declaration S′_{i}(f(s_{i,1}, …, s_{i,n})) ∈ L, S′_{i} ⊑ S_{i}

Table 2: The Sorted Rules of Sorted Unification Proof: Let σ^{c} = (σ, C) be an idempotent most general unifier, i.e. σ^{c} ∈ μU_{L}(Γ) with DOM(σ) = V(Γ). For the proof we will split Γ into two disjoint parts: Γ_{U} and Γ_{WO}. Γ_{U} contains the unsolved equations and is initialized with Γ. Γ_{WO} contains the worked off equations, i.e. equations already processed by the rules of the unification algorithm. Γ_{WO} is initialized with the empty set.

As well-founded complexity measure μ(σ, Γ) we use the multiset of all term depths in Γ_{U} σ. The idea of the proof is to show that there exists a pair (σ′, Γ′), such that Γ can be transformed into Γ′ by one step of the unification algorithm and σ′ is a mgu of Γ′ that is equal to σ on old variables and extends σ to new variables, furthermore μ(σ′, Γ′) < μ(σ, Γ).

If μ(σ′, Γ′) is minimal, i.e. Γ_{U} = ∅, then the set of equations is sorted solved and we are ready. It should be clear that in this case Γ_{WO} is sorted solved and by using Lemma 4.10 we can compute the desired mgu by restricting the domain of σ′ to V(Γ).

Now we show that there is always a step of the unification algorithm that reduces the measure μ(σ, Γ). First we argue that the rule Application (see Algorithm 3.2) does not increase the measure. The rule does not change the depths of terms is Γσ, since from xσ = tσ we obtain σ{x ↦ t} = σ, since σ is idempotent.

We go through the cases for equations s = t in Γ_{WO}:

(i) Case s = t, where neither s nor t is a variable. Then by step Decomposition we reduce μ(σ, Γ) without changing the set of solutions.

(ii) Case x = f(t_{1}, …, t_{n}). Then x ∉ V(f(t_{1}, …, t_{n}) because xσ = f(t_{1}, …, t_{n})σ. If xσ = f(t_{1}, …, t_{n}), then we have f(t_{1}, …, t_{n}) ∈ T_{S(x)}, move the equation to Γ_{WO} and are done. If xσ ≠ f(t_{1}, …, t_{n}) then f(t_{1}, …, t_{n}) ∉ T_{S(x)}^{∅} as σ is an idempotent mgu of Γ. Let S(x) = {S_{1}, …, S_{n}}. By Lemma 4.9 there exist declarations S′_{i}(f(s_{i,1}, …, s_{i,n})) with S′_{i} ⊑ S_{i} and substitution τ^{c} = (τ, E) with f(s_{i,1}, …, s_{i,n})τ = f(t_{1}, …, t_{n})σ. We use the rules Weakening, Decomposition, Orientation and Application to obtain a new equation system Γ′. Since the equation x = f(s_{1,1}, …, s_{1,n}) is sorted solved, we have μ(σ ∪ τ, Γ′) < μ(σ, Γ), since the depth of f(t_{1}, …, t_{n})σ is larger than all term depths of t_{j}σ and s_{i,j}τ. Furthermore σ ∪ τ is a solution of Γ′ with σ ∪ τ = σ[V(Γ)].

(iii) Case x = y. If xσ = y or yσ = x we can shift the equation to Γ_{WO} after applying rule Subsort if necessary. If this is not possible we apply rule Common Subsort and move the sorted solved equations x = z and y = z to Γ_{WO}. With τ = {z ↦ xσ} we have μ(σ ∪ τ, Γ′) < μ(σ, Γ) and σ ∪ τ = σ[V(Γ)]

□

Example 4.20 (Infinitely Many mgu’s) Consider the following sort theory L and unification problem Γ, where S(x_{i}) = S:

\begin{aligned}L & = & \{S(g(g(x))), S(g(a)), S(a)\} \\ Γ & = & \{x_{1} = g(x_{2})\} \end{aligned}

We have T_{S} = {g(g(x)), g(a), a, g^{i}(a), g^{2i}(x), x_{i}} with i ≥ 2. Now we apply the rules of sorted unification. Γ is standard solved but not sorted solved because g(x_{2}) ∉ T_{S}. The only applicable rule is Weakening using the declarations S(g(g(x_{3}))) and S(g(a)) resulting in the two unification problems

\begin{aligned}Γ_{1} & = & \{x_{1} = g(g(x_{3})), x_{2} = g(x_{3})\} \\ Γ_{2} & = & \{x_{1} = g(a), x_{2} = a\} \end{aligned}

respectively. Γ_{2} is sorted solved because {g(a), a} ⊆ T_{S}. Γ_{1} is not sorted solved because g(x_{3}) ∉ T_{S}. Again only rule Weakening using the declarations S(g(g(x_{4}))) and S(g(a)) is applicable. The two new unification problems after the application of standard unification (see Algorithm 3.2) are

\begin{aligned}Γ_{3} & = & \{x_{1} = g(g(g(x_{4}))), x_{2} = g(g(x_{4})), x_{3} = g(x_{4})\} \\ Γ_{4} & = & \{x_{1} = g(g(a)), x_{2} = g(a), x_{3} = a\} \end{aligned}

respectively. Γ_{4} is sorted solved because {g(g(a)), g(a), a} ⊆ T_{S}. Γ_{3} is not sorted solved because g(x_{4}) ∉ T_{S}. The algorithm stucks in a cycle. Rule Weakening can be further applied always leading to a solved problem using S(g(a)) and an unsolved problem containing an equation of the form x_{i} = g(x_{i+1}) using S(g(g(x))) renamed. The example demonstrates that unification in sort theories may lead to infinitely many mgu’s.

Lemma 4.21 (Properties of L-Unification)

(i) L-Unification is of unification type infinitary.

(ii) If L is elementary then L-Unification is decidable and of unification type finitary. In addition L-Unification is NP-complete and the number of unifiers may grow exponentially with the size of terms to be unified.

Proof: (i) The set μU_{L}(Γ) exists for every finite set Γ of equations and finite set L of conditional declarations (Lemma 4.16). Example 4.20 shows a sort theory and a unification problem such that μU_{L}(Γ) is infinite. Note that the above sort theory L is not elementary (because S(g(g(x))) ∈ L) but linear (therefore pseudo-linear). (ii) The only crucial rule of sorted unification concerning termination and decidability is the rule Weakening. Assume that the rule is applied to an equation x = t occurring in the standard solved unification problem Γ. After the application of Weakening again standard unification is performed. Let t_{i} be the terms resulting from the application of Weakening and standard unification to x = t. As L is elementary and because of Lemma 3.3 we have Depth(t) > Depth(t_{i}) or a variable occurring non-pseudo-linear in t is removed. As t contains only finitely many variables the number of terms generated by the Weakening rule is finite. Thus L-unification is decidable and of unification type finitary for elementary sort theories.

NP-completeness can be shown in the same way than for the sorted unification algorithm of Schmidt-Schauß [22]. The idea is to reduce the satisfiability problem of propositional logic to L-unification. This gives also examples where the number of unifiers may grow exponentially in the size of terms to be unified. □

The result on elementary theories is not new. Schmidt-Schauß [22] showed unification in elementary sort theories to be decidable but infinitary due to his weaker sort language. Uribe [26] gave an algorithm which computes at most finitely many solved forms for a given unification problem in a semi-linear sort theory. However, there is an important difference between our and Uribe’s approach. Our unification algorithm works in all cases whereas Uribe’s algorithm only works for semi-linear theories. Thus the result means we have an algorithm which works in any case and has the desired properties for the sub case of elementary sort theories.

Now a semi-decision algorithm for the computation of empty sorts is presented. The algorithm consists of two phases: a fast preprocessing phase there sorts are marked which can be easily detected to be non-empty and a processing phase there it is checked whether a specific sort is empty or not.

Algorithm 4.22 (Computation of Empty Sorts) The input of the algorithm Empty is a sort S = {S_{1}, …, S_{n}}. The algorithm returns True if S is empty and False otherwise. Preprocessing:

(i) For each ground declaration S(t) ∈ L, mark S to be non-empty.

(ii) For each declaration S′(t′) ∈ L where all sorts attached to variables in t′ are marked non-empty, mark S′ to be non-empty. Step (ii) is repeated until all declarations have been checked and no new sort is detected to be non-empty.

Processing:

(i) If S is marked to be non-empty then Empty(S) = False. If S is marked to be empty then Empty(S) = True.

(ii) If S = {S_{1}, …, S_{n}} and if there are conditional declarations S′_{i}(f(t_{i,1}, …, t_{i,n})) ∈ L, S′_{i} ⊑ S_{i} such that the f(t_{i,1}, …, t_{i,n}) are sorted unifiable with unifier σ and for all sorts T ∈ {S(x) | x ∈ V(COD(σ))} we have Empty(T) = False then Empty(S): = False and S is marked non-empty else Empty(S): = true and S is marked empty.

The algorithm is correct and complete which can be easily seen using Lemma 4.19, Lemma 4.18 and Lemma 4.10. If the marking is done by attaching the appropriate sets of conditions, the algorithm can also be used to compute the set of conditions which guarantees a sort to be non-empty. These conditions are needed if sorted unification is applied to a calculus (see Section 6). The time complexity of the preprocessing phase is at most O(n^{2}) where n = |L|. This phase has only to be computed once for a sort theory L. It decides the non-emptiness for all base sorts which only depend on declarations where only base sorts are attached to the variables occurring in the declarations.

Note that the second phase is recursive and is only a semi-decision algorithm if non-base sorts occur. There are several possibilities to show that the empty sort problem is undecidable. One possibility is to reduce it to Schmidt-Schauß’s empty sort problem which is known to be undecidable. Instead of checking whether {S_{1}, …, S_{n}} is empty we apply Schmidt-Schauß sorted unification to the unification problem Γ = {x_{1} = x_{2}, x_{2} = x_{3}, …, x_{n−1} = x_{n}} with S(x_{i}) = S_{i}. It is sufficient for the undecidability result to consider sort theories where only base sorts are attached to variables.

In addition Comon [6] pointed out that sort theories correspond to finite bottomup tree automaton. Using this relationship it can be shown that the empty sort problem is undecidable for pseudo-linear signatures [7, 3]. In order to show this result it is sufficient to consider non-linearities on the second level of a term. For semi-linear signatures Uribe [26] showed that the empty sort problem is decidable.

Example 4.23 (Computation of Empty Sorts) We apply Algorithm 4.22 to the the non-base sort {S, T } with respect to the sort theory

L = {(S(b), {P (a)}), (S(f(f(y_{2}))), {Q(y_{2})}), T (a), T (f(y_{1}))}

where S(y_{i}) = T. We compute Empty({S, T }). The preprocessing phase detects S and T to be non-empty using the declarations T (a) and S(b). Note that this does not imply {S, T } to be non-empty because the two terms a and b are different. Following case (ii) the only applicable declarations are S(f(f(y_{2}))) and T (f(y_{1})). The terms f(f(y_{2})) and f(y_{1}) have to be unified. The only cws. unifier is σ = {y_{1} ↦ f(y_{2})}. As we have Empty(T) = False, following case (i) we conclude Empty({S, T }) = False.

4.4 Examples for Sorted Unification

In the following we present more examples illustrating the different phenomena coming up with the sorted unification algorithm. First, we give an example with respect to a sort theory where all declarations have an empty condition part. Second, we target on the question of what happens if the condition part of declarations is not empty.

We start with the following elementary sort theory and unification problem Γ (S(x_{i}) = S, S(y_{i}) = T):

\begin{aligned}L & = & \{S(a), T (a), S(f(x)), T (f(y))\} \\ Γ & = & \{x_{1} = y_{1}\} \end{aligned}

We have

\begin{aligned}T_{S} & ⊃ & \{a, f^{i}(a), f^{i}(x_{j}), x_{i}, z_{i}\} \\ T_{T} & ⊃ & \{a, f^{i}(a), f^{i}(y_{j}), y_{j}, z_{i}\} \end{aligned}

where i, j ≥ 1 and S(z_{i}) = {S, T } . Applying the rule Common Subsort to Γ results in the following unification problem:

Γ_{1} = {x_{1} = z, y_{1} = z}

Problem Γ_{1} is sorted solved. Especially T_{{S,T }} contains infinitely many ground terms f^{i}(a). The example shows that we get one unifier where sorted approaches only considering base sorts compute infinitely many unifiers [22, 10].

The above sort theory doesn’t contain any conditional declarations, therefore T_{S} = T_{S}^{∅} for every sort S. The next sort theory contains a conditional declaration:

\begin{aligned}L & = & \{S(a), S(g(a)), (S(g(x)), \{P (x)\}), S(f(g(x)))\} \\ Γ & = & \{x_{1} = f(x_{2})\} \end{aligned}

Examples for cws. terms of sort S are:

\begin{aligned}T_{S} & ⊃ & {\{a, g(a), (g(x), \{P (x)\}),  f(g(x)),  f(g^{i}(x_{j})),  f(g^{i}(a)), \atop (f(g(g(x))), \{P (x)\}), (f(g^{3}(x)), \{P (x), P (g(x))\}), x_{j}\}} \\ T_{S}^{∅} & ⊃ & \{a, g(a), f(g(a)), f(g(g(a))), f(g(x_{j})), x_{j}\} \end{aligned}

where i > 1. The only applicable rule of sorted unification is Weakening

Γ_{1} = {x_{1} = f(g(x_{3})), x_{2} = g(x_{3})}

Γ_{1} is sorted solved yielding the cws. unifier

σ_{1} = ({x_{1} ↦ f(g(x_{3})), x_{2} ↦ g(x_{3})}, {P (x_{3})})

Nevertheless Weakening is still applicable to x_{2} = g(x_{3}) using the declaration S(g(a))

Γ_{2} = {x_{1} = f(g(x_{3})), x_{2} = g(a), x_{3} = a}

Γ_{1} is also sorted solved yielding the cws. unifier

σ_{2} = ({x_{1} ↦ f(g(a)), x_{2} ↦ g(a)}, ∅)

In fact μU_{L}(Γ) = {σ_{1}, σ_{2}} for the above sort theory L and unification problem Γ. The example shows that the rules of sorted unification are also applied to sorted solved unification problems until the problem is sorted solved with respect to T^{∅}.

4.5 Sorted Matching

A cws. substitution (σ, C) is called a cws. matcher from (t, D) to (s, E) if tσ = s and Dσ ∪ C = E. Sorted matching is decidable. Every cws. matcher is also a standard matcher. Therefore standard matching can be applied and then Lemma 4.10 can be used to check whether an appropriate set of conditions for the components of the matcher exists.

Sorted matching is the needed operation to decide subsumption, the most important reduction rule for resolution based calculi (see Section 6). As a cws. matcher may introduce new literals, for subsumption sorted matching is tested with respect to T^{∅}. In this case sorted matching is polynomially decidable, because first the standard matcher has to be computed and then each component is checked for conditional well-sortedness. Note that even if subsumption is checked with respect to T^{∅} it is more powerful than standard subsumption. Consider the following database of clauses Δ where S(x_{i}) = S and S(y_{i}) = T.

Δ:

(1) T (a)
(2) S(y)
(3) Q(x_{1}, y_{1})
(4) Q(y_{2}, a)

The sort theory L corresponding to these clauses consists of L = {T (a), S(y)} (for more details see Section 6). With respect to L, the clause (3) subsumes clause (4) with cws. matcher

σ = {x_{1} ↦ y_{2}, y_{1} ↦ a}

The standard formalization of Δ (see the relativization rules in Section 2) is Δ′

Δ′:
(1) T (a)
(2) ¬T (z) ∨ S(z)
(3) ¬S(z_{1}) ∨ ¬T (z_{2}) ∨ Q(z_{1}, z_{2})
(4) ¬T (z_{3}) ∨ Q(z_{3}, a)

where S(z_{i}) = ⊤, i.e. all variables are standard variables. In the standard formalization subsumption is not applicable.

5 Implementation of Sorted Unification

The sorted unification algorithm (Algorithm 4.17) is presented by a set of nondeterministic rules. This form is suitable to proof correctness and completeness of the algorithm but not for an implementation and further refinements. The rules have to be carefully investigated in order to solve the non-determinism and to obtain an efficient algorithm. The following observations have to be taken into account:

(i) The rules of standard unification are a subset of the rules.

(ii) The rule Subsort may be applicable infinitely many times to an equation.

(iii) The rules Subsort and Common Subsort may be both applicable to an equation.

(iv) Application of the rule Weakening may produce several new unification problems.

(v) An equation x = t may be solved, i.e. t ∈ T_{S(x)} but the sorted rules are still applicable to x = t.

(vi) If for an equation x = t we have t ∈ T_{S(x)}^{∅}, then none of the sorted rules is applicable.

(vii) Sorted unification is of unification type infinitary.

(i) means that we can split the sorted unification task into two subtasks. Standard unification which can be efficiently performed and application of the sorted rules. It is sufficient to apply rule Subsort at most once to an equation. Thus the application of rule Subsort may lead to at most two unification problems (ii). The rules Subsort and Common Subsort have to be checked independently if applied (iii). The algorithm needs to keep track of a set of unification problems (iv) and (ii). Whether an equation (a unification problem) is sorted solved has to be checked independently from the application of the sorted rules (v). well-sortedness with respect to T^{∅} is a sufficient condition for an equation not to be further processed (vi). The algorithm may not terminate (vii). Therefore we need some kind of resource bounding and the possibility to store and continue intermediate states of sorted unification.

The key to an efficient implementation is a good representation of a unification problem. In the theory this is just a set of equations. However, the above considerations show that this is not sufficient. The proof of Lemma 4.19 suggests an extended representation. A unification problem consists of a set Γ_{WO} of worked off equations and a set of Γ_{U} of unsolved equations. This representation allows for an additional mechanism, cycle checking. If an equation already worked off occurs again (modulo renaming) in Γ_{U} (for example after the application of Weakening), the unification algorithm loops. This means that either the actual unification problem can not be sorted solved or it produces infinitely many mgu’s. Checking for cycles allows to decide sorted unification in pseudo-linear sort theories (Lemma 5.4). In addition, the algorithm on empty sorts (Algorithm 4.22) can also be extended with cycle checking.

All theses considerations are implemented by the following algorithms. A unification problem is a pair (Γ_{WO}, Γ_{U} ). This representation allows to store and continue intermediate states. If a cycle is detected, the unification problem is suspended. If the corresponding equation could be solved by a different rule the unification problem is resumed (Algorithm 5.1 and line 6 of Algorithm 5.2). Resuming a suspended problem amounts to check whether the cycle still occurs even if the solved equations are disregarded. This is done by marking solved equations in Γ_{WO} and then checking for cycles with respect to unmarked equations. If such a cycle occurs the unification problem remains suspended. Otherwise is is resumed. The number of applications of the sorted rules is limited by the value of the input parameter Resource. The task of sorted unification is split into standard unification and sorted rule application. Sorted rule application is split into the processing of exactly one equation (Algorithm 5.2) and the general administration of all problems (Algorithm 5.3). These are divided into solved problems (PS), suspended problems (PP) and unsolved problems (PU).

We assume a unification algorithm for standard unification (see Definition 3.2). There are a lot of efficient unification algorithms known, e.g. see [2, 19, 17]. The standard unification algorithm is called “Standard Unification” and gets a unification problem Γ as input. The output is a pair (Δ, Value) where Value is either Solved or Fail and if Value is Solved, then Δ is the solved form of Γ (see Definition 3.1).

The algorithms are presented in an informal programming language. The bodies of If , While , and For statements are indicated by indentation. For example the body of the While loop in algorithm Sorted Unification consists of the lines three to sixteen. The Return statement immediately exits the function. The value of the function is the argument of the Return statement.

Algorithm 5.1 (Resume Suspended Problems(PP,Γ)) The input of the algorithm (see Table 3) is a set PP of suspended unification problems and a sorted solved set of equations Γ. The output is the set of problems which can be resumed because the equation which was the reason for the suspension is solved in Γ.

Algorithm 5.2 (Sorted Rule Application(Γ_{WO},Γ_{U} )) The input of the algorithm (see Table 4) is a set Γ_{WO} of worked off equations and a set Γ_{U} of unsolved equations.

Algorithm 5.3 (Sorted Unification(PU,PP,Resource)) The input of the algorithm (see Table 5) is a set PU of unsolved unification problems and a set PP of suspended unification problems. The third parameter Resource is an integer which limits the maximal number of applications of Sorted Rule Application before Sorted Unification terminates.

It can be easily seen that algorithm Sorted Unification is sound and complete. In its processing of unification problems it basically follows the ideas given in the proof of Lemma 4.19.

Resume Suspended Problems(PP,Γ)

1. Result: = ∅
2. For each pair (Γ_{WO}, Γ_{U} ) in PP Do

3. Mark all equations in Γ_{WO} which are renamed versions of equations in Γ.

4. If Γ_{U} does not contain an equation which occurs unmarked in Γ_{WO} modulo renaming Then Result: = Result ∪ {(Γ_{WO}, Γ_{U} )}

5. Return(Result)

Table 3: Algorithm Resume Suspended Problems

Lemma 5.4 (Properties of L-Unification) If L is pseudo-linear then L-Unification is decidable and of unification type infinitary. Proof: Example 4.20 shows a pseudo-linear theory with a unification problem that leads to infinitely many cws. mgu’s. The only crucial rule of sorted unification concerning termination and decidability is the rule Weakening. Assume that the rule is applied to an equation x = t occurring in standard solved unification problem Γ. After the application of Weakening using declarations S_{i}(t_{i}) standard unification is performed again. Let t′_{i} be the terms resulting from the application of Weakening and standard unification to x = t. As L is pseudo-linear we have max(Depth(t), Depth(t_{i})) ≥ Depth(t′_{i}) using Lemma 3.3 or a variable which occurs non-pseudo-linear in t is removed. If a variable occurring non-pseudo-linear is removed the number of non-pseudo-linear variable occurrences decreases for the t′_{i}. Whence the number of different terms modulo renaming that may be generated by the Weakening rule is finite, because there are only finitely many sort and function symbols in L and the maximal depth of generated terms is bound. Thus after a certain number of steps the unification problem is either solved or suspended. Therefore L-Unification is decidable for pseudo-linear sort theories. □

The following example shows that the algorithm Sorted Unification does not decide non-pseudo-linear sort theories. I conjecture sorted unification to be undecidable in general. This is not easy to prove because all techniques used so far rely on the empty sort problem. In this article the empty sort problem is separated from the unification problem.

Example 5.5 Consider the following sort theory and unification problem (S(x_{i}) = S):

Sorted Rule Application(Γ_{WO},Γ_{U} )

1. Result: = ∅

2. If Γ_{U} = ∅ Then Result: = {(Γ_{WO}, Γ_{U} , Solved)}, Return(Result)

3. Select an equation x = t from Γ_{U}

4. If rule Sorted Fail is applicable to x = t Then Result: = {(Γ_{WO}, Γ_{U} , Fail)}, Return(Result)

5. If t ∈ T_{S(x)}^{∅} Then Result: = {(Γ_{WO} ∪ {x = t}, Γ_{U} \ {x = t}, Unsolved)}, Return(Result)

6. If t is not a variable and t ∉ T_{S(x)} and x = t occurs in Γ_{WO} modulo renaming Then Result: = {(Γ_{WO}, Γ_{U} , Suspended)}, Return(Result)

7. If t ∈ T_{S(x)} then if t is not a variable or t is a variable and x ∉ T_{S(t)}^{∅} Then Result: = {(Γ_{WO} ∪ {x = t}, Γ_{U} \ {x = t}, Unsolved)}

8. If rule Subsort is applicable to x = t Then Result: = Result ∪ {(Γ_{WO} ∪ {t = x}, Γ_{U} \ {x = t}, Unsolved)}

9. If rule Common Subsort is applicable to x = t Then Result: = Result ∪ {(Γ_{WO}∪{x = z, t = z}, Γ_{U} \{x = t}, Unsolved)} where S(z) = S(x)∪S(t)

10. If rule Weakening is applicable to x = t where t = f(t_{1}, …, t_{n}) Then Result: = Result ∪ {(Γ_{WO} ∪ {x = t}, Γ_{U} \ {x = t} ∪ {t_{1} = s_{i,1}, …, t_{n} = s_{i,n}}, Unsolved)}

11. Return(Result)

Table 4: Algorithm Sorted Rule Application Sorted Unification(PU,PP,Resource)

1. PS: = ∅
2. While PU ≠ ∅ and Resource > 0 Do
3.  Select a pair (Γ_{WO}, Γ_{U} ) from PU
4.  PU: = PU \ {(Γ_{WO}, Γ_{U} )}
5.  (Γ_{U} , Value): = Standard Unification(Γ_{U} )
6.  If Value = Solved Then
7.  Resource: = Resource − 1
8.  Result: =Sorted Rule Application(Γ_{WO}, Γ_{U} )
9.  For each triple (Γ′_{WO}, Γ′_{U} , Value) in Result Do

10. If Value = Solved Then PS: = PS ∪ {Γ′_{WO}}

11. If Value = Unsolved Then PU: = PU ∪ {(Γ′_{WO}, Γ′_{U} )} 12. If Value = Suspended Then PP: = PP ∪ {(Γ′_{WO}, Γ′_{U} )}

13.  For each problem Γ in PS Do

14. Result: = Resume Suspended Problems(PP,Γ)

15. PU: = PU ∪ Result

16. PP: = PP \ Result

17. For each unification problem Γ in PS Do
18.  (Γ′, Value): =Standard Unification(Γ)
19.  If Value = Solved Then replace Γ in PS by Γ′
20. Return(PS, PU, PP)

Table 5: Algorithm Sorted Unification

\begin{aligned}L & = & \{S(f(x_{1}, f(g(x_{1}), x_{2}))), S(g(x_{1}))\} \\ Γ & = & \{x_{3} = f(g(x_{4}), x_{5})\} \end{aligned}

Applying Sorted Unification({(∅, {x_{3} = f(g(x_{4}), x_{5})})},∅,n) results in the following values of the variables Γ_{WO} and Γ_{U} after the call of Standard Unification at line 5.

1. Γ_{WO} = ∅
Γ_{U} = {x_{3} = f(g(x_{4}), x_{5})}
2. Γ_{WO} = {x_{3} = f(g(x_{4}), x_{5})}
Γ_{U} = {x_{6} = g(x_{4}), x_{5} = f(g(g(x_{4})), x_{7})}
3. Γ_{WO} = {x_{3} = f(g(x_{4}), x_{5}), x_{6} = g(x_{4})}
Γ_{U} = {x_{5} = f(g(g(x_{4})), x_{7})}
4. Γ_{WO} = {x_{3} = f(g(x_{4}), x_{5}), x_{6} = g(x_{4}), x_{5} = f(g(g(x_{4})), x_{7})}
Γ_{U} = {x_{8} = g(g(x_{4})), x_{7} = f(g(g(g(x_{4}))), x_{9})}
5. Γ_{WO} = {x_{3} = f(g(x_{4}), x_{5}), x_{6} = g(x_{4}), x_{5} = f(g(g(x_{4})), x_{7}), x_{8} = g(g(x_{4}))}
Γ_{U} = {x_{7} = f(g(g(g(x_{4}))), x_{9})}

There is no solution to the initial unification problem. The algorithm never terminates (except by resource bounding) because always new equations of the form x_{2j+1} = f(g^{j}(x_{4}), x_{2j+3}) were created by the rule Weakening.

6 Applications of Sorted Unification

Now we will fit the previous results together and apply it in full detail to the standard resolution calculus [20, 32] and the tableau calculus [24, 9]. As we promised in the introduction in order to make a calculus a sorted one, replace standard unification with sorted unification.

6.1 Resolution with Sorts

The starting point for the resolution calculus is a database of clauses Δ. From these clauses the sort theory L is chosen. L: = {(S_{i}(t_{i}), C′_{i})} such that for each declaration clause C_{i} ∈ Δ we choose exactly one declaration S_{i}(t_{i}) with C_{i} = {S_{i}(t_{i})} ∪ C′_{i}. The database is modified by the resolution and factorization rule extended with sorted unification. If application of the rules derives new declaration clauses, L must be updated. On the other hand if a reduction rule (e.g. subsumption) removes a declaration clause, this clause can also be removed from L. The inference rules are defined with respect to the dynamic sort theory L.

Definition 6.1 (Inference Rules) The rules are

Resolution  \begin{matrix}P (t_{1}, …, t_{n}) ∨ C_{1} \\ ¬P (s_{1}, …, s_{n}) ∨ C_{2} \\ C_{1}σ ∨ C_{2}σ ∨ D ∨ E \end{matrix}

where σ^{c} = (σ, D) is a cws. mgu of P (t_{1}, …, t_{n}) and P (s_{1}, …, s_{n}) and E is a set of literals (conditions) which guarantees the sorts occurring in COD(σ) but not in C_{1}σ ∨ C_{2}σ ∨ D to be non-empty. The non-emptiness conditions can be computed by Algorithm 4.22.

Factorization  \frac{P (t_{1}, …, t_{n}) ∨ P (s_{1}, …, s_{n}) ∨ C}{P (t_{1}, …, t_{n})σ ∨ Cσ ∨ D}

where σ^{c} = (σ, D) is a cws. mgu of P (t_{1}, …, t_{n}) and P (s_{1}, …, s_{n}).

The soundness of the rules follows immediately from their form, Lemma 4.4, and Lemma 4.18. Checking for empty sorts is not necessary for the factorization rule, because all sorts attached to variables in the codomain of σ occur in the factor.

Theorem 6.2 (Completeness Theorem for Resolution with Sorts) Let Δ be a clause database. We choose L: = {(S_{i}(t_{i}), C′_{i})} such that for each declaration clause C_{i} ∈ Δ we choose exactly one declaration S_{i}(t_{i}) with C_{i} = {S_{i}(t_{i})} ∪ C′_{i}.

If Δ is unsatisfiable there exists a derivation of the empty clause using resolution and factorization. The set L must be updated every time a new declaration clause is derived. Proof: (Sketch) It can be proved that every standard refutation of Δ yields a cws. substitution with respect to all declarations occurring in Δ. Now selecting one declaration from each clause consisting of declarations only and updating L during the refutation corresponds to a case analysis. Putting this together with Lemma 4.19 we obtain completeness for resolution. For more details see Weidenbach [28]. □

Considering the example from the introduction

Δ:

(1) S(a) ∨ R(a)
(2) S(f(x_{1}))
(3) Q(y_{1}, y_{1})
(4) ¬Q(a, y_{2})
(5) P (x_{2}, f(a))
(6) ¬P (a, x_{3})

where S(x_{i}) = S and S(y_{i}) = R we select the sort theory

L_{1} = {(S(a), {R(a)}), S(f(x_{1}))}

With respect to L_{1} the sort R is empty. The only applicable resolution step is (5)1 with (6)1 with cws. mgu

σc_{1} = ({x_{2} ↦ a, x_{3} ↦ f(a)}, {R(a)})

resulting in the resolvent

(7) R(a)

A new declaration clause is derived. Therefore L_{1} must be updated. As (7) subsumes (1) the new sort theory is

L_{2} = {R(a), S(f(x_{1}))}

Now S is empty and the only possible resolution step is (3)1 with (4)1 with cws. mgu

σc_{2} = ({y_{1} ↦ a, y_{2} ↦ a}, ∅)

yielding the empty clause

(8) □

The search space for Δ is finite. After selecting one of the two possible sort theories the application of resolution is deterministic. For Δ′, the standard formalization of Δ this is not the case. Here the search space is infinite and resolution can be applied to several clauses (S(z_{i}) = ⊤).

Δ′:
(1) S(a) ∨ R(a)
(2) ¬S(z_{1}) ∨ S(f(z_{1}))
(3) ¬R(z_{2}) ∨ Q(z_{2}, z_{2})
(4) ¬R(z_{3}) ∨ ¬Q(a, z_{3})
(5) ¬S(z_{4}) ∨ P (z_{4}, f(a))
(6) ¬S(z_{5}) ∨ ¬P (a, z_{5})

6.2 Tableau with Sorts

The free variable tableau is modified to a free variable sorted tableau. The usual notions for tableau are used [24, 9]. Thus an α formula is one of the kind (possibly after moving a negation inwards) F∧G, a β formula has the form F∨G, and the γ and δ formulae have a universal or an existential quantifier as top symbol respectively. Formulas of the form ¬¬F can be seen as α formulas where α_{1} = α_{2} = F.

Definition 6.3 (Inference Rules) The inference rules for tableau consist of the expansion rules

\begin{matrix}α & \frac{α}{{α_{1} \atop α_{2}}} & β & \frac{β}{β_{1} | β_{2}} \\ γ & \frac{γ}{γ(x)} & δ & δ ; δ(f(x_{1}, …, x_{n})) ; S_{1}(f(x_{1}, …, x_{n})) ; ⋮ ; S_{m}(f(x_{1}, …, x_{n})) \end{matrix}

where x is a new variable in the γ-rule. The function f is a new Skolem function where x_{1}, …, x_{n} are all the used free variables in the δ rule [9]. The sort {S_{1}, …, S_{m}} is the sort of the existentially quantified variable in δ which is replaced by f(x_{1}, …, x_{n}). Branches are closed atomically applying the atomic closure rule:

Atomic Closure Let T be a tableau for a set of sentences Δ. If some branch in T contains A and ¬B, where A and B are atoms, then Tσ is also a tableau for Δ, where σ is a most general non-empty well-sorted unifier of A and B.

The sort theory L selected for unification is the set of all declarations occurring on the current branch. Then σ must be a non-empty well-sorted unifier with respect to this sort theory. For these sort theories we always have T_{S} = T_{S}^{∅} for every sort S. Therefore the additional notions for conditional expressions can be skipped.

The δ rule not only generates the Skolemized formula but also the necessary declarations for the Skolem function. The semantics of existential quantifiers justifies the extended Skolemization (see the relativization rule in Section 2). We can easily prove that the Skolemized formula is equivalent to the original formula with respect to satisfiability.

Theorem 6.4 (Completeness Theorem for Tableau with Sorts) Let F be a valid sentence and R be any fair tableau construction rule (see Fitting [9]). Then there exists a closed tableau for ¬F such that:

(i) All tableau expansion rules come first and are according to R.

(ii) A single tableau substitution rule application follows, using a substitution σ that is a most general non-empty well-sorted atomic closure substitution.

Proof: The proof is a straight forward extension of the proof given by Fitting [9]. As we have Lemma 4.5 for sort theories used in tableau (T = T^{∅}), the non-empty well-sorted unifiers have the same properties with respect to semantics than standard unifiers. Thus together with Lemma 4.19 we obtain completeness of tableau with sorts. □

In fact, Theorem 6.4 is the sorted generalization of Theorem 7.8.6 given by Fitting [9, p. 179]. The application of sorted unification to tableau is that simple, because in tableau a case analysis is explicitly done by the β-rule. Therefore no conditional declarations are needed in the sort theory, whence Lemma 4.5 holds. Note that in different branches of a tableau different sort theories are considered in general.

Eventually, we solve the example from the introduction with the new tableau method. The tableau T after application of the expansion rules is

[figure: S(a) ∨ R(a); S(f(x_{1})); Q(y_{1}, y_{1}); ¬Q(a, y_{2}); P (x_{2}, f(a)); ¬P (a, x_{3}); S(a); R(a)]

where S(x_{i}) = S and S(y_{i}) = R. Applying atomic closure to the first branch, the corresponding sort theory is

L_{1} = {S(a), S(f(x_{1}))}

There are only two literals which become complementary: P (x_{2}, f(a)) and ¬P (a, x_{3}) with cws. unifier

σ_{1} = {x_{2} ↦ a, x_{3} ↦ f(a)}

The second branch can be closed applying atomic closure to Q(y_{1}, y_{1}) and ¬Q(a, y_{2}) with respect to the sort theory

L_{2} = {R(a), S(f(x_{1}))}

and cws. unifier

σ_{2} = {y_{1} ↦ a, y_{2} ↦ a}

As σ_{1} and σ_{2} are variable disjoint, Tσ_{1}σ_{2} is the closed tableau for the input formula and σ_{1}σ_{2} the necessary tableau substitution (see Theorem 6.4).

7 Discussion

The approach of Schmidt-Schauß [22] extends Walther’s work [27]. This paper generalizes the work of Schmidt-Schauß along the following dimensions:

(i) A sort is not only a sort symbol but a set of sort symbols.

(ii) Sorts may denote the empty set.

(iii) Declarations occurring in the sort theory may be conditioned by other literals.

(iv) If applied to a calculus the sort theory is a dynamic part of the database.

(i) is an extension of the sort language. It allows for a finite set of mgu’s in elementary sort theories where Schmidt-Schauß unification algorithm computes infinitely many mgu’s (Lemma 4.21). Schmidt-Schauß considered all (base) sorts to be a priori non-empty (ii). For the sorted unification theory this restriction plays no role. The problem arises if sorted unification is applied to a calculus. The precise problem is Skolemization. Traditionally, Skolemization in sorted languages is done in the following way [22, 11]. The formula ∃x_{S}F contained in some formula G is replaced by F{x_{S} ↦ f(…)} where f is the new Skolem function in the respective variables and the declaration S(f(…)) is put outside G into the sort theory. This is only a sound operation if S is not empty. Otherwise local Skolemization [28] must be performed where ∃x_{S}F is replaced by F{x_{S} ↦ f(…)} ∧ S(f(…)). Now declarations may occur together with other literals. Therefore the sort theory must either be a dynamic part of the database or additional inference rules which form the bridge between sort literals in the database and sort literals in the sort theory become necessary. Thus allowing for empty sorts results either in a calculus consisting of more rules than the standard rules of the calculus (e.g. see Cohn [5] or Beierle et al. [1]) or the sort theory must be a dynamic part of the database (iv) (see Weidenbach [30]). Thus approaches with a static sort theory and no additional inference rules must require sorts to be a priori non-empty (e.g. see Schmidt-Schauß [22] or Frisch [11]).

The same that holds for the introduction of possibly empty sorts applies to the notion of conditional expressions (iii). The additional notion does not change general properties of sorted unification (see Lemma 4.10). But then applied to the resolution calculus the notion allows an extension without the introduction of new inference rules. Until now this is the most efficient (in terms of search space reduction) method known [30].

Uribe [26] showed that sorted unification is decidable for semi-linear sort theories. Lemma 5.4 extends the class of sort theories with a decidable unification problem to pseudo-linear sort theories. However, there are differences between the two approaches. I separate the problem of sorted unification from the problem whether a sort is empty. Uribe doesn’t separate these problems. Whence he both proved unification and the empty sort problem decidable for semi-linear sort theories. Lemma 5.4 only says that the unification part is decidable for pseudo-linear sort theories. In fact, the empty sort problem is not decidable for pseudo-linear sort theories. This was shown by Tommasi [25]. Deciding whether a sort is empty (or whether two base sorts share a common ground term) is a harder problem than unification in sort theories. Uribe also gives a finite representation for a solution of a unification problem in semi-linear sort theories. The sorted unification problem for semi-linear sort theories is of unification type infinitary (see Example 4.20).

For his result, Tommasi used the correspondence between sort theories and finite tree automaton. This correspondence was first pointed out by Comon [6]. It makes results in automaton theory available to unification in sort theories. The general undecidability result given by Schmidt-Schauß could be confirmed. In addition, it was possible to proof decidability for linear sort theories this way. Until now other researchers have used the correspondence between tree automata and theories related to sort theories (e.g. set constraints) [3, 13].

The paper given by Frisch and Cohn [12] reformulates and abstracts results previously established by Schmidt-Schauß. They only consider base sorts as sorts but abstract away from a specific concept of a sort theory. An oracle is assumed which can be asked whether terms are well-sorted and which computes all possible weakenings σ such that tσ ∈ T_{S} for some sort S. Thus their sorted unification procedure GSUP has no specific sorted rules but a general, abstract weakening rule. Weakening and all cases of sorted failure are left to this rule. Compared to Schmidt-Schauß unification algorithm GSOUP, the six sorted rules are comprised in this abstract weakening rule. All other rules of the two algorithms are identical.

A property which was very often addressed in the past is regularity of sort theories [22, 14]. Schmidt-Schauß showed that if a sort theory is regular a more efficient unification algorithm can be formulated. However, regularity is an undecidable property for a given sort theory. The sorted unification algorithm presented in this paper overcomes the problem. It is as efficient as the unification algorithm SOUP for regular sort theories given by Schmidt-Schauß. This was possible by introducing sets of sort symbols as sorts. Thus from an efficiency point of view regularity is a superfluous concept. In addition, Comon [7] pointed out that if equality is included in the logic regularity is also not a useful concept.

In my previous work [31, 28, 30] I mainly addressed the extension of resolution with sorted unification. Only base sorts were considered as sorts and no specific results were given for unification in sort theories. In this paper the notion of sorts is extended, unification in elementary sort theories is proved to be decidable and of unification type finitary. Unification in pseudo-linear sort theories is proved decidable and of unification type infinitary. Algorithms for the computation of empty sorts and well-sortedness are presented and upper bounds for their time complexity established. A transformation of the rule based sorted unification algorithm into a sorted unification procedure is given. The new representation of the algorithm introduces more control structure and more data structure. The additional structure is used to prove unification in pseudo-linear sort theories decidable. Eventually, I generalized tableau with sorts from tableau with free variables. Future work will concentrate on the combination of sorts and equality.

References

[1] C. Beierle, U. Hedstück, U. Pletat, and J. Siekmann. An order-sorted logic for knowledge representation systems. Artificial Intelligence, 55:149–191, 1992.

[2] M. Bidoit and J. Corbin. A rehabilitation of robinson’s unification algorithm. In Proceedings of IFIP 9th World Computer Congress, pages 909–914. North-Holland, 1983.

[3] B. Bogaert and S. Tison. Equality and disequality constraints on direct subterms in tree automata. In Proc. of 9th Annual Symposium on Theoretical Aspects of Computer Science, STACS92, pages 161–171. Springer Verlag, 1992.

[4] A.G. Cohn. A more expressive formulation of many sorted logic. Journal of Automated Reasoning, 3(2):113–200, 1987.

[5] A.G. Cohn. A many sorted logic with possibly empty sorts. In 11th International Conference on Automated Deduction, CADE-11, LNCS 607, pages 633–647. Springer Verlag, 1992.

[6] H. Comon. Inductive proofs by specifications transformation. In Proc. of RTA, pages 76–91. Springer Verlag, 1989.

[7] H. Comon. Equational formulas in order-sorted algebras. In Proc. of ICALP, pages 674–688. Springer Verlag, 1990.

[8] N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1):69–115, July 1987.

[9] M. Fitting. First-Order Logic. Texts and Monographs in Computer Science. Springer, 1990.

[10] A.M. Frisch. A general framework for sorted deduction: Fundamental results on hybrid reasoning. In Proceedings of the First International Conference on Principles of Knowledge Representation and Reasoning, pages 126–136, May 1989.

[11] A.M. Frisch. The substitutional framework for sorted deduction: fundamental results on hybrid reasoning. Artificial Intelligence, 49:161–198, 1991.

[12] A.M. Frisch and A.G. Cohn. An abstract view of sorted unification. In 11th International Conference on Automated Deduction, CADE-11, LNCS 607, pages 178–192. Springer Verlag, 1992.

[13] R. Gilleron, S. Tison, and M. Tommasi. Solving systems of set constraints using tree automata. In P. Enjalbert, K.W. Wagner, and A. Finkel, editors, Proc. of 10th Annual Symposium on Theoretical Aspects of Computer Science, STACS93, pages 505–514. Springer Verlag, February 1993.

[14] J.A. Goguen and J. Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Draft, Programming Research Group, University of Oxford and SRI International, 1989.

[15] J. Herbrand. Investigations in proof theory: The properties of true propositions. In J. van Heijenoort, editor, From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, pages 525–581. Harvard University Press, 1967.

[16] G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, 1980.

[17] A. Martelli and U. Montanari. An efficient unification algorithm. ACM Trans. Programming Languages ans Systems, 4(2):258–282, 1982.

[18] A. Oberschelp. Untersuchungen zur mehrsortigen quantorenlogik. Mathematische Annalen, 145:297–333, 1962.

[19] M. Paterson and M. Wegman. Linear unification. Journal of the Computers and Systems, 16, 1978.

[20] J.A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, January 1965.

[21] A. Schmidt. Über deduktive theorien mit mehreren sorten von grunddingen. Mathematische Annalen, 115:485–506, 1938.

[22] M. Schmidt-Schauß. Computational aspects of an order sorted logic with term declarations, volume 395 of Lecture Notes in Artificial Intelligence. Springer Verlag, 1989.

[23] J. Siekmann. Unification theory. Journal of Symbolic Computation, Special Issue on Unification, 7:207–274, 1989.

[24] R.M. Smullyan. First-Order Logic. Springer Verlag, 1968.

[25] M. Tommasi. Automates avec tests d’égalités entre cousins germains. Master’s thesis, Universié de Lille, France, 1991.

[26] T.E. Uribe. Sorted unification using set constraints. In 11th International Conference on Automated Deduction, CADE-11, LNCS 607, pages 163–177. Springer Verlag, 1992.

[27] C. Walther. A Many-sorted Calculus based on Resolution and Paramodulation. Research Notes in Artificial Intelligence. Pitman Ltd., 1987.

[28] C. Weidenbach. A sorted logic using dynamic sorts. MPI-Report MPI-I-91-218, Max-Planck-Institut für Informatik, Saarbrücken, December 1991.

[29] C. Weidenbach. A new sorted logic. In Proceedings of the 16th German AI-Conference, GWAI-92, pages 43–54. Springer, LNAI 671, April 1992.

[30] C. Weidenbach. Extending the resolution method with sorts. In Proc. of 13th International Joint Conference on Artificial Intelligence, IJCAI-93. Morgan Kaufmann, 1993. To appear.

[31] C. Weidenbach and H.J. Ohlbach. A resolution calculus with dynamic sort structures and partial functions. In Proceedings of the 9th European Conference on Artificial Intelligence, pages 688–693. Pitman Publishing, London, August 1990.

[32] L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning, Introduction and Applications. McGraw-Hill, second edition, 1992.