A Sorted Logic Using Dynamic Sorts

Christoph Weidenbach

MPI–I–91–218 December 1991 Author’s Address

Christoph Weidenbach Max-Planck-Institut für Informatik Im Stadtwald 6600 Saarbrücken 11 Germany weidenb@mpi-sb.mpg.de

Publication Notes

This report is a more detailed and elaborated version of a number of papers submitted to several conferences.

Acknowledgements

I would like to thank D. Fehrer, P. Graf, M. Keil, A. Nonnengart and H.J Ohlbach for many discussions on sorted deduction as well as for many helpful remarks directly concerning this report.

Abstract

We present a sound and complete calculus CL_{S} for the first-order logic L_{S} without equality but dynamic sorts. By dynamic sorts we understand a sort structure which is exploited during the deduction process and is not fixed from the beginning. Therefore the logic allows arbitrary sort declarations and every first-order logic formula can be compiled into our logic. Deductions in the calculus turn out to be very efficient as will be shown by examples.

Thus the new logic significantly improves the efficiency of automated deductions if one-place (predicates) sorts are involved in the reasoning process. Furthermore the calculus CL_{S} is conservative extension of the existing approaches to sorted logic. That means if the sorted information could be represented in the known approaches the more general calculus CL_{S} has the same behaviour as the existing calculi.

Chapter 1

Introduction

It is widely accepted that the addition of “sorts” to first-order logic results in a more efficient resolution calculus and a more natural representation of problems, e.g. see [Wal87, SS89, WO90, Coh87, Fri89, BHPS89]. Although the “naturalness” of a representation may depend on the personal taste, there are many examples in the literature, where a sorted formalization of a problem leads to shorter proofs and a lesser branching rate, i.e. a smaller search space (e.g. the first solution to Schubert’s Steamroller [Wal84]).

Sorts correspond to unary predicates in unsorted first-order logic. For example in the logic of [WO90] the sort “declaration” f(x_{Male})< −Male is logically equivalent to the clause Male(x) ⇒ Male(f(x)) (where f denotes the father function). This simple example shows the advantages of a sorted formalization: less literals and hence less resolution possibilities. In particular, for this simple example there are infinitely many (self) resolution possibilities in the unsorted version, whereas there are no possible resolution steps in the sorted version.

Most of the work done so far separates the information about sorts from the rest [Wal87, SS89, Coh87, Fri89, BHPS89]. The description of the sort structure, e.g. subsort relationships or how functions operate on sorts, is contained in what is called the SBOX (Sort Box) and this remains static during the deduction process. The rest of the formulas is put in an FBOX (Formula Box) and here standard deduction rules (e.g. resolution) are applied. The SBOX is either built up using a special language (e.g. the declaration x_{S}< −T expresses that S is a subsort of T, using the language of [WO90]) or a first-order language is restricted to sort symbols as predicates (e.g. ∀x S(x) ⇒ T (x) [Fri89] also expressing the subsort relationship between S and T). In the FBOX no sort symbols are allowed as predicates. The connection between the SBOX and the FBOX is established by affixing a sort symbol to the variables. Variables are restricted to range over the denotation of their sort which is semantically viewed as a subset of the universe of discourse. Deduction rules (e.g. resolution) are modified by replacing the unsorted unification algorithm by a sorted version. The sorted unification algorithm checks the assignments to variables with respect to the information in the SBOX. In order so illustrate sorted resolution consider the following example (for the SBOX we use the syntax of [WO90]):

SBOX

(1) peter< −Male

(2)

mary< −Woman
(3) x_{Man}< −Male

(4) f(x_{Male})< −Male

FBOX (5) Love(x_{Male}, mary)

(6) ¬Love(f(f(peter)), y_{Woman})

which is logically equivalent to the unsorted formalization

UNSORTED

(1) Male(peter)

(2) Woman(mary)

(3) Man(x) ⇒ Male(x)

(4) Male(x) ⇒ Male(f(x))

(5) Male(x) ⇒ Love(x, mary)

(6) Woman(y) ⇒ ¬Love(f(f(peter)), y)

All variables are assumed to be universally quantified and the function f denotes the father of a person. There is only one resolution step between the clauses (5) and (6) in the sorted formalization leading to the unification problem [Sie89] Γ = {x_{Male} = f(f(peter)), y_{Woman} = mary}. The unification problem is trivially solved already, if we disregard the sort unification. However the sorted unification algorithm must also check the well sortedness of the assignments. It has to be proved that in every model satisfying the SBOX, f(f(peter)) is of sort Male and mary of sort Woman. In this example this is clearly the case. In general the proof is done by the sorted unification algorithm. In our case Γ is well sortedly solved and one resolution step yields the empty clause.

In the unsorted version of the example there are several possible resolution steps. Resolution between (5) and (6) results in the clause

(7) ¬Male(f(f(peter))) ∨ ¬Woman(mary)

which can be refuted using twice clause (4) and then the clauses (1) and (2). This simple example demonstrates the advantages of sorted deduction:

• Compact Representations In the sorted version we needed six literals (including the declarations in the SBOX) in the unsorted version ten.

• Short Deductions In the sorted version the clauses are refuted in one step, in the unsorted version we needed five steps. Of course we have also to take the steps of the sorted unification algorithm into account. But in practise the amount spent on the sorted unification can be neglected in comparison to the rest of the work. This topic will be discussed in more detail later on.

• Small Search Space In the sorted version there is one unique resolution step yielding the empty clause, in the unsorted version there are infinitely many possible steps. For example there are infinitely many (self) resolvents of clause (4).

In this report we present a new approach to sorted deduction which generalizes the existing ones: Arbitrary formulas are allowed in the SBOX and there is no longer a distinction between the SBOX and the FBOX. Sort declarations of the form t< −S (or sort predicates known from other sorted logics) can be used as ordinary predicates. Nevertheless the new sorted calculus which follows the ideas of [Wal87, SS89, WO90] significantly outperforms unsorted calculi. In addition the new approach is a conservative extension of the existing ones. That means if the information could be separated and represented in the known approaches (e.g. [Wal87, SS89]) the more general calculus has the same behaviour as the existing calculi.

Compared to the other approaches [Wal87, SS89, Fri89] strictly follow the SBOX, FBOX paradigm and [Coh87, BHPS89] allow sort information to occur in the FBOX, but they only consider the static SBOX information for the sorted reasoning. In addition all these approaches impose strong restrictions on the formulas in the SBOX in order to obtain a sound and complete calculus. This topic will be discussed in more detail in Section 1.1.1. In [WO90] the SBOX, FBOX scheme is still abolished but the calculus presented there is rather weak compared to the CL_{S} calculus which is established in this report. This topic will be discussed in more detail in Chapter 6.

The following sections give a an informal overview of the subsequent chapters. Results will be motivated and discussed but without any technical details. In Section 1.1 the new logic will be motivated and introduced. Section 1.2 explains the new calculus. The following sections are informal versions of the chapters 2-6. Chapter 7 introduces some refinements and further improvements on the calculus CL_{S}. In Chapter 8 we solve some well known examples which are introduced in Section 3.3 and discuss efficiency aspects. The report is finished by the conclusions presented in Chapter 9.

1.1 The Sorted Logic L_{S}

1.1.1 Motivation

The main difference between the new sorted logic L_{S} presented in this paper and existing approaches is that we abolish the SBOX, FBOX paradigm. There are at least three reasons to pull down the barrier between SBOX and FBOX: (i) expressivity, (ii) Skolemization and (iii) disjunctions in the SBOX.

In order to exemplify the first problem, namely expressivity consider the phrase which says that a male is a man if he has written a book, begotten a child and planted a tree. Coding this example gives the formula:

Write(x_{Male}, y_{Book}) ∧ Plant(x_{Male}, z_{Tree}) ∧ Beget(x_{Male}, u_{Child})
⇒ x_{Male}< −Man

This formula does not fit into the SBOX, FBOX scheme, because ordinary twoplace predicates are used to define a sort. Thus the formula can not be represented adequately in existing approaches. Formulas of the above kind are not artificial, e.g. they frequently occur in knowledge bases of the KL-ONE [BS85] family.

The next problem is Skolemization, the elimination of existential quantifiers in refutation based deduction systems. The proper Skolemization (see Chapter 4) of the FBOX formula

∃y_{Woman} Love(peter, y_{Woman}) ∨ Love(peter, Bill)

is (Love(peter, a) ∧ a< −Woman) ∨ Love(peter, Bill)

where a is a new Skolem constant. Again the SBOX, FBOX framework is violated because declarations (or sort predicates) are not allowed in the FBOX. Putting the declaration a< −Woman outside the FBOX and into the SBOX results in a Skolemization which does not preserve satisfiability, because a< −Woman in the SBOX forces the sort Woman to be non empty in every model whereas there are models of the input formula which assign the empty set to the sort Woman. However empty sorts are not the only reason that disallow declarations resulting from skolemization in the SBOX and in general we need strong restrictions (e.g. see [Wal87, SS89]) to be imposed on the SBOX in order to place these declarations into the SBOX.

The third problem arises from disjunctions in the SBOX. If there are formulas like

peter< −Man ∨ peter< −Woman

in the SBOX then there is no initial model for the SBOX. A least model either includes peter< −Man or peter< −Woman. From the formula

∀x_{Man} Love(x_{Man}, mary)

we must be able to deduce

Love(peter, mary) ∨ peter< −Woman

in order to obtain a complete calculus. Again this clause does not fit into the SBOX, FBOX paradigm.

All these problems can be overcome if the artificial barrier between SBOX an FBOX is eliminated: SBOX expressions are also FBOX expressions and formulas denoting sort relationships can be combined with ordinary formulas. This logic is called L_{S}.

1.1.2 Syntax of L_{S}

A signature Σ: = (S, V, F, P) of the sorted logic L_{S} contains a set of sort symbols in addition to the usual sets V of variable symbols, F of function symbols and P of predicate symbols. The fixed 2-place predicate < − is always in P. Variables are indexed with their sort, e.g. x_{S}, y_{V}.

Terms and atoms are built in the usual unsorted way with the addition that if t is a term and S a sort symbol, then t< −S is an atom. Atoms of the form t< −S are called declarations. From atoms we construct literals and formulas using the logical connectives. A clause is a set of literals which is interpreted as the universal closure of the disjunction of the literals.

The set of all terms is denoted by T_{Σ}. Substitutions are total functions σ: V → T_{Σ} such that the set DOM(σ): = {x_{S} | σ(x_{S}) ≠ x_{S}} is finite. The application of substitutions can be extended to terms, formulas, and clauses in the usual way.

1.1.3 Semantics of L_{S}

In order to define the semantics for the new logic, a set of objects from the nonempty universe has to be assigned to every sort symbol and a total function to every function symbol. The symbol < − is interpreted as the membership relation, whereas predicates and the logical connectives are interpreted as in unsorted first-order logic.

Let Σ be a signature. A Σ-algebra A consists of a non-empty carrier set A, a total function f_{A}: A^{n} → A for every function symbol f∈F_{n}, a set S_{A} ⊆ A for every sort S.

An interpretation ℑ ^{1} assigns an n-ary relation P_{ℑ} ⊆ A^{n} to every n-place predicate symbol P and the membership relation to < −, such that for every formula F, t∈T_{Σ}, S∈S, and P ∈P_{n}:

• ℑ ⊧ P (t_{1}, …, t_{n})  iff (ℑ_{h}(t_{1}), …, ℑ_{h}(t_{n}))∈P_{ℑ}.
• ℑ ⊧ t< −S  iff ℑ_{h}(t)∈S_{A}
• ℑ ⊧ ∀x_{S} F  iff for all a∈S_{A}, ℑ{x_{S}/a} ⊧ F
• ℑ ⊧ ∃x_{S} F  iff there exists an a∈S_{A}, ℑ{x_{S}/a} ⊧ F

• The logical connectives are interpreted as usual.

1An interpretation ℑ{x_{S}/a} is like ℑ except that it maps x_{S} to a

1.2 Calculi for Sorted Logics

1.2.1 Existing Calculi

Logics following the SBOX, FBOX paradigm [Wal87, SS89, Fri89, Coh87, BHPS89] construct a free model from the declarations in the SBOX^{2}. In order to guarantee the existence of a free model only unit declarations of the form t< −S are allowed in the SBOX. The free model is the set T_{L< −} of well sorted terms where L_{< −} is the set of all declarations occurring in the SBOX.

Definition 1.2.1 (Well Sorted Terms) Let L_{< −} be a set of declarations. Then the set of well sorted terms T_{L_{< −},S} of sort S is recursively defined by:

• for every variable x_{S}, x_{S}∈T_{L_{< −},S}

• for every declaration (t< −S)∈L_{< −} with V (t) = {x_{S_{1}}, …, x_{S_{n}}} and terms t_{i}∈T_{L_{< −},S_{i}}, σ: = {x_{S_{1}} ↦t_{1}, …, x_{S_{n}} ↦t_{n}}, σ(t)∈T_{L_{< −},S}

The function V maps terms to their variables, substitutions σ are enumerated by the variable term pairs (e.g. x_{S_{1}} ↦t_{1}) of their finite domain (DOM(σ)). Computations in the free model are very efficient (this is one serious reason why sorted unification is always more efficient than the corresponding unsorted resolution). It is decidable in polynomial time and space [SS89] if t∈T_{L< −,S} for an arbitrary term t, sort S, and set of declarations L_{< −}.

Applying the definition of well sorted terms to the initial example, we get L_{< −} = {peter< −Male, mary< −Woman, x_{Man}< −Male, f(x_{Male})< −Male} and T_{L< −,Male} = {peter, f(peter), f(f(peter)), …, x_{Male}, y_{Male}, …, f(x_{Male}), …}

The sorted unification algorithm is an extension of the known unsorted unification algorithm. In addition to the unsorted algorithm variables are weakened until for every assignment x_{S} ↦ t we have t∈T_{L< −,S}. The sorted resolution rule is an extension of the unsorted resolution rule by sorted unification.

1.2.2 The New Sorted Calculus CL_{S}

The starting point for the new calculus is a set CS of clauses (in Chapter 4 we show the transformation into clause normal form). Clearly the traditional means of sorted reasoning do not apply to this expressive sorted logic L_{S} since in general there exist no free model for the declarations occurring in a clause set. Even more, as declarations can be combined with arbitrary first-order formulas well sortedness can not be decided globally. Thus it is not clear how sorted unification can be established. Nevertheless the information about sorts for the unification algorithm is contained in the declarations occurring in the clause set. The open question is which declarations must be considered for the unification algorithm. Clearly all declarations occurring in unit clauses must be chosen (e.g. peter< −Man from the initial example) because every model satisfying the clause set satisfies these declarations. Additionally a translation of the sort structures of [Wal87, SS89] into L_{S} results in unit clauses that are declarations.

2Frisch [Fri89] does not give a syntactic characterization of well sortedness and hence the question how to check well sortedness remains open

But if we choose only declarations that occur in unit clauses, this would result in an incomplete calculus as the following example shows.

SBOX-FBOX (1) peter< −Man ∨ peter< −Woman (2) Love(x_{Man}, paul)

(3) Love(y_{Woman}, mary)

(4) ¬Love(peter, paul)

(5) ¬Love(peter, mary)

The clause set is unsatisfiable. There is no unit declaration because the only declarations peter< −Man and peter< −Woman occur in the same clause. Thus if we only consider unit declarations, there is no well sorted resolution step. The sorted unification algorithm has no information about sorts. Thus neither the assignment x_{Man} ↦ peter nor y_{Woman} ↦ peter is well sorted. But to obtain a complete calculus we must consider at least one of the declarations for unification. This can not be done in the standard way (see Section 1.2.1) because not every model satisfying the clause (1) satisfies the chosen declaration^{3}. The other literal can not be discarded, it must be taken as a residue literal for the chosen declaration similar to a partial theory resolution step [Sti85]. A declaration occurring in a non unit clause is called a conditioned declaration and denoted as a pair (t< −S, C) where C is a set of literals. The idea is to use the declaration as for sorted unification and to collect the conditions during the computation of well sortedness.

Selecting the set of declarations L_{< −} = {(peter< −Man, {peter< −Woman})} for unification, a resolution step between (2) and (4) is possible as the assignment x_{Man} ↦ peter is well sorted with respect to the chosen declaration (peter< −Man, {peter< −Woman}). But as not every model satisfies the chosen declaration the result is the only condition

(6) peter< −Woman

Intuitively clause (6) means that if we assume peter to be a Man we get a contradiction between (2) and (4). Therefore we conclude peter to be of sort Woman. This new clause is a unit declaration and subsumes clause (1). We must change the information of the unification algorithm into L_{< −} = {(peter< −Woman, ∅)}. Now a resolution step between clause (3) and clause (5) is possible, yielding the empty clause.

If we would have started with the set of declarations L_{< −} = {(peter< −Woman, {peter< −Man})} we would have made the same resolution steps in reverse order.

3An alternative approach was presented in [WO90] where residue literals were added for each assignment in order to get sound inference rules.

The example shows that for the CL_{S} calculus, the sort information must be changed dynamically during the deduction process and non unit declarations have to be considered.

The conditioned declarations are needed for a generalized notion of well sortedness where a term is of a specific sort under certain conditions. Thus conditioned declaration cause conditioned terms (pairs of the kind (t, C) where t is a term and C a set of literals) and conditioned substitutions (pairs of the kind (σ, C) where σ is a substitution and C a set of literals).

Definition 1.2.2 (Conditioned Well Sorted Terms) Let L_{< −} be a set of conditioned declarations. Then the set of conditioned well sorted terms Tc_{L_{< −},S} of sort S is recursively defined by:

• for every variable x_{S}, (x_{S}, ∅)∈Tc_{L_{< −},S}

• for every conditioned declaration (t< −S, C)∈L_{< −} with V (t) = {x_{S_{1}}, …, x_{S_{n}}} and

conditioned terms (t_{i}, C_{i})∈Tc_{L_{< −},S_{i}}, σ: = {x_{S_{1}} ↦t_{1}, …, x_{S_{n}} ↦t_{n}}, (σ(t), σ(C) ∪

C_{1} … ∪ C_{n})∈Tc_{L_{< −},S}

Questions of the form t< −Tc_{L< −,S} are again decidable in polynomial time and space with respect to the number of symbols in t and the number of declarations in L_{< −}. The new sorted unification algorithm is an extension of the known sorted unification algorithms (for an overview see [SS89]) by conditioned well sorted terms. A presentation of the algorithm can be found in Section 6.1. The result of the algorithm is a conditioned well sorted unifier including the set of conditions that are needed on order to establish the conditioned well sortedness. The resolution rule is then:

Definition 1.2.3 (Resolution Rule) Let C_{1} and C_{2} be two clauses with no variables in common, L∈C_{1} and K∈C_{2}. If there exists a conditioned well sorted mgu σ^{c} = (σ, D) of L and K, such that σ(L) and σ(K) are two complementary literals, then

σ((C_{1} \ {L}) ∪ (C_{2} \ {K})) ∪ D

is a resolvent of C_{1} and C_{2}.

A conditioned substitution σ^{c} = (σ, D) consists of the substitution σ and the set of conditions D. The sorted factorization rule is defined accordingly. The correctness of the inference rules follows immediately from the correctness of conditioned well sorted terms and the form of the rules. The proof of the following completeness theorem is given in Section 6.3:

Theorem 1.2.4 (Completeness Theorem) Let CS be a clause set of L_{S} and let L_{< −}: = {(t_{i}< −S_{i}, C′_{i})} such that for each clause C_{i}∈CS consisting of declarations we choose exactly one declaration t_{i}< −S_{i} with C_{i} = {t_{i}< −S_{i}} ∪ C′_{i}.

If CS is unsatisfiable, there exists a derivation of the empty clause using resolution and factorization.

Now the refutation procedure works as follows: a set L_{< −} of declarations (see Theorem 1.2.4) from the given clause set CS is chosen and the inference rules are applied. If a new clause consisting of declarations only is derived, the set L_{< −} of declarations is updated. This process is repeated until the empty clause is obtained.

Syntax of LS

The Syntax of L_{S} is very similar to the syntax of unsorted first-order logic, because we have to allow for “ill-sorted” terms. Thus we generate terms, atoms, and formulas without considering sorts. Only the special relation < − is added and variables are indexed with the sort they range over.

2.1 Signature

Definition 2.1.1 (Signature) A signature Σ: = (S, V, F, P) consists of the following disjoint sets:

• S is a finite set of sort symbols, the fixed symbol ⊤ for “any” is always in S. Sort symbols are S, T.

• V is an infinite set of countably many variable symbols. The symbols x, y, z represent variables.

• F is a countably infinite set of function symbols. F is divided into the sets of n–place function symbols F_{n} (n∈IN_{0}). We use the f, g, h as function symbols and a, b, c as constant symbols (0-place function symbols).

• P is a finite set of predicate symbols divided into the sets of n–place predicate symbols P_{n}. Predicates are named by P, Q.

Additionally, we assume a function sort: V → S such that for every sort T ∈S, there exist countably infinite many variables x∈V, with sort(x) = T. In this case we say x has sort T which is denoted by x_{T}.

In order to simplify the notation for variables, we allow to write x_{S} and x_{T} in the same formula even if they are supposed to be different. Using this writing convention two variables are equal if they consist of the same variable symbol and have the same sort.

Definition 2.1.2 (Special Symbols) The following symbols are available:

• The logical connectives ¬, ∧, ∨, ⇒, ⇔, ∀, ∃

• The auxiliary symbols “(”, “)”, “, ”

• The special relation < − which is used to represent sort information.

Assumption 2.1.3 (Non-empty Universe) We always assume that there is at least one constant symbol in Σ. This assumption implies that the universe of discourse and the sort ⊤ are not empty. This appears natural to us, because we have the same assumption in unsorted first-order logic.

2.2 Terms, Atoms, and Formulas

Definition 2.2.1 (Terms) The set of all terms T_{Σ} is inductively constructed by the following two rules:

• x∈T_{Σ}, if x∈V

• f(t_{1}, …, t_{n})∈T_{Σ}, if f∈F_{n} and t_{i}∈T_{Σ} for every i

Let V (t) denote the set of variables occurring in a term t, i. e. V (t): = {t}, if t is a variable and V (t): = ⋃_{1≤i≤n} V (t_{i}), if t = f(t_{1}, …, t_{n}). We can naturally extend V

to atoms, literals, clauses, and other objects. An object t having V (t) = ∅ is called ground.

Definition 2.2.2 (Atoms) If P ∈P_{n} and t_{1}, …, t_{n} are terms then P (t_{1}, …, t_{n}) is an atom. If S is a sort symbol and t is a term, then t< −S is an atom. An atom of the form t< −S is called a declaration.

Definition 2.2.3 (Literals) Atoms and their negations are literals. A literal is called negative if it consists of an atom and a negation symbol. Otherwise it is called positive. The meta level function atom maps literals to their atoms. For literals we write L, K.

Definition 2.2.4 (Clauses) A clause is a finite set of literals. It is interpreted as the disjunction of its literals where the whole clause is universally quantified over all occurring variables. For clauses we write C = {L_{1}, L_{2}}. The empty clause is denoted by □.

If C is a clause then ∀(C) denotes the formula obtained by building the disjunction of all literals in C and closing all variables universally. For example if C = {P (x_{S}), ¬Q(x_{S}, f(y_{T}))} then ∀(C) = ∀x_{S} ∀y_{T} (P (x_{S}) ∨ ¬Q(x_{S}, f(y_{T}))). If we want a variable in C not to be universally closed, we write ∀[x_{S}] (C), i.e. for the example ∀[x_{S}] (C) = ∀y_{T} (P (x_{S}) ∨ ¬Q(x_{S}, f(y_{T}))).

Definition 2.2.5 (Formulas) Every literal is a formula. If F and G are formulas then (¬F), (F ∧ G), (F ∨ G), (F ⇒ G) and (F ⇔ G) are formulas. If F is a formula and x_{T} a variable then (∀x_{T} F) and (∃x_{T} F) are formulas. We omit parenthesis whenever possible using the following precedence starting from the logical connective with the highest precedence to the lowest one: ¬, ∀, ∃, ∧, ∨, ⇒, ⇔.

Definition 2.2.6 (Substitutions) A substitution σ is a total function σ: V → T_{Σ}, such that the set { x_{S}∈V | σ(x_{S}) ≠ x_{S} } is finite.

Let DOM(σ): = { x_{S}∈V | σ(x_{S}) ≠ x_{S} }. Since every substitution σ is uniquely determined by its action on the variables of DOM(σ), it can be represented as a finite set of variable–term pairs {x_{S_{1}} ↦ t_{1}, …, x_{S_{n}} ↦ t_{n}}, where DOM(σ) = {x_{S_{1}}, …, x_{S_{n}}}. We can extend the application of σ to T_{Σ} by σ(t): = σ(t), if t∈V and σ(t): = f(σ(t_{1}), …, σ(t_{n})), if t = f(t_{1}, …, t_{n}). Similarly, the application of σ can be extended to other objects, e.g. literals, clauses or sets of such objects. Let COD(σ): = σ(DOM(σ)) and I(σ): = V (COD(σ)). A substitution σ is called ground if I(σ) = ∅.

The composition of two substitutions σ = {x_{S_{1}} ↦ t_{1}, …, x_{S_{n}} ↦ t_{n}} and τ = {y_{T_{1}} ↦s_{1}, …, y_{T_{m}} ↦s_{m}} can be computed by στ = {y_{T_{1}} ↦σ(s_{1}), …, y_{T_{m}} ↦σ(s_{m})}∪ { x_{S_{i}} ↦ t_{i} | x_{i}∈(DOM(σ) − DOM(τ)) }. A substitution σ is called idempotent if σσ = σ. Note that a substitution σ is idempotent iff DOM(σ) ∩ I(σ) = ∅. With σ[x_{S}] we denote a substitution that is equal to σ, except that it maps x_{S} to x_{S}.

Definition 2.2.7 (Subformula, Scope, Positive Component) Let F, G, H be formulas. F is a subformula of G, if F is G or a formula that occurs within G. F (or a variable x_{T}) is in the scope of a universal quantifier ∀ (an existential quantifier ∃, a conjunction ∧,…) iff F is a subformula of G (or H) in ∀x_{S} G (∃x_{S} G, G ∧ H, …). An occurrence of a subformula F in a formula G is a positive component of G iff G contains no implication or equivalence symbols and the occurrence of F is not in the scope of a negation symbol.

Definition 2.2.8 (Free, Bound Variables) For a formula F, the set F V (F) of free variables of F [Gal86] is defined by:

• F V (P (t_{1}, …, t_{n})) = V (t_{1}) ∪ … ∪ V (t_{n}) for an n–place predicate P

• F V (t< −S) = V (t) for the special relation < −

• F V (¬F) = F V (F)

• F V (F ⋆ G) = F V (F) ∪ F V (G), where ⋆∈{∧, ∨, ⇒, ⇔}

• F V (∀x_{T} F) = F V (F) \ {x_{T} }

• F V (∃x_{T} F) = F V (F) \ {x_{T} }

Given a formula F, the set BV (F) of bound variables of F is given by:

• BV (P (t_{1}, …, t_{n})) = ∅ for an n–place predicate P • BV (t< −S) = ∅ for the special relation < −

• BV (¬F) = BV (F)

• BV (F ⋆ G) = BV (F) ∪ BV (G), where ⋆∈{∧, ∨, ⇒, ⇔}

• BV (∀x_{T} F) = BV (F) ∪ {x_{T} }

• BV (∃x_{T} F) = BV (F) ∪ {x_{T} } A variable x_{T} is free within a formula F if x_{T} ∈F V (F) and x_{T} is called bound within a formula F if x_{T} ∈BV (F). Note that a variable can occur both free and bound in a formula. For example the variable x_{S} in the formula ∀x_{S} P (x_{S}) ∨ Q(x_{S}) has this property.

Assumption 2.2.9 (Considering only Sentences) We only consider formulas without free variables. Such formulas are called sentences.

Semantics

In order to define the semantics for L_{S}, we have to assign a set of objects of the non-empty universe to every sort symbol, a total function to every function symbol, < − is interpreted as the membership relation and we interpret predicate symbols and the logical connectives in the usual way.

3.1 Algebras

Definition 3.1.1 (Σ-algebra) Let Σ be a signature. A Σ-algebra A consists of a non-empty carrier set A, a total function f_{A}: A^{n} → A for every function symbol f∈F_{n}, a set S_{A} ⊆ A for every sort S and ⊤_{A}: = A.

Definition 3.1.2 (Σ-assignment) Let A be a Σ-algebra. A Σ-assignment is a partial mapping φ: V → A with φ(x)∈sort(x)_{A} if x∈D(φ)^{1}. The homomorphic extension φ_{h}: T_{Σ} → A of a Σ-assignment φ is defined as follows:

• φ_{h}(x)  : = φ(x) for all Σ-variables x
• φ_{h}(f(t_{1}, …, t_{n}))  : = f_{A}(φ_{h}(t_{1}), …, φ_{h}(t_{n})) if t_{i}∈D(φ_{h})
and we define f(t_{1}, …, t_{n})∈D(φ_{h})

From now on we don’t distinguish between φ and φ_{h}. Let φ be a Σ-assignment, a∈S_{A}, x∈V with sort(x) = S and t∈T_{Σ} then

• φ[{x/a}](t)  : = a if t∈V and t = x.
• φ[{x/a}](t)  : = φ(t) if t∈V and t ≠ x.
• φ[{x/a}](t)  : = f_{A}(φ[{x/a}](t_{1}), …, φ[{x/a}](t_{n}))
if t = f(t_{1}, …, t_{n}).

That means φ[{x/a}] is like φ except that it maps x to a.

1D(φ) denotes the domain of the function φ

3.2 Structures and Interpretations

Definition 3.2.1 (Σ-structure) Let Σ be a signature. A Σ-structure M is a Σalgebra A which has additional denotations P_{M} for every predicate symbol P ∈P_{n} and the special symbol < −, such that:

• P_{M} is a relation with P_{M} ⊆ A^{n}

• < −_{M} is the membership relation, i.e. < −_{M} = ∈

Definition 3.2.2 (Interpretation) Let M be a Σ-structure and φ: T_{Σ} → A a Σ-assignment. The pair ℑ = (M, φ) is called an interpretation and we define the satisfiability relation ⊧ between ℑ and formulas as follows: let F be a formula, s, t∈T_{Σ}, T ∈S and P ∈P_{n}:

• ℑ(t) = φ(t)

• ℑ ⊧ P (t_{1}, …, t_{n})  iff t_{i}∈D(φ) and (φ(t_{1}), …, φ(t_{n}))∈P_{M}.
• ℑ ⊧ s< −T  iff s∈D(φ) and φ(s)∈T_{M}.
• ℑ ⊧ ∀x_{S} F  iff for all a∈S_{A}, (M, φ[{x_{S}/a}]) ⊧ F
• ℑ ⊧ ∃x_{S} F  iff there exists an a∈S_{A}, (M, φ[{x_{S}/a}]) ⊧ F

• The logical connectives ¬, ∧, ∨, ⇒, ⇔ are interpreted in the usual way.

Note that the Σ-assignment φ is defined for every term occurring in a sentence.

Definition 3.2.3 (Σ-model, satisfiable, unsatisfiable, well-sorted) Let F be a formula. An interpretation ℑ is a Σ-model for F if ℑ ⊧ F. A set F of formulas has a Σ-model ℑ if for every F∈F, ℑ ⊧ F. A formula is called satisfiable if it has a Σ-model. We call a formula unsatisfiable if it has no Σ-model.

3.3 Examples

Example 3.3.1 (Schubert’s Steamroller) The first example is the standard example for the first complete order-sorted calculus given by Walther [Wal87].

Wolves, foxes, birds, caterpillars, and snails are animals, and there are some of each of them. Also there are some grains, and grains are plants. Every animal either likes to eat all plants or all animals much smaller than itself that like to eat some plants. Caterpillars and snails are much smaller than birds, which are much smaller than foxes, which in turn are much smaller than wolves. Wolves do not like to eat foxes or grains, while birds like to eat caterpillars, but not snails. Caterpillars and snails like to eat some plants. Therefore there is an animal that likes to eat a grain-eating animal.

This problem has been coded in first-order logic in many different ways. We adopt a formulation proposed by Mark Stickel in [Sti86] where “grain-eating animal” refers to an animal that eats some grain. We introduce two binary relations E and M, where E(x, y) means “x likes to eat y” and M(u, v) means “u is much smaller than v” and the sort symbols G, P, C, B, S, F, W, A for grains, plants, caterpillars, birds, snails, foxes, wolves, and animals respectively. In order to have only nonempty sorts we introduce a constant for each of them. Then the following formulas represent the steamroller problem:

1) ∀x_{W} x_{W} < −A ∧ ∀x_{F} x_{F} < −A ∧ ∀x_{B} x_{B}< −A ∧ ∀x_{C} x_{C}< −A ∧

∀x_{S} x_{S}< −A

2) lupo< −W ∧ foxy< −F ∧ tweety< −B ∧ raupy< −C ∧

schnecky< −S

3) muesli< −G  ∧ ∀x_{G} x_{G}< −P
4) ∀x_{A} (∀y_{P} E(x_{A}, y_{P}) ∨ ∀z_{A} ((M(z_{A}, x_{A}) ∧ ∃v_{P} E(z_{A}, v_{P})) ⇒ E(x_{A}, z_{A})))
5) ∀x_{C}, y_{S}, z_{B}, x′_{F} , y′_{W} (M(x_{C}, z_{B}) ∧ M(y_{S}, z_{B}) ∧ M(z_{B}, x′_{F}) ∧ M(x′_{F} , y′_{W}))
6) ∀x_{G}, y_{F} , z_{W} (¬E(z_{W} , y_{F}) ∧ ¬E(z_{W} , x_{G}))
7) ∀x_{B}, y_{C}, z_{S} (E(x_{B}, y_{C}) ∧ ¬E(x_{B}, z_{S}))
8) ∀x_{C} ∃y_{P} E(x_{C}, y_{P}) ∧ ∀x_{S} ∃y_{P} E(x_{S}, y_{P})
9) ∃x_{A}, y_{A}, z_{G} (E(x_{A}, y_{A}) ∧ E(y_{A}, z_{G}))

In [Sti86] different formalizations of the theorem are discussed. In order to demonstrate our CNF-Algorithm (see Chapter 4, Example 4.2.3) we will use the theorem formula ∃x_{A} ∃y_{A} (E(x_{A}, y_{A}) ∧ ∀x_{G} E(y_{A}, x_{G})). Choosing this representation of the theorem results in a more complicated resolution proof.

Example 3.3.2 (The Lion and the Unicorn) The second example is a puzzle named “The Lion and the Unicorn”, that can be found in [Smu78]. It reads as follows:

When Alice entered the forest of forgetfulness, she did not forget everything, only certain things. She often forgot her name, and the most likely thing for her to forget was the day of the week. Now, the lion and the unicorn were frequent visitors to this forest. These two are strange creatures. The lion lies on Mondays, Tuesdays and Wednesdays and tells the truth on the other days of the week. The unicorn, on the other hand, lies on Thursdays, Fridays and Saturdays, but tells the truth on the other days of the week. One day Alice met the lion and the unicorn resting under a tree. They made the following statements:

Lion: Yesterday was one of my lying days. Unicorn: Yesterday was one of my lying days.

From this statements, Alice, who was a bright girl, was able to deduce the day of the week. What was it ?

In our formalization of the problem we follow mainly the suggestions in [OSS85]. Thus our signature consists of the sorts Mo, Tu, We, Th, Fr, Sa and Su which stand for the days of the week, the sorts LL and LU which denote the lying days of the lion and the unicorn, respectively, a sort D for all days and a sort C for the two creatures. The constants mon, tue, wed, thu, fri, sat and sun, the constants lion and uni and a 1-place function f are needed. Furthermore we need a 3-place predicate Lies(x_{C}, y_{D}, z_{D}) which is true if the creature x_{C} says at day y_{D} that it lies at day z_{D}. Now we can give a complete set of formulas for this problem:

1) mon< −Mo  ∧ tue< −Tu  ∧ wed< −We  ∧
thu< −Th  ∧ fri< −Fr  ∧ sat< −Sa  ∧
sun< −Su
2) ∀x_{Mo} x_{Mo}< −LL  ∧ ∀x_{Tu} x_{Tu}< −LL  ∧ ∀x_{We} x_{We}< −LL  ∧
∀x_{Th} x_{Th}< −| LL  ∧ ∀x_{Fr} x_{Fr}< −| LL  ∧ ∀x_{Sa} x_{Sa}< −| LL  ∧
∀x_{Su} x_{Su}< −| LL
3) ∀x_{Mo} x_{Mo}< −| LU  ∧ ∀x_{Tu} x_{Tu}< −| LU  ∧ ∀x_{We} x_{We}< −| LU  ∧
∀x_{Th} x_{Th}< −LU  ∧ ∀x_{Fr} x_{Fr}< −LU  ∧ ∀x_{Sa} x_{Sa}< −LU  ∧
∀x_{Su} x_{Su}< −| LU
4) ∀x_{Mo} x_{Mo}< −D  ∧ ∀x_{Tu} x_{Tu}< −D  ∧ ∀x_{We} x_{We}< −D  ∧
∀x_{Th} x_{Th}< −D  ∧ ∀x_{Fr} x_{Fr}< −D  ∧ ∀x_{Sa} x_{Sa}< −D  ∧
∀x_{Su} x_{Su}< −D
5) ∀x_{LL} x_{LL}< −D  ∧ ∀x_{LU} x_{LU} < −D
6) lion< −C  ∧ uni< −C
7) ∀x_{Mo} f(x_{Mo})< −Su ∧ ∀x_{Tu} f(x_{Tu})< −Mo ∧ ∀x_{We} f(x_{We})< −Tu ∧
∀x_{Th} f(x_{Th})< −We ∧ ∀x_{Fr} f(x_{Fr})< −Th ∧ ∀x_{Sa} f(x_{Sa})< −Fr  ∧
∀x_{Su} f(x_{Su})< −Sa
8) ∀x_{D} ∀y_{D} (x_{D}< −| LL ∧ Lies(lion, x_{D}, y_{D}) ⇒ y_{D}< −LL)
9) ∀x_{D} ∀y_{D} (x_{D}< −| LL ∧ ¬Lies(lion, x_{D}, y_{D}) ⇒ y_{D}< −| LL)
10) ∀x_{D} ∀y_{D} (x_{D}< −LL ∧ Lies(lion, x_{D}, y_{D}) ⇒ y_{D}< −| LL)
11) ∀x_{D} ∀y_{D} (x_{D}< −LL ∧ ¬Lies(lion, x_{D}, y_{D}) ⇒ y_{D}< −LL)
12) ∀x_{D} ∀y_{D} (x_{D}< −| LU ∧ Lies(uni, x_{D}, y_{D}) ⇒ y_{D}< −LU)
13) ∀x_{D} ∀y_{D} (x_{D}< −| LU ∧ ¬Lies(uni, x_{D}, y_{D}) ⇒ y_{D}< −| LU)
14) ∀x_{D} ∀y_{D} (x_{D}< −LU ∧ Lies(uni, x_{D}, y_{D}) ⇒ y_{D}< −| LU)
15) ∀x_{D} ∀y_{D} (x_{D}< −LU ∧ ¬Lies(uni, x_{D}, y_{D}) ⇒ y_{D}< −LU)
16) ∃x_{D} (Lies(lion, x_{D}, f(x_{D})) ∧ Lies(uni, x_{D}, f(x_{D})))

Comparing our formalization given so far with the formalization in [OSS85], we have replaced the MEMBER predicate by the < − relation and we have tried to express as much as possible in terms of sort.

Example 3.3.3 (Condensed Detachment) Condensed detachment is an inference rule that combines modus ponens and instantiation [Mer77]. The general technique is to code various problems into the term structure of first-order logic. Thus we only need one predicate symbol P expressing “is a theorem”. Solving examples of this form with an automated theorem prover can be arbitrarily hard [MW92]. The example shown here is from the two-valued sentential calculus, where the 2place function i denotes implication and the 1-place function n negation. We give an unsorted formalization:

1) ∀x, y (P (i(x, y)) ∧ P (x) ⇒ P (y))

2) ∀x, y, z P (i(i(x, y), i(i(y, z), i(x, z))))

3) ∀x P (i(i(n(x), x), x))

4) ∀x, y P (i(x, i(n(x), y)))

5) ∀x P (i(x, x))

We will prove that ( 1 ∧ 2 ∧ 3 ∧ 4) ⇒ 5.

3.4 Relativization

In this subsection we show how to transform formulas of L_{S} into unsorted firstorder logic. This is useful for two reasons. Firstly, the aim of our approach is not to develop a more expressive logic than unsorted first-order logic, but a sorted first-order logic which can deal with taxonomic information in a more efficient way. Secondly, if we can prove that the semantic and syntactic notations of both logics are equivalent well known results from unsorted first-order logic can be taken over. Therefore, we prove the model theoretic part of the sort theorem which states the equivalence of the logics.

The transformation of the formulas will be done in two steps. The first step of the transformation eliminates variables which have not sort ⊤. Then we use the standard method [Wal87] to provide a unary predicate for each sort symbol and to add the formula ∀x ⊤(x) to axiomatize the top sort.

Lemma 3.4.1 (Simple Properties) Let F be a formula, ℑ be an interpretation and S a sort symbol, then:

• ℑ ⊧ ∀x_{S} F  iff ℑ ⊧ ∀x_{⊤} (x_{⊤}< −S ⇒ {x_{S} ↦x_{⊤}}F) x_{⊤}∉F V (F)
• ℑ ⊧ ∃x_{S} F  iff ℑ ⊧ ∃x_{⊤} (x_{⊤}< −S ∧ {x_{S} ↦x_{⊤}}F) x_{⊤}∉F V (F)

Proof: Can easily be seen by exploiting the semantics. □

Algorithm 3.4.2 (Ψ: Eliminating variables with sorts different from ⊤) We will now present an algorithm Ψ, which uses the equivalences of Lemma 3.4.1 to eliminate variables with sorts different from ⊤. We present our algorithms in terms of nondeterministic rules, because this gives a better understanding of their properties and the fundamental ideas.

• Ψ(∀x_{S} F)  → ∀x_{⊤} (x_{⊤}< −S ⇒ {x_{S} ↦x_{⊤}}Ψ(F)) x_{⊤}∉F V (F)
• Ψ(∃x_{S} F)  → ∃x_{⊤} (x_{⊤}< −S ∧ {x_{S} ↦x_{⊤}}Ψ(F)) x_{⊤}∉F V (F)
• Ψ(¬F)  → ¬Ψ(F)
• Ψ(F ⋆ G)  → Ψ(F) ⋆ Ψ(G) with  ⋆∈{⇔, ⇒, ∧, ∨}
• Ψ(P (t_{1}, …, t_{n}))  → P (t_{1}, …, t_{n})
• Ψ(t< −S)  → t< −S

Using Lemma 3.4.1 we find that Ψ(F) is logically equivalent to F for every formula F. Obviously, Ψ terminates and Ψ(F) contains only variables of sort ⊤.

Before we show the transformation of our logic into first-order logic we have to give a brief introduction. Mainly the syntax and semantics of the logics are the same. The only differences are the sort symbols and the special relation < −. Therefore we use similar syntactic and semantic notions by adding ′ to predicate and function symbols of our logic. The sort symbols attached to variables are omitted. All this leads to the corresponding symbols of unsorted first-order logic.

Definition 3.4.3 (Unsorted First-Order Logic) The first-order signature Σ′ is given by Σ′: = (V′, F′, P′). Terms, atoms, literals and formulas are built in the usual way. An interpretation ℑ′ = (M′, φ′) consists of a Σ′-structure M′ and a total Σ′-assignment φ′: V′ → U which can be naturally extended to terms. The Σ′-structure M′ consists of a non empty universe U, a total function fU^{′}: U^{n} → U for each n-place function symbol f′∈F′_{n} and a n-place relation P′_{M′} ⊆ U^{n} for each predicate symbol P′∈P′_{n}. The evaluation of terms, atoms, literals, and formulas is straightforward.

Algorithm 3.4.4 (Φ: Transformation into Unsorted First-Order Logic) Let Σ: = (S, V, F, P) be a sorted signature and F be a Σ-sentence. Then the corresponding Σ′-signature is given by Σ′: = (V′, F′, P′) where V′ is a countably infinite set of variable symbols, F′: = { f′ | f′ is a new n-place function symbol for every f∈F_{n} } and P′: = { P′ | P′ is a new n-place predicate symbol for every P ∈P_{n} } ∪ { S′ | S′ is a new 1-place predicate for every sort S∈S }. The algorithm Π translates Σ-expressions in Σ′-expressions:

• Π(f(t_{1}, …, t_{n}))  → f′(Π(t_{1}), …, Π(t_{n}))
• Π(Qx_{⊤} F)  → Qx Π(G)

where Q∈{∀, ∃} and G is obtained by replacing every free occurrence of x_{⊤} in F by x

• Π(¬F)  → ¬Π(F)
• Π(F ⋆ G)  → Π(F) ⋆ Π(G) with ⋆∈{⇔, ⇒, ∧, ∨}
• Π(P (t_{1}, …, t_{n}))  → P′(t′_{1}, …, t′_{n})

• Π(t< −S)  → S′(t′)

Then the corresponding set of Σ′-sentences is:

Φ(F) = Π(Ψ(F)) ∪ {∀x ⊤′(x)}

Theorem 3.4.5 (Sort Theorem) Let F be a sentence of L_{S}. Then F has a Σmodel iff Φ(F) has a Σ′-model. Proof: It suffices to show that Ψ(F) has a Σ-model iff Φ(F) has a Σ′-model, because Ψ(F) is equivalent to F according to Lemma 3.4.1

“⇒” Let ℑ = (M, φ) be a Σ-model for Ψ(F). Then we construct a Σ′-model ℑ′ as follows: U: = A, functions and predicates are interpreted in M′ as they are interpreted in M and the added unary predicates S′_{i} for the sort symbols are given by (S′_{i})_{M′}: = (S_{i})_{A}. Especially (⊤′)_{M′}: = A. Obviously U is not empty and ℑ′ ⊧ ∀x ⊤′(x). Thus we only have to show by induction on the structure of formulas, that ℑ ⊧ Ψ(F) implies ℑ′ ⊧ Π(Ψ(F)). We prove the non trivial parts only.

• Ψ(F) = P (t_{1}, …, t_{n}) for a n-place predicate symbol P ∈P_{n}, then ℑ ⊧ P (t_{1}, …, t_{n}) implies ℑ′ ⊧ P′(t′_{1}, …, t′_{n}), because ℑ(P) = ℑ′(P′) and ℑ(t_{i}) = ℑ′(t′_{i}) for every i by construction and by defining φ′(x): = φ(x) for all x∈V (P (t_{1}, …, t_{n})).

• Ψ(F) = ∀x_{⊤} (x_{⊤}< −S ⇒ G), then ℑ ⊧ ∀x_{⊤} (x_{⊤}< −S ⇒ G) implies ℑ′ ⊧ ∀x (S′(x) ⇒ G′), because U = ⊤_{A} and we have (M, φ[{x_{⊤}/a}]) ⊧ x_{⊤}< −S ⇒ G for all a∈⊤_{A} implies (M′, φ′[{x/a}]) ⊧ S′(x) ⇒ G′ by induction hypothesis. The case Ψ(F) = ∃x_{⊤} (x_{⊤}< −S ∧ G) is similar to this one.

“⇐” Let ℑ′ = (M′, φ′) be a Σ′-model for Φ(F). Then we construct a Σ-model ℑ as follows: the Σ-algebra A is defined with carrier A = ⊤′_{M′} = U. A is not empty because U is not empty. For every n-place function symbol f∈F_{n}, (u_{1}, …, u_{n})∈A^{n} we define f_{A}(u_{1}, …, u_{n}) = f′_{M′}(u_{1}, …, u_{n}). For every sort symbol S∈S the set S′_{M′} is assigned. S_{A} ⊆ A because of ℑ′ ⊧ ∀x ⊤′(x). For every n-place predicate symbol P ∈P_{n} we assign the relation P_{M}: = P′_{M′}. Finally we show by induction on the structure of formulas, that ℑ′ ⊧ Π(Ψ(F)) implies ℑ ⊧ Ψ(F).

• Π(Ψ(F)) = P′(t′_{1}, …, t′_{n}) for a n-place predicate symbol P′∈P′_{n}, then ℑ′ ⊧ P′(t′_{1}, …, t′_{n}) implies ℑ ⊧ P (t_{1}, …, t_{n}), because the fact that Π(Ψ(F)) is a sentence of a special form ensures that φ′(x)∈(sort(x))_{A} for all x∈V (P′(t′_{1}, …, t′_{n}))

• Π(Ψ(F)) = S′(t′) then ℑ′ ⊧ S′(t′) implies ℑ ⊧ t< −S by construction and the above argumentation for the interpretation of t′.

• Π(Ψ(F)) = ∀x (S′(x) ⇒ G′) then ℑ′ ⊧ ∀x (S′(x) ⇒ G′) implies ℑ ⊧ ∀x_{⊤} (x_{⊤}< −S ⇒ G) because a∈S′_{M′} implies a∈S_{A} and the induction hypothesis for G′ and S′(x) holds. The case Π(Ψ(F)) = ∃x (S′(x) ∧ G′) is similar to this case.

□

Theorem 3.4.6 (Compactness Theorem) A set F of L_{S} sentences is satisfiable iff every finite subset F′ of F is satisfiable. Proof: Follows from Theorem 3.4.5 and the fact that the Compactness Theorem holds for first-order logic. □

Clause Normal Form

4.1 Introduction

Resolution based deduction systems usually require a certain normal form of formulas, called “clause normal form”. In clause normal form negation symbols do only occur in front of predicate symbols, all variables are universally quantified and the whole formula is a conjunction of disjunctions, called clauses. In most sorted logics, the process of transforming a formula into clause normal form is very similar to the unsorted case, because they do not allow for empty sorts and declarations inside the formula. In L_{S}, this is all possible. Therefore, transformations have to be realized more carefully.

The main differences between the standard algorithms [CL73, Lov78, SS89] and our algorithm are as follows. Firstly, sets may be empty and therefore some standard transformation rules don’t hold, e.g. the rule for extending the scope of a universal quantifier. ∀x_{S} F ∧ G is not equivalent to ∀x_{S} (F ∧ G), where x_{S} occurs free in F. Consider an interpretation ℑ where S_{A} = ∅ and ℑ⊧ / G. Then ℑ ⊧ ∀x_{S} (F ∧ G) but ℑ⊧ / ∀x_{S} F ∧ G. Secondly, Skolemization doesn’t work in the usual way, because information about the domain and range sorts of a Skolem function has to be locally provided. In other sorted logics [SS89] the sort information of a Skolem function can be globally declared, but the example below shows that this does lead to an incorrect transformation in our logic. The formula (∃x_{S} P (x_{S}) ∨ Q(a)) ∧ ∀x_{S} x_{S}< −| S has a model, but the naive global skolemization (P (b) ∨ Q(a)) ∧ ∀x_{S} x_{S}< −| S ∧ b< −S has no model, whereas the local Skolemization ((P (b) ∧ b< −S) ∨ Q(a)) ∧ ∀x_{S} x_{S}< −| S preserves satisfiability. The necessity for doing local Skolemization results from the combination of allowing empty sorts on the semantic level and negative sort information on the syntactic one.

4.2 The CNF Algorithm

Definition 4.2.1 (Normal Forms) A formula F is said to be in negation normal form, if every negation symbol occurring in F stands directly in front of a predicate symbol. F is in clause normal form, if F is in negation normal form and F = F_{1} ∧ … ∧ F_{n}, where the F_{i} = ∀y_{S_{1}}, …, y_{S_{n}} (L_{1} ∨ … ∨ L_{n}) , the L_{i} are literals and V ({L_{1}, …, L_{n}}) = {y_{S_{1}}, …, y_{S_{n}}}

Algorithm 4.2.2 (Δ: Transformation in Clause Normal Form) The input of the algorithm Δ is a sorted logic sentence F, which is transformed into a set of clauses Δ(F). Δ includes seven steps which are applied incrementally. A step is finished if none of its rules is applicable.

Step1: Use the rules

• F ⇔ G → (F ⇒ G) ∧ (G ⇒ F)

• F ⇒ G → ¬F ∨ G

to eliminate implications and equivalences. Note that the two rules establish a naive equivalence elimination, because formulas may grow exponentially in size and are highly redundant after performing the elimination. Here standard techniques as described in [Soc90, Soc91] can be applied.

Step2: Use the rules

• ¬∀x_{S} F → ∃x_{S} ¬F

• ¬∃x_{S} F → ∀x_{S} ¬F

• ¬(F ∧ G) → ¬F ∨ ¬G

• ¬(F ∨ G) → ¬F ∧ ¬G

• ¬(¬F) → F

to move the negation sign inwards.

Step3: Use the rules

• ∀x_{S} (F ∨ G) → ∀x_{S} F ∨ G x_{S}∉F V (G)

• ∃x_{S} (F ∧ G) → ∃x_{S} F ∧ G x_{S}∉F V (G)

• ∀x_{S} (F ∧ G) → ∀x_{S} F ∧ ∀x_{S} G x_{S}∈F V (F) and x_{S}∈F V (G)

• ∃x_{S} (F ∨ G) → ∃x_{S} F ∨ ∃x_{S} G x_{S}∈F V (F) and x_{S}∈F V (G)

• ∀x_{S} ∀y_{T} (F ∨ G) → ∀y_{T} ∀x_{S} (F ∨ G) y_{T} ∈F V (F) and y_{T} ∈F V (G), but either x_{S}∉F V (F) or x_{S}∉F V (G)

• ∃x_{S} ∃y_{T} (F ∧ G) → ∃y_{T} ∃x_{S} (F ∧ G)

y_{T} ∈F V (F) and y_{T} ∈F V (G), but either x_{S}∉F V (F) or x_{S}∉F V (G)

to move the quantifiers inwards. These rules are not necessary for Skolemization, but are useful to get small Skolem functions, which increase efficiency of the refutation process.

Step4: Rename all variables, such that different quantifiers have different variables.

Step5: From left to right remove all existential quantifiers. Let F = ∃x_{S} G be the formula of the current existential quantifier. Let ∀y_{S_{1}} … ∀y_{S_{n}} be the universal quantifiers which have F in their scope. Then replace F by ({x_{S} ↦f(y_{S_{1}}, …, y_{S_{n}})}G ∧

f(y_{S_{1}}, …, y_{S_{n}})< −S) where f is a new n-place Skolem function. If we have S = ⊤, we can skip the declaration f(y_{S_{1}}, …, y_{S_{n}})< −S.

Step6: Use the rules

• H ∨ (F ∧ G) → (H ∨ F) ∧ (H ∨ G)

• ∀x_{S} (F ∧ G) → ∀x_{S} F ∧ ∀x_{S} G

• (∀x_{S} F) ∨ G → ∀x_{S} (F ∨ G)

and variable renaming to transform the formula into the form F = F_{1} ∧ … ∧ F_{n}, where the F_{i} = ∀x_{S_{1}} … ∀x_{S_{n}} L_{1} ∨ … ∨ L_{m} and the L_{i} are literals. Again the rule may grow the formula exponentially in size. The growing can be prevented by introducing new predicates regarded as abbreviations for subformulas.

Step7: Use the rule

• ∀x_{S_{1}} … ∀x_{S_{n}} (L_{1} ∨ … ∨ L_{m}) → ∀x_{S_{1}} … ∀x_{S_{i−1}} ∀x_{⊤} ∀x_{S_{i+1}} ∀x_{S_{n}} (L_{1} ∨ … ∨ L_{m} ∨ x_{⊤}< −| S_{i}) where x_{S_{i}} ∉F V (L_{1} ∨ … ∨ L_{m}) and x_{⊤} is a new variable

to ensure that a variable occurs in a disjunction L_{1} ∨ … ∨ L_{m} iff it occurs in the universal quantifiers in front of the disjunction. After having applied the above rule, we reach the clause normal form of the input formula.

The rule can be further improved. We only need to add the additional literals of the form x_{⊤}< −| S for variables x_{S}, if no different variable of sort S is bound by the universal quantifier. For example the formula ∀x_{S}, y_{S} P (x_{S}) can be transformed into ∀x_{S} P (x_{S}).

Now we can drop the quantifiers and switch to the clause oriented notation by transforming all disjunctions into clauses and the whole conjunction in a set of clauses.

Note that dropping the quantifiers and assuming all variables to be universally quantified is not a correct operation if the disjunctions of Step6 contain free variables or there are variables which do not occur in the literals of a disjunction but in the universal quantifiers. For example the formula ∀x_{S} P (a) ∧ ¬P (a) has a model, but P (a) ∧ ¬P (a) is unsatisfiable. Also ∀x_{S} (P (x_{S}) ∨ Q(y_{T})) ∧ ¬P (a) ∧ ¬Q(b) ∧ a< −S ∧ b< −T is satisfiable, but dropping the quantifiers and assuming all variables to be universally quantified leads to an unsatisfiable formula. Therefore we demand sentences to be the input of Δ.

Example 4.2.3 (Applying Δ) The following example demonstrates the transformation of the complicated theorem formula of Example 3.3.1 in clause normal form.

¬(∃x_{A} ∃y_{A} (E(x_{A}, y_{A}) ∧ ∀x_{G} E(y_{A}, x_{G})))

→^{⋆} ∀x_{A} ∀y_{A} (¬E(x_{A}, y_{A}) ∨ ∃x_{G} ¬E(y_{A}, x_{G}))

using the rules of Step2

→ ∀y_{A} ∀x_{A} (¬E(x_{A}, y_{A}) ∨ ∃x_{G} ¬E(y_{A}, x_{G}))

using Step3, fifth rule

→ ∀y_{A} (∀x_{A} ¬E(x_{A}, y_{A}) ∨ ∃x_{G} ¬E(y_{A}, x_{G}))

using Step3, first rule

→ ∀y_{A} (∀x_{A} ¬E(x_{A}, y_{A}) ∨ (¬E(y_{A}, f(y_{A})) ∧ f(y_{A})< −G))

using Step5 where f is a new 1-place Skolem function. Without having applied the rules of Step3 we would have got a 2-place Skolem function

→ ∀y_{A} ((∀x_{A} ¬E(x_{A}, y_{A}) ∨ ¬E(y_{A}, f(y_{A}))) ∧ (∀z_{A} ¬E(z_{A}, y_{A}) ∨ f(y_{A})< −G)) using Step6, first rule and variable renaming

→ ∀y_{A} (∀x_{A} ¬E(x_{A}, y_{A}) ∨ ¬E(y_{A}, f(y_{A}))) ∧ ∀u_{A} (∀z_{A} ¬E(z_{A}, u_{A}) ∨ f(u_{A})< −G) using Step6, second rule and variable renaming

→^{⋆} ∀y_{A} ∀x_{A} (¬E(x_{A}, y_{A}) ∨ ¬E(y_{A}, f(y_{A}))) ∧ ∀u_{A} ∀z_{A} (¬E(z_{A}, u_{A}) ∨ f(u_{A})< −G)

using Step6, third rule

→ {{¬E(x_{A}, y_{A}), ¬E(y_{A}, f(y_{A}))} , {¬E(z_{A}, u_{A}), f(u_{A})< −G}}

using Step7

Example 4.2.4 (Schubert’s Steamroller) We present the set of clauses obtained from applying the algorithm to the formulas presented in Example 3.3.1. The theorem was negated.

(1) {x_{W} < −A}  (2) {x_{F} < −A}  (3) {x_{B}< −A}
(4) {x_{C}< −A}  (5) {x_{S}< −A}  (6) {lupo< −W }
(7) {foxy< −F }  (8) {tweety< −B}  (9) {raupy< −C}
(10) {schnecky< −S} (11) {muesli< −G}  (12) {x_{G}< −P }
(13) {E(x_{A}, y_{P}), ¬M(z_{A}, x_{A}), ¬E(z_{A}, v_{P}), E(x_{A}, z_{A})}
(14) {M(x_{C}, z_{B})} (15) {M(y_{S}, z_{B})}  (16) {M(z_{B}, x_{F})}
(17) {M(x_{F} , y_{W})} (18) {¬E(z_{W} , y_{F})} (19) {¬E(z_{W} , x_{G})}
(20) {E(x_{B}, y_{C})}  (21) {¬E(x_{B}, z_{S})} (22) {E(x_{C}, f(x_{C}))}
(23) {f(x_{C})< −P }  (24) {E(x_{S}, g(x_{S}))} (25) {g(x_{S})< −P }
(26) {¬E(x_{A}, y_{A}), ¬E(y_{A}, z_{G})}

Example 4.2.5 (The Lion and the Unicorn) We present the set of clauses obtained by applying the algorithm to the formulas presented in Example 3.3.2. The theorem was negated.

(1) {mon< −Mo}  (2) {tue< −Tu}  (3) {wed< −We}
(4) {thu< −Th}  (5) {fri< −Fr}  (6) {sat< −Sa}
(7) {sun< −Su}  (8) {x_{Mo}< −LL}  (9) {x_{Tu}< −LL}
(10) {x_{We}< −LL}  (11) {x_{Th}< −| LL}  (12) {x_{Fr}< −| LL}
(13) {x_{Sa}< −| LL}  (14) {x_{Su}< −| LL}  (15) {x_{Th}< −LU}
(16) {x_{Fr}< −LU}  (17) {x_{Sa}< −LU}  (18) {x_{Su}< −| LU}
(19) {x_{Mo}< −| LU} (20) {x_{Tu}< −| LU}  (21) {x_{We}< −| LU}
(22) {x_{Mo}< −D}  (23) {x_{Tu}< −D}  (24) {x_{We}< −D}
(25) {x_{Th}< −D}  (26) {x_{Fr}< −D}  (27) {x_{Sa}< −D}
(28) {x_{Su}< −D}  (29) {x_{LL}< −D}  (30) {x_{LU} < −D}
(31) {lion< −C}  (32) {uni< −C}  (33) {f(x_{Mo})< −Su}
(34) {f(x_{Tu})< −Mo} (35) {f(x_{We})< −Tu} (36) {f(x_{Th})< −We}
(37) {f(x_{Fr})< −Th} (38) {f(x_{Sa})< −Fr} (39) {f(x_{Su})< −Sa}
(40) {x_{D}< −LL, ¬Lies(lion, x_{D}, y_{D}), y_{D}< −LL}
(41) {x_{D}< −LL, Lies(lion, x_{D}, y_{D}), y_{D}< −| LL}
(42) {x_{D}< −| LL, ¬Lies(lion, x_{D}, y_{D}), y_{D}< −| LL}
(43) {x_{D}< −| LL, Lies(lion, x_{D}, y_{D}), y_{D}< −LL}
(44) {x_{D}< −LU, ¬Lies(uni, x_{D}, y_{D}), y_{D}< −LU}
(45) {x_{D}< −LU, Lies(uni, x_{D}, y_{D}), y_{D}< −| LU}
(46) {x_{D}< −| LU, ¬Lies(uni, x_{D}, y_{D}), y_{D}< −| LU}
(47) {x_{D}< −| LU, Lies(uni, x_{D}, y_{D}), y_{D}< −LU}
(48) {¬Lies(lion, x_{D}, f(x_{D})), ¬Lies(uni, x_{D}, f(x_{D}))}

Example 4.2.6 (Condensed Detachment) We present the set of clauses obtained by applying the algorithm to the formulas presented in Example 3.3.3. The theorem is negated.

\begin{matrix}(1) & \{¬P (i(x, y)), ¬P (x), P (y)\} \\ (2) & \{P (i(i(x, y), i(i(y, z), i(x, z))))\} \\ (3) & \{P (i(i(n(x), x), x))\} \\ (4) & \{P (i(x, i(n(x), y)))\} \\ (5) & \{¬P (i(a, a))\} \end{matrix}

We can use the CNF-algorithm in order to transform unsorted formulas also, if the top sort ⊤ is attached to all variables of the problem.

4.3 Properties of Δ

We prove that the usual properties of CNF-algorithms also hold for Δ. The termination of the algorithm can be shown by assigning an appropriate measure to every step, which decreases with every rule application. We can easily show by contradiction that Δ(F) is in clause normal form for every sorted logic sentence F. Now we focus on the remaining logical properties of Δ.

Lemma 4.3.1 (Correctness of Replacing Positive Components) If F is a positive component of a formula G and G′ is obtained from G by replacing F in G by a formula F′ and if there is a model ℑ for the set of formulas {G, F ⇒ F′}, then G′ has model ℑ. Proof: The proof is a direct extension of the proof in [Lov78]. □

Theorem 4.3.2 (Soundness and Completeness of Δ) Let F be a sentence. Then F has a model ℑ iff Δ(F) has a model ℑ′. Proof: Except for Step5, both parts of each conversion rule are equivalent, so for these rules there is nothing to show. It remains to consider the elimination of the existential quantifiers. Wlog. we can assume that there is only one Skolemization step. Let G = ∃x_{S} H be the formula with the existential quantifier being eliminated, ∀y_{S_{1}} … ∀y_{S_{n}} be the universal quantifiers which have G in their scope and G′ = {x_{S} ↦ f(y_{S_{1}}, …, y_{S_{n}})}H ∧ f(y_{S_{1}}, …, y_{S_{n}})< −S be the formula obtained from G after elimination of the existential quantifier. “⇒” Let ℑ = (M, φ) be a model for F, (S_{i})_{A} ≠ ∅ for every i and (M, φ[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}}]) ⊧ ∃x_{S} H for an arbitrary Σ-assignment φ[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}}] with a_{i}∈(S_{i})_{A} for all i. We will now extend ℑ to a model ℑ′ which satisfies Δ(F). If ∃x_{S} H holds, there must be an a∈S_{A}, such that (M, φ[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}, x_{S}/a}]) ⊧ H. Now define ℑ′ like ℑ except that f_{A}(a_{1}, …, a_{n}) = a. Thus we have ℑ′ ⊧ {F, G ⇒ G′} and together with Lemma 4.3.1 we conclude ℑ′ ⊧ Δ(F). “⇐” Let ℑ′ = (M′, φ′) be a model for Δ(F), (S_{i})_{A} ≠ ∅ for every i and (M′, φ′[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}}]) ⊧ G′ for a Σ-assignment φ′[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}}] with a_{i}∈(S_{i})_{A} for all i. Then f_{A}(a_{1}, …, a_{n})∈S_{A}. Therefore ℑ′ ⊧ ∃x_{S} H and application of Lemma 4.3.1 proves the theorem. □

The Basic Resolution Calculus

In this section we will develop a sound and complete resolution calculus for sorted logic. From the computational point of view the question is how the sort information can be used to reduce the number of possible resolution steps and how to deal with taxonomic information in an efficient way. There are lots of answers to this question for standard sorted logics [SS89]. At first sight these results don’t apply here, because in L_{S} the sort information is part of the formulas itself and therefore any question concerning the structure of the sort information is undecidable and can e.g. not be attacked by efficient sorted unification algorithms. So our first answer to the question how the sort information can be exploited is a basic calculus which uses unsorted unification.

In the next chapter we will show how sorted unification can be established in this dynamic environment.

5.1 The Herbrand Theorem

The development of the calculus will be done by the usual two steps. First we investigate the ground case and then lift this result to the general case.

Before defining the ground term structure we should make a remark on the sort ⊤. The clause set {{a< −| ⊤}} is unsatisfiable, because every object is of sort ⊤. This implies that we should be able to refute this clause set. As the standard resolution rule does not apply to one literal we introduce the ⊤-reduction rule which allows to delete literals of the form t< −| ⊤.

As well sortedness is not decidable in our logic, we have to change the usual instantiation rule. The idea is to add a literal of the form t< −| S for every variable x_{S} which is replaced by a term t. A ground instance of the clause {P (x_{S})} is {P (a), a< −| S} applying the ground substitution {x_{S} ↦ a}. The intuitive semantics of the clause is “if a is an element of sort S, then P (a) holds”. From an unsorted point of view we just delay the introduction of the sort literals. The unsorted formalization of {P (x_{S})} is {P (x), ¬S′(x)} which yields {P (a), ¬S′(a)} using the unsorted substitution {x↦a} and the unsorted instantiation rule.

Definition 5.1.1 (Conditioned Literals) Let σ be a substitution. Then the set of conditioned literals Cond(σ) of σ is defined as Cond(σ): = { (t< −| T) | there is an x_{T} ∈DOM(σ) with σ(x_{T}) = t }.

Definition 5.1.2 (Conditioned Instantiation of Clauses) Let C = {L_{1}, …, L_{n}} be a clause and σ a substitution. Then σ↓C: = {σ(L_{1}), …, σ(L_{n})} ∪ Cond(σ) is called a conditioned instance of C.

The conditional literals of the form t< −| T handle the case that σ is not well sorted, i.e. in some interpretation ℑ, ℑ(t)∉ℑ(T). So either for every variable x_{T} ∈DOM(σ), ℑ(σ(x_{T}))∈ℑ(T) or some of the added literals become true.

Lemma 5.1.3 (Soundness of Conditioned Instantiation) For every interpretation ℑ, substitution σ and clause C, ℑ ⊧ ∀ (C) implies ℑ ⊧ ∀ (σ↓C). Proof: We prove the lemma by induction on the number of variables in DOM(σ): |DOM(σ)| = 0: σ↓C = C and therefore the lemma holds trivially. |DOM(σ)| = n + 1: let x_{S}∈DOM(σ) with σ(x_{S}) = t. If x_{S}∉V (C) then σ[x_{S}]↓ C ⊆ σ↓C and the lemma is proven by induction hypothesis. So assume x_{S}∈V (C), V (σ↓C) = {y_{S_{1}}, …, y_{S_{n}}} and ℑ = (M, φ) is a model for ∀ (C). If S_{A} = ∅, then ℑ ⊧ (t< −| S) and because (t< −| S)∈(σ ↓C) we conclude ℑ ⊧ σ ↓C. If S_{A} ≠ ∅, let φ[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}}] be an arbitrary assignment for the variables of σ ↓ C. If φ[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}}](t)∉S_{A} we again have (M, φ[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}}]) ⊧ t< −| S and thus (M, φ[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}}]) ⊧ σ ↓C. If φ[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}}](t)∈S_{A} with φ[{y_{S_{1}}/a_{1}, …, y_{S_{n}}/a_{n}}](t) = a, then we conclude ℑ ⊧ ∀ (σ↓C), because ℑ ⊧ ∀ (σ[x_{S}]↓C) by induction hypothesis and a∈S_{A}. . □

Lemma 5.1.4 (Associativity of Conditioned Instantiation) Let σ, τ be two substitutions and C = {L_{1}, …, L_{n}} be a clause. If DOM(σ) ∩ DOM(τ) = ∅, then τ↓(σ↓C) = (τσ)↓C. Proof:

(τσ)↓C

= { (τσ)(L_{1}), …, (τσ)(L_{n})}∪{(t< −| T) | there is an x_{T} ∈DOM(τσ) with (τσ)(x_{T}) = t } according Definition 5.1.2

= { (τσ)(L_{1}), …, (τσ)(L_{n})} ∪ {τ(t< −| T) | there is an x_{T} ∈DOM(σ) with σ(x_{T}) = t } ∪ { (s< −| S) | there is an x_{S}∈(DOM(τ) \ DOM(σ)) with τ(x_{S}) = s } according Definition 2.2.6

= {(τσ)(L_{1}), …, (τσ)(L_{n})} ∪ { τ(t< −| T) | there is an x_{T} ∈DOM(σ) with σ(x_{T}) = t } ∪ { (s< −| S) | there is an x_{S}∈DOM(τ) with τ(x_{S}) = s } because DOM(σ) ∩ DOM(τ) = ∅ = τ↓({σ(L_{1}), …, σ(L_{n})} ∪ { t< −| T | there is an x_{T} ∈DOM(σ) with σ(x_{T}) = t })

according Definition 5.1.2

= τ↓(σ↓C)

□

Definition 5.1.5 (Herbrand Set of Clauses) Let F be a sentence, then the Herbrand clause set Δ(F)_{H} is defined as follows: Δ(F)_{H}: = { σ↓C | C∈Δ(F) and σ is a ground substitution with DOM(σ) = V (C) }

Definition 5.1.6 (Herbrand Interpretation) A Herbrand interpretation ℑ_{H} is a set ℑ_{H} of ground literals satisfying the following conditions:

• There are no literals L_{1} and L_{2} in ℑ_{H} which are equal as atoms but L_{1} is positive and L_{2} is negative or vice versa

• For every ground term t, t< −⊤ is in ℑ_{H}

A Herbrand model of a Herbrand clause set Δ(F)_{H}, is a Herbrand interpretation ℑ_{H} such that for every clause C_{H}∈Δ(F)_{H}: C_{H} ∩ ℑ_{H} ≠ ∅. If ℑ_{H} is a Herbrand model for a Herbrand clause set CS_{H}, we write ℑ_{H} ⊧ CS_{H} or ℑ_{H} ⊧ C_{H} for a clause C_{H}∈CS_{H}.

Lemma 5.1.7 (Compatibility of Σ-models and Herbrand models) Let F be a sentence, CS: = Δ(F) and CS_{H}: = Δ(F)_{H}. Then CS has a Σ-model ℑ iff CS_{H} has a Herbrand model ℑ_{H}. Proof: “⇒” Let ℑ = (M, φ) be a Σ-model for CS. Then ℑ_{H}: = { L | L is a ground literal and ℑ ⊧ L }. ℑ_{H} is a Herbrand interpretation. Now we prove by contradiction that ℑ_{H} is a Herbrand model for CS_{H}. Suppose there is a clause C_{H}∈CS_{H} with C_{H} ∩ ℑ_{H} = ∅. We know that C_{H} is an instantiation of a clause C∈CS. That means C = {L_{1}, …, L_{n}} and there exists a ground substitution σ = {y_{S_{1}} ↦ t_{1}, …, y_{S_{n}} ↦ t_{n}} with DOM(σ) = V (C) and σ↓C = C_{H}. If ℑ(t_{i})∉(S_{i})_{A} for some i, then ℑ ⊧ t_{i}< −| S_{i} and this contradicts C_{H} ∩ ℑ_{H} = ∅. So ℑ(t_{i})∈(S_{i})_{A} for all i. Therefore (M, φ[{y_{S_{1}}/ℑ(t_{1}), …, y_{S_{1}}/ℑ(t_{1})}])⊧ / C. But C is universally closed over the y_{S_{i}}, hence this contradicts the assumption that ℑ is a Σ-model for CS. “⇐” Let ℑ_{H} be a Herbrand model for CS_{H}. We construct a Σ-model as follows: The Σ-algebra A is defined with carrier A: = { t | t is a ground term }, for every sort S∈S a set S_{A}: = { t | (t< −S)∈ℑ_{H} } is assigned and for every f∈F_{n}, f_{A}(t_{1}, …, t_{n}): = f(t_{1}, …, t_{n}). Note that we have ⊤_{A} = A.

Next we define a Σ-structure M by adding P_{M}: = { (t_{1}, …, t_{n}) | P (t_{1}, …, t_{n})∈ℑ_{H} } for every P ∈P_{n}.What we have defined so far is a kind of initial model for CS which is based on a ground term algebra. So from now on we can drop the differences between terms and their interpretations. To finish the proof we show by contradiction that ℑ = (M, φ) is a Σ-model for CS.

Assume ℑ is not a Σ-model for CS. Then there is a clause C∈CS with ℑ⊧ / ∀ (C) Let V (C) = {y_{S_{1}}, …, y_{S_{n}}} be the variables occurring in C. As ℑ is not a model for C, we have (S_{i})_{A} ≠ ∅ for every i and there is a Σ-assignment φ[{y_{S_{1}}/t_{1}, …, y_{S_{n}}/t_{n}}] with t_{i}∈(S_{i})_{A} and (M, φ[{y_{S_{1}}/t_{1}, …, y_{S_{n}}/t_{n}}])⊧ / C. But there is a clause C_{H}∈CS_{H} with C_{H} = {y_{S_{1}} ↦ t_{1}, …, y_{S_{n}} ↦ t_{n}} ↓ C and ℑ_{H} ⊧ C_{H}. Thus there is at least one literal L which is both in C_{H} and ℑ_{H}. If L is a literal introduced by conditioned instantiation, we have a contradiction against Definition 5.1.6. If L is an instance of a literal occurring in C we have (M, φ[{y_{S_{1}}/t_{1}, …, y_{S_{n}}/t_{n}}]) ⊧ L and hence (M, φ[{y_{S_{1}}/t_{1}, …, y_{S_{n}}/t_{n}}]) ⊧ C contradicting the assumption that (M, φ[{y_{S_{1}}/t_{1}, …, y_{S_{n}}/t_{n}}])⊧ / C. □

Theorem 5.1.8 (Herbrand Theorem) Let F be a sentence, CS and CS_{H} be the above defined clause sets. Then CS is unsatisfiable iff there is a finite subset of CS_{H} which is unsatisfiable. Proof: “⇒” We show this part by contradiction. Assume CS is unsatisfiable and every finite subset of CS_{H} is satisfiable. Then because of Theorem 3.4.6, CS_{H} is satisfiable and with Lemma 5.1.7 CS is satisfiable, which contradicts our assumption. “⇐” If CS_{H} has a finite unsatisfiable subset, CS_{H} has no Herbrand model and with Lemma 5.1.7 CS has no Σ-model. □

5.2 Ground Resolution

The next step towards a sound and complete calculus is to define a resolution rule on ground level. For this rule we have to prove the soundness and completeness, i.e. we prove that a set of ground clauses is unsatisfiable iff there is a derivation of the empty clause using ground resolution. The only difference between the resolution calculus for the sorted logic and the resolution rule for unsorted first-order logic is a rule eliminating literals of the form t< −| ⊤.

Definition 5.2.1 (Ground Resolution Rule) Let C_{1} and C_{2} be ground clauses, L_{1}∈C_{1} and L_{2}∈C_{2}. If L_{1} and L_{2} are two complementary literals, then R_{g}(C_{1}, C_{2}, L_{1}, L_{2}): = (C_{1} \ {L_{1}}) ∪ (C_{2} \ {L_{2}}) is a ground resolvent of C_{1} and C_{2}.

Definition 5.2.2 (⊤-Reduction Rule) Let C be a ground clause containing a literal t< −| ⊤, then E_{g}(C, t< −| ⊤): = C \ {t< −| ⊤} is an ⊤-reduction of C.

Lemma 5.2.3 (Ground Resolution and ⊤-Reduction are Sound) Let C_{1} and C_{2} be ground clauses, L_{1}∈C_{1} and L_{2}∈C_{2}, L_{1} and L_{2} be complementary literals, then for every interpretation ℑ having ℑ ⊧ C_{1} and ℑ ⊧ C_{2}, ℑ ⊧ R_{g}(C_{1}, C_{2}, L_{1}, L_{2}) holds. If (t< −| ⊤)∈C_{1} then for every interpretation ℑ with ℑ ⊧ C_{1}, ℑ ⊧ E_{g}(C_{1}, t< −| ⊤) holds. Proof: The proofs are obvious. □

Lemma 5.2.4 (Unsatisfiability of Ground Unit Clauses) Let CS be an unsatisfiable set of ground unit clauses. Then CS is unsatisfiable iff CS contains two unit clauses with complementary literals or a clause {t< −| ⊤}. Proof: We will prove the following equivalent conjecture: a set CS of ground unit clauses has a Σ-model iff CS does not contain complementary literals and no literal t< −| ⊤. “⇒” If CS has a Σ-model, then by Lemma 5.1.7, CS has a Herbrand model and therefore CS does not contain complementary literals and no literal t< −| ⊤. “⇐” If CS does not contain complementary literals and no literal t< −| ⊤, then CS can be turned into a Herbrand model and using Lemma 5.1.7 we conclude that CS has a Σ-model. □

Lemma 5.2.5 (Ground Resolution and ⊤-Reduction are Complete) Let CS be an unsatisfiable set of ground clauses. Then there exists a derivation of the empty clause using ground resolution and ⊤-reduction. Proof: The lemma is proved by induction on the k-parameter [AB70], k(CS): = ∑ {|C| − 1 | C∈CS}, where |C| is the number of literals in the clause C. If k(CS) = 0, then from Lemma 5.2.4 we follow that CS contains two clauses with complementary literals or a clause {t< −| ⊤}. Hence one ground resolution step or one ⊤-reduction step yields the empty clause. If k(CS) > 0, then there exists a non-unit clause C. Doing a case analysis, we separate C into two parts C_{1} and C_{2} and obtain two unsatisfiable clause sets CS_{1} and CS_{2} by replacing C by C_{1} or C_{2}, respectively. Since k(CS_{i}) < k(CS), there are refutations of CS_{1} and CS_{2} by ground resolution. As all clauses are ground, these resolution proofs can be combined to a resolution proof of the empty clause in CS.

□

5.3 Unsorted Unification

After proving the soundness and completeness on the ground level, we will now show how to lift these results on the general level where we also deal with variables. One problem that arises is that if some terms are syntactically equal on ground level they need not to be equal on the general level. For example the ground literals P (f(a)), ¬P (f(a)) are syntactically equal if we disregard their sign. Suppose they stem from two literals P (x_{S}), ¬P (f(x_{T})) after applying the ground substitution σ = {x_{S} ↦f(a), x_{T} ↦a}. Clearly P (x_{S}) and ¬P (f(x_{T})) are not syntactically equal and the unification task is now to find a more general substitution which equals the literals.

Since unification works as in unsorted first-order logic, we give only a brief introduction to unification. A lot of efficient unification procedures are known, e.g. [PW78, MM82]. For reasons of simplicity we will present a rule based version of the Robinson [Rob65] unification procedure following [MM82]. We use the standard notions for unification [Sie89].

Definition 5.3.1 (Notions for Unification) Two objects (terms, atoms, literals) t_{1} and t_{2} are called unifiable, iff there exists a substitution σ such that σ(t_{1}) = σ(t_{2}). In this case the substitution σ is called a unifier of t_{1} and t_{2}. A unifier σ of two objects t_{1} and t_{2} is called an mgu (most general unifier), iff for every unifier λ of t_{1} and t_{2} there exists a substitution τ, such that τσ = λ. If L_{1} = P (t_{1}, …, t_{n}) and L_{2} = P (s_{1}, …, s_{n}) are two literals with no variables in common, then Γ = {t_{1} = s_{1}, …, t_{n} = s_{n}} is called the unification problem for L_{1} and L_{2}. A substitution σ solves 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_{S_{1}} = t_{1}, …, x_{S_{n}} = t_{n}} where the x_{S_{i}} are variables, x_{S_{i}} ∉V (t_{j}) and x_{S_{i}} ≠ x_{S_{j}} for every i and j.

Algorithm 5.3.2 (An Unsorted 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:

• ({x_{S} = x_{S}} ∪ Γ) → (Γ)

• ({f(t_{1}, …, t_{n}) = f(s_{1}, …, s_{n})} ∪ Γ) → ({t_{1} = s_{1}, …, t_{n} = s_{n}} ∪ Γ)

• ({x_{S} = t} ∪ Γ) → ({x_{S} = t} ∪ {x_{S} ↦t}Γ)

if x_{S} is a variable, t a non-variable term and x_{S}∉V (t), x_{S}∈V (Γ)

• ({t = x_{S}} ∪ Γ) → ({x_{S} = t} ∪ Γ)

if x_{S} is a variable and t a non-variable term

• ({f(t_{1}, …, t_{n}) = g(s_{1}, …, s_{m})} ∪ Γ) → STOP.FAIL if f ≠ g

• ({x_{S} = t} ∪ Γ) → STOP.FAIL if x_{S}∈V (t)

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 mgu of the term pairs (t_{1}, s_{1}), …, (t_{n}, s_{n}).

Assumption 5.3.3 (Properties of Unifiers) Note that every substitution σ corresponding to a unification problem Γ solved by the above unification algorithm is idempotent and introduces no new variables. So from now on we assume that unifiers are idempotent substitutions in the variables of the unified terms.

Lemma 5.3.4 (Relationship MGU and Ground Unifier) Let L_{1}, …, L_{n} be some atoms, σ a ground substitution with σ(L_{1}) = … = σ(L_{n}) and λ an mgu of the L_{i}. Then σλ = σ.

Proof: As λ is an mgu, we know the existence of a ground substitution τ with τλ = σ. Now we have σλ = τλλ = τλ = σ, where the second equation holds because λ is idempotent. □

5.4 General Resolution

The idea of the general resolution rule is to simulate every ground resolution step on the general level using unification. Thus the general resolution rule is similar to the ground rule, except that the syntactical equality of literals is not given in advance, but has to be produced by unification.

The idea of the completeness proof for general resolution is to simulate every step of the ground proof by a general resolution step. The problem that always arises at this point is the merging of literals on ground level. Consider the ground clause set

{{P (a), Q(a), a< −| S, a< −| T }, {¬P (a)}, {¬Q(a)}, {a< −T }, {a< −S}}

obtained from the clause set

{{P (x_{S}), P (x_{T}), Q(y_{S})}, {¬P (a)}, {¬Q(a)}, {a< −T }, {a< −S}}

using conditioned instantiation by the ground substitution

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

On ground level we can apply the ground resolution rule to the clauses {P (a), Q(a), a< −| S, a< −| T } and {¬P (a)} yielding the clause {Q(a), a< −| S, a< −| T }. On the general level we can compute the clauses {P (x_{T}), Q(y_{S}), a< −| S},{P (x_{S}), Q(y_{S}), a< −| T }, but both still contain a literal starting with predicate symbol P. What we need is a kind of merging rule on the general level. This rule is usually called “factorization” and allows the merging of literals having equal signs and predicate symbols by instantiation. Therefore we apply the factorization substitution τ = {x_{S} ↦ x_{T} } for our example first resulting in the clause {P (x_{T}), Q(y_{S}), x_{T} < −| S} and then perform the resolution step with {¬P (a)} yielding {Q(y_{S}), a< −| S, a< −| T }. This clause has the desired property of the corresponding ground resolvent {Q(a), a< −| S, a< −| T } being an instantiation of it.

The factorization problem is also well known from unsorted first-order logic. In L_{S} there are two more problems resulting from the conditioned literals. Let’s consider the above example again. On ground level we can perform a resolution step between the clauses {P (a), Q(a), a< −| S, a< −| T } and {a< −S} yielding {P (a), Q(a), a< −| T }. On the general level this step is not possible, because there is no complementary literal for a< −S in {P (x_{S}), P (x_{T}), Q(y_{S})}. Note that the literal a< −| S on ground level is introduced by conditioned instantiation. Thus we cannot lift every ground level step to the general level, but we will show that there is always an ordering on the ground level steps such that every step is liftable. Coming back to our example we first have to resolve between {P (x_{S}), P (x_{T}), Q(y_{S})} and {¬P (a)} yielding {Q(y_{S}), a< −| S, a< −| T }. Afterwards we can lift the resolution step using a< −S.

At this point the second problem occurs. The general resolvent of {Q(y_{S}), a< −| S, a< −| T } and {a< −S} is {Q(y_{S}), a< −| T }, but the corresponding ground resolvent {Q(a), a< −| T } is not a conditioned instance of the general clause. The corresponding conditioned instance would be {Q(a), a< −| T, a< −| S}. The reason for this divergence is the merging of two conditioned literals on ground level. In general this problem cannot be solved by reordering the resolution steps, so we may have to perform several steps on the general level to lift one ground level step.

Definition 5.4.1 (Factor) Let C = {L_{1}, …, L_{n}} be a clause, {L_{i}, L_{j}} ⊆ C (i ≠ j), and σ a mgu of {L_{i}, L_{j}}, i.e. σ(L_{i}) = σ(L_{j}), then F (C, L_{i}, L_{j}): = σ↓C is called a factor of C.

Lemma 5.4.2 (Factorization is Sound) If C = {L_{1}, …, L_{n}} is a clause and F (C, L_{i}, L_{j}) a factor of C for every interpretation ℑ having ℑ ⊧ ∀ (C), ℑ ⊧ ∀ (F (C, L_{i}, L_{j})) holds. Proof: Follows from Lemma 5.1.3 □

Definition 5.4.3 (General Resolution Rule) Let C_{1} and C_{2} be two clauses with no variables in common, L∈C_{1} and K∈C_{2}. If there exists an mgu σ of L and K, such that σ(L) and σ(K) become two complementary literals then

R(C_{1}, C_{2}, L, K): = σ↓((C_{1} \ {L}) ∪ (C_{2} \ {K}))

is a resolvent of C_{1} and C_{2}.

Definition 5.4.4 (General ⊤-Reduction Rule) Let C be a clause and (t< −| ⊤)∈C, then

E(C, t< −| ⊤): = (C \ {t< −| ⊤}) ∪ {x_{S}< −| S | x_{S}∈V (t), S ≠ ⊤}

is called a ⊤-Reduction of C.

Lemma 5.4.5 (Resolution and ⊤-Reduction are Sound) Let C_{1} and C_{2} be two clauses with no variables in common, L∈C_{1} and K∈C_{2}. If resolution using the literals L and K is possible then for every interpretation ℑ having ℑ ⊧ ∀ (C_{1}) and ℑ ⊧ ∀ (C_{2}), ℑ ⊧ ∀ (R(C_{1}, C_{2}, L, K)) holds. If (t< −| ⊤)∈C_{1} then for every interpretation ℑ with ℑ ⊧ ∀ (C_{1}), ℑ ⊧ ∀ (E(C_{1}, t< −| ⊤)) holds. Proof: For the resolution rule we have: for every interpretation ℑ, ℑ ⊧ σ(L) and ℑ ⊧ σ(K) do not hold both. Thus together with Lemma 5.4.2 and Lemma 5.1.3 we obtain the desired result.

For the ⊤-reduction rule we know that ℑ ⊧ ∀ (t< −| ⊤) iff there is at least one variable x_{S}∈V (t) such that S_{ℑ} = ∅ iff ℑ ⊧ ∀x_{S} x_{S}< −| S. □

Lemma 5.4.6 (Refutations yield ground substitutions) Let CS be a set of clauses such that different clauses are variable disjoint. If CS can be refuted by resolution, i.e. the empty clause can be derived, then the resulting overall substitution is a ground substitution. Proof: by induction on the number n of resolution steps. n = 1 The only possibility for a one step refutation are two ground unit clauses or a clause {t< −| ⊤}. n > 1 Let us choose an arbitrary resolution step of the refutation between clauses C_{1} and C_{2}, literals L,K and substitution σ, according Definition 5.4.3. By induction hypothesis the refutation using CS ∪ R(C_{1}, C_{2}, L, K) yields a ground substitution τ for the variables of the clauses used in the refutation. Now assume for a variable x_{S}∈(V (C_{1}) ∪ V (C_{2})) that x_{S}∉DOM(τ). Then x_{S}∈DOM(σ), with σ(x_{S}) = t and (t< −| S)∈R(C_{1}, C_{2}, L, K). Thus x_{S} is substituted by the ground term τ(t).

The same argumentation holds for a factorization or an ⊤-reduction step. □

Lemma 5.4.7 (Distributivity of Conditioned Instantiation) Let C_{1} = {L_{1}, …, L_{n}} and C_{2} = {K_{1}, …, K_{m}} be two clauses having no variables in common, L_{1}∈C_{1} and K_{1}∈C_{2} and σ be a substitution. If σ(L_{1})∉Cond(σ) and σ(K_{1})∉Cond(σ), then

σ↓((C_{1} \ {L_{1}}) ∪ (C_{2} \ {K_{1}})) = (σ↓C_{1} \ {σ(L_{1})}) ∪ (σ↓C_{2} \ {σ(K_{1})})

Proof:

σ↓((C_{1} \ {L_{1}}) ∪ (C_{2} \ {K_{1}}))

= σ↓({L_{2}, …, L_{n}} ∪ {K_{2}, …, K_{m}})

= {σ(L_{2}), …, σ(L_{n})} ∪ {σ(K_{2}), …, σ(K_{m})} ∪ Cond(σ)

according Definition 5.1.2

= ({σ(L_{2}), …, σ(L_{n})} ∪ Cond(σ)) ∪ ({σ(K_{2}), …, σ(K_{m})} ∪ Cond(σ))

= (({σ(L_{1}), …, σ(L_{n})}\{σ(L_{1})})∪Cond(σ))∪(({σ(K_{1}), …, σ(K_{m})}\{σ(K_{1})})∪

Cond(σ))

= (({σ(L_{1}), …, σ(L_{n})}∪Cond(σ))\{σ(L_{1})})∪(({σ(K_{1}), …, σ(K_{m})}∪Cond(σ))\

{σ(K_{1})})

= (σ↓C_{1} \ {σ(L_{1})}) ∪ (σ↓C_{2} \ {σ(K_{1})})

□

Lemma 5.4.8 (Ground Substitutions swallow more general substitutions) Let C = {L_{1}, …, L_{n}} be a clause, C′ = {K_{1}, …, K_{m}} be a set of atoms, σ a ground substitution with DOM(σ) = V (C′) and σ(K_{1}) = … = σ(K_{m}) and let λ be the mgu of {K_{1}, …, K_{m}}, then

σ↓(λ↓C) = σ↓C

Proof:

σ↓(λ↓C)

= σ↓({λ(L_{1}), …, λ(L_{n})} ∪ Cond(λ))

= {(σλ)(L_{1}), …, (σλ)(L_{n})} ∪ σ(Cond(λ)) ∪ Cond(σ)

= {σ(L_{1}), …, σ(L_{n})} ∪ σ(Cond(λ)) ∪ Cond(σ) follows from Lemma 5.3.4

= {σ(L_{1}), …, σ(L_{n})} ∪ Cond(σ)

as λ is more general than σ, we have σ(Cond(λ)) ⊆ Cond(σ)

= σ↓C

□

Lemma 5.4.9 (Resolvent Lifting I) Let C_{1} = {L_{1}, …, L_{n}} and C_{2} = {K_{1}, …, K_{m}} be two clauses with no variables in common. Let σ be a ground substitution such that for two arbitrary literals L_{1} and K_{1} with σ(L_{1})∉Cond(σ) and σ(K_{1})∉Cond(σ), σ(L_{1}) and σ(K_{1}) are complementary there exists a sequence of factorization steps and a resolvent R(C′_{1}, C′_{2}, L′, K′) such that

R_{g}(σ↓C_{1}, σ↓C_{2}, σ(L_{1}), σ(K_{1})) = σ↓R(C′_{1}, C′_{2}, L′_{1}, K′_{1})

Proof: Let {L_{i_{1}}, …, L_{i_{k}}} ⊆ C_{1} be the set of literals which merge with L_{1} by σ and {K_{j_{1}}, …, K_{j_{h}}} the corresponding set for C_{2}. Let λ_{1} be the mgu of {L_{1}, L_{i_{1}}, …, L_{i_{k}}}, λ_{2} the mgu of {K_{1}, K_{j_{1}}, …, K_{j_{h}}} and λ = λ_{1} ∪ λ_{2}, F^{∗}(C_{1}, L_{1}, L_{i}) = λ_{1} ↓ C_{1}, F^{∗}(C_{2}, K_{1}, K_{j}) = λ_{2}↓C_{2} (we use F^{∗}() as an abbreviation for the necessary sequence of binary factorization steps) and δ the mgu of λ(L_{1}) and λ(K_{2}).

σ↓R(λ_{1}↓C_{1}, λ_{2}↓C_{2}, λ_{1}(L_{1}), λ_{2}(K_{1}))

= σ↓(δ↓((λ_{1}↓(C_{1} \ {L_{1}}) ∪ (λ_{2}↓(C_{2} \ {K_{1}})))

according Definition 5.4.3

= σ↓(δ↓(λ↓((C_{1} \ {L_{1}}) ∪ (C_{2} \ {K_{1}})))

because λ = λ_{1} ∪ λ_{2} and the clauses are variable disjoint

= σ↓((δλ)↓((C_{1} \ {L_{1}}) ∪ (C_{2} \ {K_{1}})))

follows from Lemma 5.1.4

= σ↓((C_{1} \ {L_{1}}) ∪ (C_{2} \ {K_{1}})))

follows from Lemma 5.4.8, because (δλ) is the mgu of the set of atoms {atom(L_{1}), atom(L_{i_{1}}), …, atom(L_{i_{k}}), atom(K_{1}), atom(K_{j_{1}}), …, atom(K_{j_{h}})} = (σ↓C_{1} \ {σ(L_{1})}) ∪ (σ↓C_{2} \ {σ(K_{1})})

follows from Lemma 5.4.7

= R_{g}(σ↓C_{1}, σ↓C_{2}, σ(L_{1}), σ(K_{1}))

□

Lemma 5.4.10 (⊤-Reduction Lifting I) Let C be a clause, (t< −| ⊤)∈C, σ a ground substitution with σ(t< −| ⊤)< −| Cond(σ), then there exists an ⊤-reduction such that

E_{g}(σ↓C, σ(t< −| ⊤)) = σ↓E(C′, t′< −| ⊤)

Proof: Let {L_{1}, …, L_{k}} ⊆ C be the set of literals which merge with t< −| ⊤ by σ. Let λ be the mgu of {t< −| ⊤, L_{1}, …, L_{k}}, such that F^{∗}(C, t< −| ⊤, L_{i}) = λ↓C.

σ↓E(λ↓C, λ(t< −| ⊤))

= σ↓(λ↓C \ {λ(t< −| ⊤)} ∪ λ({x_{S}< −| S | x_{S}∈V (λ(t)), S ≠ ⊤}))

= σ↓(λ↓C) \ {σ(λ(t< −| ⊤))} ∪ σ(λ({x_{S}< −| S | x_{S}∈V (λ(t)), S ≠ ⊤})) by Lemma 5.4.7

= σ↓C \ {σ(t< −| ⊤)} ∪ σ({x_{S}< −| S | x_{S}∈V (λ(t)), S ≠ ⊤})

by Lemma 5.4.8

= σ↓C \ {σ(t< −| ⊤)} because for all x_{S}∈V (t) we have x_{S}∈V (C) and for the added literals of the form x_{S}< −| S we have S ≠ ⊤

= E_{g}(σ↓C, σ(t< −| ⊤))

□

Lemma 5.4.11 (Resolvent Lifting II) Let C_{1} = {L_{1}, …, L_{n}} and C_{2} = {K_{1}, …, K_{m}} be two clauses with no variables in common. Let σ be a ground substitution such that for two arbitrary literals L_{1} and K_{1} with σ(L_{1}) and σ(K_{1}) are complementary and wlog. let σ(L_{1})∈Cond(σ), then there exists a resolvent R(C_{1}, C_{2}, L, K) such that

R_{g}(σ↓C_{1}, σ↓C_{2}, σ(L_{1}), σ(K_{1})) ∪ {σ(L_{1})} = σ↓R(C_{1}, C_{2}, L_{1}, K_{1})

Proof: The proof is similar to the proof of Lemma 5.4.9. We only have to change Lemma 5.4.7 slightly in σ↓((C_{1} \ {L_{1}}) ∪ (C_{2} \ {K_{1}})) = (σ↓C_{1} \ {σ(L_{1})}) ∪ (σ↓ C_{2} \ {σ(K_{1})}) ∪ {σ(L_{1}}. □

Remark 5.4.12 (Relaxing the lifting Lemmata) We can relax the premises of Lifting I and Lifting II by assuming two clauses C_{1},C_{2} and two ground clauses C_{1g},C_{2g} with σ↓C_{1} = C_{1g}∪{L_{1g}, …, L_{n′g}} and σ↓C_{2} = C_{2g}∪{K_{1g}, …, K_{m′g}}. For the potentially complementary literals L_{1} and K_{1} we have σ(L_{1})∈C_{1g} and σ(K_{1})∈C_{2g}. Then the following equations R_{g}(C_{1g}, C_{2g}, σ(L_{1}), σ(K_{1})) ∪ {L_{1g}, …, L_{n′g}} ∪ {K_{1g}, …, K_{m′g}} = σ↓R(C_{1}, C_{2}, L_{1}, K_{1})

R_{g}(C_{1g}, C_{2g}, σ(L_{1}), σ(K_{1})) ∪ {L_{1g}, …, L_{n′g}} ∪ {K_{1g}, …, K_{m′g}} ∪ {σ(L_{1})} = σ↓R(C_{1}, C_{2}, L_{1}, K_{1})

hold for Lifting I and Lifting II respectively.

For the ⊤-reduction rule we also have the corresponding lifting Lemma II and the corresponding relaxation.

Theorem 5.4.13 (Completeness of the Rules) Let CS be an unsatisfiable set of clauses. Then there exists a derivation of the empty clause using resolution, factorization and ⊤-reduction. Proof: If CS is unsatisfiable, Theorem 5.1.8 guarantees the existence of a finite and unsatisfiable set CS_{H} of ground clauses. With Lemma 5.2.5 we know that it is possible to derive the empty clause from CS_{H} using ground resolution and ground ⊤-reduction. Now we show by induction on the k-parameter that the ground proof can be lifted to a proof using resolution, factorization and ⊤-reduction as defined in Definitions 5.4.3, 5.4.4, 5.4.1.

k(CS_{H}) = 0: We have derived the empty clause on ground level from two ground unit clauses C_{1g} and C_{2g} or a ground unit clause {t< −| ⊤}. In the case of having performed performed a resolution step, the parent clauses are conditioned instances of two clauses C_{1},C_{2} using a ground substitution σ, e.g. {C_{1}, C_{2}} ⊆ CS, σ↓C_{1} = C_{1g} and σ↓C_{2} = C_{2g}. Now we have to distinguish two cases.

Firstly, if the premises of Lemma 5.4.9 are satisfied by C_{1}, C_{2}, C_{1g} and C_{2g} we can directly lift this step and have derived the empty clause on the general level. Secondly, if the premises of Lemma 5.4.11 are satisfied by C_{1}, C_{2}, C_{1g} and C_{2g} we can also lift the ground step, but we obtain a clause C′ ≠ □ on the general level. But as C_{1g} and C_{2g} are ground unit clauses, we have C′ = C_{1g} or C′ = C_{2g}. Thus one more resolution step yields the empty clause on the general level, too.

If we perform a ⊤-reduction step in order to get the empty clause, this step can be lifted to a step on the general level directly.

k(CS_{H}) > 0: There is at least one clause C_{g}∈CS_{H} with |C_{g}| > 1. We also know of the existence of a clause C∈CS with σ↓C = C_{g}. Again we have to distinguish two cases.

Firstly, if we can split the clause C_{g} into two nonempty clauses C_{1g} and C_{2g} such that we can also split C into two nonempty clauses C_{1} and C_{2} with σ_{1}↓C_{1} = C_{1g} and σ_{2}↓C_{2} = C_{2g} we are done by induction hypothesis.

Secondly, if we cannot split C_{g} in the way mentioned above, we have at least one literal L_{g}∈C_{g} and a literal L∈C with σ(L) = L_{g}. By induction hypothesis we can lift the refutation of CS_{H} \ {C_{g}} ∪ {{L_{g}}} using C as the general clause for {L_{g}}. This can be done following Remark 5.4.12 where we use the relaxed lifting lemma versions for steps involving clauses stemming from {L_{g}}. As a result we obtain a general clause C′ with either σ′↓C′ = C_{g} \ {L_{g}} or σ′↓C′ = C_{g} (σ′ is the restriction of σ to the variables occurring in C′). In the first case we have finished the proof by induction hypothesis. In the second case, we again try to split C_{g} and C′ in the described way. This process terminates because as a consequence of Lemma 5.4.6 V (C′) ⊂ V (C) is valid. □

The Calculus CLS

The calculus introduced in Chapter 5 is on half the way to a sorted calculus. It uses the additional expressiveness of sorted logic but doesn’t exploit the information about sorts by special reasoning mechanisms. For sorted logic the right way to do the sorted reasoning is to use a sorted unification algorithm. This point of view is more efficient than a theory resolution [Sti85] or constraint resolution [Bue91] approach to sorted reasoning.

In this chapter we introduce our sorted unification algorithm which is an extension of the unification algorithm given in [SS89]. For the algorithm we need one additional rule rejecting unification problems which contain variables with empty sorts. Additionally we need to be able to deal with “conditioned” declarations. Translating the sort structure of [Wal87, SS89] into sorted logic we obtain a set of unit clauses containing declarations. In our logic declarations may occur together in a clause with arbitrary literals. They are “conditioned” by other literals. In Section 6.3 we will show that me must consider “conditioned” declarations in order to get a complete calculus.

6.1 Sorted Unification

Definition 6.1.1 (Conditioned Objects) A pair (t< −S, C) is called a conditioned declaration (conditioned term, conditioned substitution) if C is a set of literals and t< −S a declaration (term, substitution). A conditioned object (t, C) is called ground if t is ground.

Definition 6.1.2 (Well Sorted Terms) Let L_{< −} be a set of conditioned declarations. Then the set of conditioned well sorted terms Tc_{L_{< −},S} of sort S is recursively defined by:

• for every variable x_{S}∈V, (x_{S}, ∅)∈Tc_{L_{< −},S}

• for every conditioned declaration (t< −S, C)∈L_{< −} (S ≠ ⊤) with V (t) = {x_{S_{1}}, …,

x_{S_{n}}} and conditioned terms (t_{i}, C_{i})∈Tc_{L_{< −},S_{i}}, σ: = {x_{S_{1}} ↦ t_{1}, …, x_{S_{n}} ↦ t_{n}},

(σ(t), σ(C) ∪ C_{1} … ∪ C_{n})∈Tc_{L_{< −},S}

• for every term t we have (t, ∅)∈Tc_{L_{< −},⊤}

We define T_{L< −,S}: = {(t, C) | (t, C)∈Tc_{L< −,S} and C = ∅}. Tc_{L< −,gr,S} stands for the set of conditioned well sorted ground terms of sort S. Obviously Tc_{L< −,gr,S} = {(t, C) | (t, C)∈Tc_{L< −,S} and t is ground }. Thus we always have T_{L< −,gr,⊤} = Tc_{L< −,gr,⊤} ≠ ∅,

Tc_{L< −,gr,S} ⊆ Tc_{L< −,S} and T_{L< −,S} ⊆ Tc_{L< −,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_{S} with x_{S}∈Tc_{L< −,T}. Note that if there exists a variable x_{S}∈Tc_{L< −,T} there are infinitely many variables of sort S in Tc_{L< −,T}. The relation S ⊑ T implies

Tc_{L< −,S} ⊆ Tc_{L< −,T}.

Seldom we are interested in the condition part of a conditioned object. We say that t∈Tc_{L< −,S} if there is a set of literals C such that (t, C)∈Tc_{L< −,S}. Similarly we say that a declaration (t< −S)∈L_{< −} if there is a set of literals C such that (t< −S, C)∈L_{< −}. If not necessary we do not mention the conditioned part of a conditioned substitution.

Lemma 6.1.3 (Correctness of Well Sorted Terms) Let L_{< −} be a set of conditioned declarations. Then for every interpretation ℑ = (M, φ) with ℑ ⊧ L_{< −} and every conditioned term (t, C)∈Tc_{L< −,S} with V ((t, C)) ⊆ DOM(φ) we have φ(t)∈ℑ(S) or ℑ ⊧ C. Proof: By structural induction according to Definition 6.1.2 □

Definition 6.1.4 (Well Sorted Substitutions) A conditioned substitution σ^{c} = (σ, C) is called well sorted with respect to the set of declarations L_{< −} if for every

x_{S_{i}}∈DOM(σ), (σ(x_{S_{i}}), C_{i})∈Tc_{L< −,S_{i}} and C = ⋃ C_{i}.

The composition of two well sorted substitutions can be computed by σ^{c}(τ^{c}): = (σ(τ), σ(K) ∪ C′), where σ^{c} = (σ, C), τ^{c} = (τ, K) and C′ is the restriction of C to the conditions of the variables in DOM(σ)\DOM(τ). The result of the composition is again a well sorted substitution. Thus the set of all well sorted substitutions builds a monoid.

Definition 6.1.5 (Notions for Sorted Unification) In order to define well sorted unification, we have to extend Definition 5.3.1. A unification problem Γ = {x_{S_{1}} = t_{1}, …, x_{S_{n}} = t_{n}} is called well sorted solved with respect to a set of declarations L_{< −} if Γ is solved and for every variable x_{S_{i}} we have t_{i}∈Tc_{L< −,S_{i}}.

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

(1) ({x_{S} = x_{S}} ∪ Γ) → Γ

(2) ({x_{S} = t} ∪ Γ) → ({x_{S} = t} ∪ {x_{S} ↦t}Γ) if x_{S} is a variable, t a term and x_{S}∉V (t), x_{S}∈V (Γ)

(3) ({t = x_{S}} ∪ Γ) → ({x_{S} = t} ∪ Γ)

if x_{S} is a variable and t a non-variable term

(4) ({x_{S} = t} ∪ Γ) → STOP.FAIL if x_{S}∈V (t) and t ≠ x_{S}

(5) ({f(t_{1}, …, t_{n}) = f(s_{1}, …, s_{n})} ∪ Γ) → ({t_{1} = s_{1}, …, t_{n} = s_{n}} ∪ Γ)

(6) ({f(t_{1}, …, t_{n}) = g(s_{1}, …, s_{m})} ∪ Γ) → STOP.FAIL if f ≠ g

(7) Γ → STOP.FAIL if there exists a variable x_{S}∈V (Γ) such that Tc_{L< −,gr,S} = ∅

(8) ({x_{S} = y_{T} } ∪ Γ) → STOP.FAIL if S ≠ ⊤, T ≠ ⊤, y_{T} ∉Tc_{L< −,S} and x_{S}∉Tc_{L< −,T} and there is no common subsort of S and T and there are no conditioned declarations (f(s_{1}, …, s_{n})< −S′)∈L_{< −}, S′ ⊑ S and (f(t_{1}, …, t_{n})< −T′)∈L_{< −}, T′ ⊑ T

(9) ({x_{S} = f(t_{1}, …, t_{n})} ∪ Γ) → STOP.FAIL if S ≠ ⊤, x_{S}∉V (f(t_{1}, …, t_{n})), f(t_{1}, …, t_{n})∉Tc_{L< −,S} and there is no declaration (f(s_{1}, …, s_{n})< −S′)∈L_{< −}, S′ ⊑ S

(10) ({x_{S} = f(t_{1}, …, t_{n})}∪Γ) → ({x_{S} = f(t_{1}, …, t_{n})}∪{t_{1} = s_{1}, …, t_{n} = s_{n}}∪Γ) if S ≠ ⊤, x_{S}∉V (f(t_{1}, …, t_{n})), f(t_{1}, …, t_{n})∉T_{L< −,S} and there is a conditioned declaration (f(s_{1}, …, s_{n})< −S′)∈L_{< −}, S′ ⊑ S

(11) ({x_{S} = y_{T} } ∪ Γ) → ({y_{T} = x_{S}} ∪ Γ)

if x_{S}∈Tc_{L< −,T} and y_{T} ∉T_{L< −,S}

(12) ({x_{S} = y_{T} } ∪ Γ) → ({x_{S} = z_{V} } ∪ {y_{T} = z_{V} } ∪ Γ)

if S ≠ ⊤, T ≠ ⊤, x_{S}∉T_{L< −,T} and y_{T} ∉T_{L< −,S} and V is a maximal sort with V ⊑ S and V ⊑ T

(13) ({x_{S} = y_{T} } ∪ Γ) → ({x_{S} = f(s_{1}, …, s_{n})} ∪ {y_{T} = f(t_{1}, …, t_{n})} ∪ {s_{1} = t_{1}, …, s_{n} = t_{n}} ∪ Γ) if S ≠ ⊤, T ≠ ⊤, y_{T} ∉T_{L< −,S} and x_{S}∉T_{L< −,T} and there are conditioned declarations (f(s_{1}, …, s_{n})< −S′)∈L_{< −}, S′ ⊑ S and (f(t_{1}, …, t_{n})< −T′)∈L_{< −}, T′ ⊑ T and S′ ⋢ T′ and T′ ⋢ S′

In order to compute a well sorted substitution from a solved unification problem, we have to do the following. Let Γ = {x_{S_{1}} = t_{1}, …, x_{S_{n}} = t_{n}} be the solved unification problem, then σ: = {x_{S_{1}} ↦t_{1}, …, x_{S_{n}} ↦t_{n}} is the corresponding unconditioned most general well sorted unifier. σ^{c}: = (σ, C_{1} ∪ … ∪ C_{n} ∪ D) is a most general well sorted unifier if we have (t_{i}, C_{i})∈Tc_{L< −,S_{i}} and D is a minimal set of conditions under which we have Tc_{L< −,gr,S_{i}} ≠ ∅ for all x_{S_{i}}∈I(σ). Thus from a solved unification problem we may be able to compute several (but only finitely many) most general well sorted unifiers.

Lemma 6.1.7 (Correctness of the Unification Algorithm) The unification algorithm is correct. Proof: Can be easily proved for the rules. The proof is achieved by showing that every well sorted (ground) substitution solving the problem after the application of a rule solves the original problem. □

If there is no conditioned declaration in L_{< −} and sorts are assumed to be nonempty our unification algorithm simplifies to the algorithm of [SS89]. In this case our algorithm computes a minimal set of most general unifiers and we know that the unification problem is undecidable and of type infinitary. In the case of conditioned declarations it is not possible to characterize a minimal set of mgu’s without “looking into the conditions”. At the end of the algorithm we just collect the conditions. Therefore our algorithm may compute a non minimal set of mgu’s. Nevertheless the algorithm is complete in the sense that we can lift every ground step using sorted unification.

Lemma 6.1.8 (Completeness of the Unification Algorithm) Let Γ be a unification problem and τ^{c} a well sorted ground substitution which solves Γ. Then our algorithm computes a well sorted mgu σ^{c} which solves Γ such that there is a well sorted ground substitution λ^{c} with λ^{c}(σ^{c}) = τ^{c}. Proof: Straightforward using the techniques given in [SS89]. □

Our completeness result is weaker than the completeness result given in [SS89]. But it is sufficient to show the completeness of our sorted calculus. It is not straightforward (and maybe not possible) to obtain a more general result, because this implies a very careful and exact examination of the conditions. The theory coded in the conditions may be arbitrarily complex. Nevertheless there are possible improvements, e.g. if σ^{c} = (σ, C) and τ^{c} = (τ, K) are two mgu’s generated by the algorithm and if there is a well sorted substitution λ^{c} = (λ, D) such that λ(σ) = τ and (λ(C) ∪ D′) ⊆ K, where D′ is the restriction of D to the conditions of the variables in DOM(λ) \ DOM(σ) we can skip τ^{c}. This corresponds to an application of subsumption on the clause level.

6.2 Examples for Sorted Unification

In the following we present a bunch of examples illustrating the different phenomena coming up with our sorted unification algorithm. Firstly, we show the properties of the algorithm not using conditioned declarations. Secondly, we target on the question of what happens if we need to consider conditioned declarations. The application of the algorithm to our examples is discussed in Chapter 8.

We start with the following set of (unconditioned) declarations: L_{< −}: = {(a< −S, ∅), (a< −T, ∅), (f(y_{S})< −S, ∅), (f(y_{T})< −T, ∅)} and the unification problem Γ_{0} = {x_{S} = x_{T} }.

We have Tc_{L< −,S} = T_{L< −,S} = {a, f(a), f(y_{S}), f(f(a)), …, x_{S}, y_{S}, …} and Tc_{L< −,T} =

T_{L< −,T} = {a, f(a), f(y_{T}), f(f(a)), …, x_{T} , y_{T} , …}, where all well sorted terms are unconditioned. Applying the algorithm results in the following unification problems:

Γ_{0} = {x_{S} = x_{T} }

The only rule applicable is rule 13 resulting in the two new problems

\begin{aligned}Γ_{01} & = & \{x_{S} = a, x_{T} = a\} \\ Γ_{02} & = & \{x_{S} = f(y_{S}), x_{T} = f(y_{T}), y_{S} = y_{T} \} \end{aligned}

Problem Γ_{01} is solved. Again we are able to apply rule 13 in order to solve problem Γ_{02}. Thus we obtain the following mgu’s

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

Again all declarations are unconditioned and therefore we can skip the conditioned part of the unifiers. This well known example [Wal87, SS89] shows that we may obtain infinitely many most general well sorted unifiers.

Now we replace some of the unconditioned declarations by conditioned declarations. We choose L_{< −}: = {(a< −S, ∅), (a< −T, ∅), (f(y_{S})< −S, {P (y_{S})}), (f(y_{T})< −T, {R(y_{T})})}.

Thus T_{L< −,S} = {a, x_{S}, y_{S}, …} and Tc_{L< −,S} = {a, x_{S}, y_{S}, …, (f(a), {P (a)}), (f(y_{S}),

{P (y_{S})}), (f(f(a)), {P (a), P (f(a))}), …}. The sets T_{L< −,T} and Tc_{L< −,T} have a similar structure. Again an unconditioned term is denoted by the term itself. Solving the same problem as above, we get the same solved problems but different conditioned unifiers:

σc_{1} = ({x_{S} ↦a, x_{T} ↦a}, ∅)
σc_{2} = ({x_{S} ↦f(a), x_{T} ↦f(a)}, {P (a), R(a)})
σc_{3} = {(\{x_{S} ↦f(f(a)), x_{T} ↦f(f(a))\}, \atop \{P (a), R(a), P (f(a)), R(f(a))\})}
⋮

In order to make clear why we choose t∈Tc_{L< −,S} as a success condition for a pair x_{S} = t occurring in a unification problem but t∈T_{L< −,S} as a stop condition for the sorted rules (no sorted rule is applicable to an equation x_{S} = t with t∈T_{L< −,S}) consider the next example. We choose L_{< −}: = {(x_{S}< −T, {P (x_{S})}), (x_{S}< −V, ∅), (x_{A}< −S, ∅), (x_{A}< −T, ∅), (a< −A, {Q(a)})} and solve the unification problem

Γ_{0} = {x_{V} = x_{T} }

The only applicable rule is rule 12 using the conditioned declarations x_{S}< −T and x_{S}< −V resulting in the problem

Γ_{01} = {x_{V} = x_{S}, x_{T} = x_{S}}

The problem is solved because we have x_{S}∈Tc_{L< −,V} and x_{S}∈Tc_{L< −,T}. But the rule 12 is still applicable because x_{S}∉T_{L< −,T}. Another application of rule 12 using the declarations x_{A}< −S and x_{A}< −T leads to

Γ_{011} = {x_{V} = x_{S}, x_{T} = x_{A}, x_{S} = x_{A}}

and after another application of rule 2 using the equation x_{S} = x_{A} we end up in the solved problem

Γ_{0111} = {x_{V} = x_{A}, x_{T} = x_{A}, x_{S} = x_{A}}

The problems Γ_{01} and Γ_{0111} represent the two conditioned unifiers

\begin{aligned}σ_{01} & = & (\{x_{V} ↦x_{S}, x_{T} ↦x_{S}\}, \{P (x_{S}), Q(a)\}) \\ σ_{0111} & = & (\{x_{V} ↦x_{A}, x_{T} ↦x_{A}, x_{S} ↦x_{A}\}, \{Q(a)\}) \end{aligned}

The unifier σ_{0111} is not subsumed by σ_{01} because it contains less conditions. The condition Q(a) ensures that the sort A is not empty, i.e. Tc_{L< −,gr,A} ≠ ∅.

6.3 The Sorted Inference Rules

Now we present the sorted counterparts of the inference rules given in Chapter 5. Instead of adding conditional literals, the sorted rules apply the sorted unification algorithm where the well sortedness of the unifier is checked.

Definition 6.3.1 (Sorted Factor) Let C = {L_{1}, …, L_{n}} be a clause, {L_{i}, L_{j}} ⊆ C (i ≠ j), and σ^{c} = (σ, D) a well sorted mgu of {L_{i}, L_{j}}, i.e. σ(L_{i}) = σ(L_{j}), then F (C, L_{i}, L_{j}): = σ(C) ∪ D is called a sorted factor of C.

Definition 6.3.2 (Sorted Resolution Rule) Let C_{1} and C_{2} be two clauses with no variables in common, L∈C_{1} and K∈C_{2}. If there exists a well sorted mgu σ^{c} = (σ, D) of L and K, such that σ(L) and σ(K) become two complementary literals then

R(C_{1}, C_{2}, L, K): = σ((C_{1} \ {L}) ∪ (C_{2} \ {K})) ∪ D

is a sorted resolvent of C_{1} and C_{2}.

Definition 6.3.3 (Sorted ⊤-Reduction Rule) Let C be a clause and let (t< −| ⊤)∈C, with Tc_{L< −,gr,S} ≠ ∅ for every x_{S}∈V (t) under some minimal conditions D then

E(C, t< −| ⊤): = (C \ {t< −| ⊤}) ∪ D

is called a sorted ⊤-Reduction of C.

Lemma 6.3.4 (Correctness of the Rules) Let CS be a set of clauses and L_{< −} a set of declarations, such that every declaration in L_{< −} occurs in a clause in CS and the other literals of the clause constitute the condition of the declaration. Then the rules sorted resolution, sorted factorization, and sorted ⊤-reduction are correct. Proof: Follows from the form of the rules, Lemma 6.1.3 and Lemma 6.1.7 □

There still remains an open question: which declarations we have to select for L_{< −} in order to obtain a complete calculus. The general idea is to reduce the number of declarations which have to be taken into account deciding unification. We will show that it is necessary and sufficient to arbitrarily choose from every clause containing declarations only, one declaration to build the well sorted terms. This has to be done dynamically during the derivation process, i.e. if we have derived a new clause only containing positive declarations we may have to change the set L_{< −}. On the other hand no declaration which occurs in a clause containing different literals has to be taken into consideration. These clauses typically occur if the membership of an object to a sort depends on certain properties or some other relations are defined by means of sorts.

The minimal set of literals for building the well sorted terms, is the set of declarations occurring in unit clauses, because every interpretation satisfying the clause set satisfies these literals. The following example shows that this set is too small for a complete calculus.

Example 6.3.5 (Considering Declarations in Unit Clauses is not Sufficient) Let CS be the clause set CS = {{P (x_{A})}, {P (x_{B})}, {¬P (a)}, {¬P (b)}, {a< −A, b< −B}}. If we only take declarations in unit clauses into account we have L_{< −} = ∅ and therefore Tc_{L< −,gr,A} = Tc_{L< −,gr,B} = ∅. There is no well sorted resolution step. But CS is unsatisfiable as the following refutation shows (we use the calculus given in Chapter 5). From {P (x_{A})} and {¬P (a)} we derive {a< −| A}. Using {a< −A, b< −B} we conclude {b< −B}. {P (x_{B})} and {¬P (b)} lead to {b< −| B} and finally we succeed in deriving the empty clause by using {b< −B}.

The problem in Example 6.3.5 is the clause {a< −A, b< −B} which triggers a case analysis in the refutation proof. The example shows that we can not disregard such clauses. We have to extend the set of declarations used for building the well sorted terms by exactly one literal from each clause containing declarations only. But these declarations are conditioned, i.e. not every interpretation satisfying the clause set satisfies the declaration we choose. Therefore we must keep track of the conditions for the declaration. This leads to the definitions of the previous section.

Now we will develop the definitions and lemmata which enable us to proof the completeness of the calculus.

Definition 6.3.6 (Declaration Clause) A clause C is called a declaration clause if C consists of declarations only.

Let CS be a clause set. We define L_{< −}^{U}: = {(t< −S, ∅) | t< −S occurs in CS in a unit clause}, L_{< −}^{M}: = {(t< −S, C′) | t< −S occurs in a clause C in CS, and C = {t< −S} ∪ C′}, and L_{< −}^{C}: = {(t_{i}< −S_{i}, C′_{i}) | such that for each declaration clause C_{i}∈CS we choose exactly one declaration t_{i}< −S_{i} with C_{i} = {t_{i}< −S_{i}} ∪ C′_{i}}.

Lemma 6.3.7 (Refutations yield Well Sorted Ground Substitutions) Let CS be a set of clauses. If we can derive the empty clause from CS using the inference rules of Chapter 5 then the resulting overall ground substitution τ is well sorted with respect to L_{< −}^{M}. Proof: by induction on the number of variables in DOM(τ) Wlog. we assume that CS is a clause set such that every clause in CS is used exactly once in the refutation proof and all clauses are variable disjoint. If τ is the overall ground substitution then DOM(τ) = V (CS). In order to be precise we show the existence of a well sorted ground substitution τ^{c} = (τ, K). As the case S = ⊤ is trivial we assume S ≠ ⊤. |DOM(τ)| = 1: then DOM(τ) = {x_{S}} and there is exactly one clause C∈CS with V (C) = {x_{S}} and for all clauses C′∈CS with C′ ≠ C we have V (C′) = ∅. Now we focus on the deduction step where x_{S} is instantiated by a ground term t. For the resolvent (factor) R we know that (t< −| S)∈R. Therefore there is a positive literal t< −S occurring in some clause C = {t< −S} ∪ C′ in CS, thus (t< −S, C′)∈L_{< −}^{M}, thus (t, C′)∈Tc_{L< −^{M},gr,S} and therefore τ^{c} = ({x_{S} ↦t}, C′) is well sorted.

|DOM(τ)| > 1: We choose an arbitrary variable x_{S}∈DOM(τ) and focus on the resolution step where x_{S} is instantiated by a term t. Again we know that the resolvent R contains the literal t< −| S and therefore there is a literal t′< −S occurring in some clause C = {t< −S} ∪ C′ in CS, (t′< −S, C′)∈L_{< −}^{M} which is used to eliminate t< −| S. We have τ[x_{S}](t) = τ[x_{S}](t′) and because τ^{c}[x_{S}] = (τ[x_{S}], K′) is well sorted by induction hypothesis we have (τ[x_{S}](t), τ[x_{S}](C′) ∪ K′′)∈Tc_{L< −^{M},gr,S} where K′′ is the restriction of K′ to the variables in t. Thus τ^{c} = (τ, K) = (τ[x_{S}] ∪ {x_{S} ↦ τ[x_{S}](t)}, K′ ∪ τ[x_{S}](C′)) is a well sorted ground substitution. □

Theorem 6.3.8 (Completeness of the Calculus: Choosing L_{< −}^{C} is Sufficient) Let CS be a clause set and let L_{< −}^{C} be the set of declarations dynamically chosen for unification. Dynamically chosen means that we have to update L_{< −}^{C} after the generation of a new declaration clause. If CS is unsatisfiable there exists a derivation of the empty clause using sorted resolution, sorted factorization, and sorted ⊤-reduction. Proof: by induction on the k-parameter [AB70], k(CS): = ∑ {|C| − 1 | C∈CS} where |C| is the number of literals in the clause C. If k(CS) = 0: We know by Theorem 5.4.13 of the existence of a refutation. Lemma 6.3.7 states that this refutation produces a well sorted ground substitution with respect to L_{< −}^{M}. As k(CS) = 0 we have L_{< −}^{M} = L_{< −}^{C} and therefore the ground substitution is also well sorted with respect to L_{< −}^{C}. Now Lemma 6.1.8 ensures that we can refute the clause set by a single sorted inference step.

If k(CS) > 0: There exists a non unit clause C. In a case analysis we separate C into two parts C_{1} and C_{2} and CS into the clause sets CS_{1}: = CS \ {C} ∪ {C_{1}} and CS_{2}: = CS \ {C} ∪ {C_{2}}. Both clause sets are unsatisfiable and we have k(CS_{i}) < k(CS). Thus by induction hypothesis we can refute the two clause sets. The two proofs can be combined, because Theorem 5.4.13 ensures the existence of a common (ground) substitution. In order to apply the induction hypothesis we must guarantee that all bottom clause sets (k(CS) = 0) can be refuted. For the refutation of a bottom clause set we need L_{< −}^{M} = L_{< −}^{C}. If we split a declaration clause we can first refute the bottom clause set containing the declaration we choose for L_{< −}^{C}. After this refutation we obtain a clause which may contain some additional instances of the other declarations of the splitted clause. Using the factorization rule we can generate a clause where just the literal we chose for L_{< −}^{C} is deleted. Now we must dynamically change L_{< −}^{C} and choose one of the other literals from the new, smaller declaration clause. If we split a clause which is not a declaration clause but contains some declarations we can first refute the part not containing declarations. The refutation results in a declaration clause. We change L_{< −}^{C} and continue. If we split a clause not containing any declaration we can continue in an arbitrary order. □

Example 6.3.9 We again consider the clause set of Example 6.3.5. If we choose L_{< −}^{C}: = {(a< −A, {b< −B})} there is only one possible resolution step between {P (x_{A})} and {¬P (a)} resulting in {b< −B}. This clause subsumes the clause {a< −A, b< −B} and we obtain the new clause set {{P (x_{A})}, {P (x_{B})}, {¬P (a)}, {¬P (b)}, {b< −B}}. Now we also have to change L_{< −}^{C} into L_{< −}^{C}: = {(b< −B, ∅)}. Again only one resolution step between {P (x_{B})} and {¬P (b)} is applicable which yields the empty clause.

Note that we could also have chosen L_{< −}^{C}: = {(b< −B, {a< −A})} as the starting set of declarations. We can derive {a< −A} by resolving {P (x_{B})} and {¬P (b)}. The clause {a< −A} again subsumes {a< −A, b< −B} and we obtain the new clause set {{P (x_{A})}, {P (x_{B})}, {¬P (a)}, {¬P (b)}, {a< −A}} and the new set of declarations L_{< −}^{C}: = {(a< −A, ∅)}. Now we can refute the new clause set by resolving {P (x_{A})} and {¬P (a)}.

The calculus established by Theorem 6.3.8 is not the only one possible. Depending on the set of declarations we choose and the way we deal with the conditions of conditioned declarations there are more different complete and correct calculi. We can give some examples.

• We choose L_{< −}^{M} as the set of declarations for unification. The consequence of this choice is that we need not to change the set of declarations during deduction and that the calculus can be straightforward combined with all strategies (e.g. set of support) known from unsorted resolution preserving completeness. The disadvantage of choosing L_{< −}^{M} may be a collapse of the sort structure due to the additional declarations. The clause {x_{D}< −LL, ¬Lies(lion, x_{D}, y_{D}), y_{D}< −LL} of Example 4.2.5 demonstrates such a collapse. We have (x_{D}< −LL)∈L_{< −}^{M} and therefore the sorts D and LL collapse into one sort. This increases the number of resolution possibilities significantly such that nearly all advantages of the sorted formalization are lost.

• We change the unification Algorithm 6.1.6 in the following way: Every condition of type t∈T_{L< −,S} (in rules 10 to 13) is replaced by t∈Tc_{L< −,S}. The computation of the conditioned unifier from a solved problem is also changed. For each solved pair x_{S_{i}} = t_{i} with t_{i}∉T_{L< −,S_{i}} or T_{L< −,gr,S_{j}} = ∅ for some x_{S_{j}}∈V (t_{i}) we add the condition t_{i}< −| S_{i} to the unconditioned unifier. No extra conditions are added with respect to empty sorts. Thus all conditions are of the form t< −| S. These changes simplify the computation of well sorted unifiers significantly. But the resulting calculus is less restrictive, because the conditioned literals of the form t< −| S can be resolved with all positive declarations of the appropriate form occurring in the clause set. Instead of choosing the original unification algorithm only the declarations in L_{< −}^{C} are considered.

• In general we can establish any calculus between the calculus given in Section 5 using unsorted unification and the calculus of Theorem 6.3.8 using sorted unification with respect to L_{< −}^{C}. The idea is to add to all pairs x_{S} = t of an unsorted solved unification problem the conditional literal t< −| S if we do not have t∈T_{L< −^{U},S} or T_{L< −^{U},gr,S′} ≠ ∅ for some x_{S′}∈V (t_{i}). Thus we have all freedom which equations of the unification problem we want to solve in an unsorted way and which we want to weaken until they are well sorted.

Although the presented calculi are simpler, as they either simplify the unification algorithm or the process of choosing the relevant declarations, we believe that the calculus established by Theorem 6.3.8 is most efficient. This statement is based upon the fact that that in all “practical” examples the sorted unification problem computes a finite set of unifiers in polynomial time and that the number of conditioned declarations is pretty small.

The calculus choosing L_{< −}^{M} as the set of declarations is close to the calculus presented in [WO90]. The treatment of the conditions makes the difference between the two calculi. In [WO90] we also considered L_{< −}^{M} as the set of declarations, But residue literals of the form t< −| S for every assignment x_{S} ↦t were added to a clause after the application of a substitution. In CL_{S} we do not add literals of the form t< −| S, but literals which prove t< −S if they are deleted by the inference rules.

Refinements on the Calculus CLS

7.1 Compilation

If we reverse the relativization process of Section 3.4 we are able to compile unsorted first-order formulas into sorted formulas and we may optimize sorted formulas.

Algorithm 7.1.1 (Compilation into Sorted Logic) The input of the algorithm is a sentence of unsorted first-order logic.

(1) Attach the top sort ⊤ to all unsorted variables.

(2) Translate the formulas into CNF, see Chapter 4.

(3) Select a set of 1-place predicates for the transformation into sorts.

(4) Change all occurrences of S(t) for the predicates in the selected set into t< −S.

(5) Build L_{< −}^{U}.

(6) For every clause C containing a negated declaration of the form x_{S}< −| T: if S ⊑ T (with respect to L_{< −}^{U}) and T_{L< −^{U},gr,S} ≠ ∅ delete the literal x_{S}< −| T; if T ⊑ S change C into {x_{S} ↦ x_{T} }(C \ {x_{S}< −| T }).

Note that the application of step 6 may produce the empty clause.

The steps 5 to 6 can also be applied in order to improve the representation of problems which are given in a sorted formalization. The compilation works for arbitrary unsorted clause sets. This is not the case for the compilation algorithm SOGEN of [SS89]. Our extensions to the work of [SS89] are necessary and sufficient to obtain this general result:

• Declarations can be used in the same way as any other atom.

• Sorts may denote empty sets.

• We have a fixed sort symbol ⊤ which denotes the topsort “Any”.

Let us apply Algorithm 7.1.1 to the clause normal forms of Example 4.2.5 and Example 4.2.6.

7.1.1 Compiling the Example “Condensed Detachment”

We start with the unsorted clause normal form of Example 4.2.6 where we have applied Step 1 and Step 2 of the algorithm.

\begin{matrix}(1) & \{¬P (i(x_{⊤}, y_{⊤})), ¬P (x_{⊤}), P (y_{⊤})\} \\ (2) & \{P (i(i(x_{⊤}, y_{⊤}), i(i(y_{⊤}, z_{⊤}), i(x_{⊤}, z_{⊤}))))\} \\ (3) & \{P (i(i(n(x_{⊤}), x_{⊤}), x_{⊤}))\} \\ (4) & \{P (i(x_{⊤}, i(n(x_{⊤}), y_{⊤})))\} \\ (5) & \{¬P (i(a, a))\} \end{matrix}

As there is only one 1-place predicate symbol P we select P and turn it into a sort. Thus after Step 3 and Step 4 we get the clause set

\begin{matrix}(1) & \{i(x_{⊤}, y_{⊤})< −| P, x_{⊤}< −| P, y_{⊤}< −P \} \\ (2) & \{i(i(x_{⊤}, y_{⊤}), i(i(y_{⊤}, z_{⊤}), i(x_{⊤}, z_{⊤})))< −P \} \\ (3) & \{i(i(n(x_{⊤}), x_{⊤}), x_{⊤})< −P \} \\ (4) & \{i(x_{⊤}, i(n(x_{⊤}), y_{⊤}))< −P \} \\ (5) & \{i(a, a)< −| P \} \end{matrix}

So far the changes have not affected the structure of the clause set but the syntax. Step 5 leads to L_{< −}^{U} = {i(i(x_{⊤}, y_{⊤}), i(i(y_{⊤}, z_{⊤}), i(x_{⊤}, z_{⊤})))< −P, i(i(n(x_{⊤}), x_{⊤}), x_{⊤})< −P, i(x_{⊤}, i(n(x_{⊤}), y_{⊤}))< −P }. The only candidate for application of Step 6 is the literal x_{⊤}< −| P in the first clause. As we have P ⊑ ⊤ we change the sort of the variable x_{⊤} into x_{P}, delete the literal from the clause and result in the final compiled clause set

\begin{matrix}(1) & \{i(x_{P} , y_{⊤})< −| P, y_{⊤}< −P \} \\ (2) & \{i(i(x_{⊤}, y_{⊤}), i(i(y_{⊤}, z_{⊤}), i(x_{⊤}, z_{⊤})))< −P \} \\ (3) & \{i(i(n(x_{⊤}), x_{⊤}), x_{⊤})< −P \} \\ (4) & \{i(x_{⊤}, i(n(x_{⊤}), y_{⊤}))< −P \} \\ (5) & \{i(a, a)< −| P \} \end{matrix}

It seams as if the effect of the compilation is rather small, because we have saved one literal only. But in Section 8.3 we will show that the proof using the compiled clause set is unique whereas the proof using the original unsorted clause set requires search in an infinite search space.

7.1.2 Compiling the Clause Set of “The Lion and the Unicorn”

Now we consider Example 4.2.5. As the problem is given in a sorted form we start the compilation with Step 5. We get L_{< −}^{U} = {(1)1−(10)1, (15)1−(17)1, (22)1−(39)1} (the notation (n)m refers to the m’th literal of clause n). Step 6 is applicable to the clauses (40) to (47). The literals of the form x_{D}< −| LL and x_{D}< −| LU can be deleted after having changed the sort of the variables because we have LU ⊑ D and LL ⊑ D with respect to L_{< −}^{U}. Therefore we get the compiled clauses:

(40) {x_{D}< −LL, ¬Lies(lion, x_{D}, y_{D}), y_{D}< −LL}
(41) {x_{D}< −LL, Lies(lion, x_{D}, y_{LL})}
(42) {¬Lies(lion, x_{LL}, y_{LL})}
(43) {Lies(lion, x_{LL}, y_{D}), y_{D}< −LL}
(44) {x_{D}< −LU, ¬Lies(uni, x_{D}, y_{D}), y_{D}< −LU}
(45) {x_{D}< −LU, Lies(uni, x_{D}, y_{LU} )}
(46) {¬Lies(uni, x_{LU} , y_{LU} )}
(47) {Lies(uni, x_{LU} , y_{D}), y_{D}< −LU}

Here we could delete all literals of the form x_{D}< −| LL (x_{D}< −| LU) in the clauses (40) to (47). This deletion will allow us to prove the theorem exploiting a very small search space, see Section 8.2.

7.2 Refinements on the Inference Rules

Some refinements concerning the interaction of the unification algorithm and the inference rules are possible. Consider the clauses

\begin{matrix}(1) & \{P (x_{S}), Q(x_{S})\} \\ (2) & \{a< −S, f(x_{⊤})< −V \} \\ (3) & \{¬P (y_{S})\} \\ (4) & \{¬Q(y_{S})\} \\ (5) & \{f(x_{⊤})< −| V \} \end{matrix}

We choose L_{< −}^{C} = {(a< −S, {f(x_{⊤})< −V })} and compute a resolvent between (1)1 and (3)1

(6) {Q(x_{S}), f(y_{⊤})< −V }

with unconditioned well sorted unifier σ = {y_{S} ↦x_{S}} and conditioned unifier σ^{c} = ({y_{S} ↦ x_{S}}, {f(y_{⊤})< −V }). The condition f(y_{⊤})< −V is the (only) minimal condition which guarantees T_{L< −^{C},gr,S} ≠ ∅. Next we built a resolvent between (6)1 and (4)1

(7) {f(y_{⊤})< −V, f(y′_{⊤})< −V }

Again we get the condition f(y′_{⊤})< −V, because the sort S is the sort of a variable in the codomain of the unconditioned unifier. We apply factorization to (7)1 and (7)2

(8) {f(y_{⊤})< −V }

and finally refute the clause set by resolving (8)1 and (5)1

(9) □

As the top sort ⊤ is non empty by definition, no conditions need to be added to the clauses (8) and (9).

What we want to show with the example is that the conditions coming from T_{L< −^{C},gr,S} ≠ ∅ need not to be added to the resolvent if there are some variables of sort S still occurring in the resolvent. Therefore we can get a closer interaction between the inference rules and the unification algorithm.

In the following assume that we have solved a unification problem in order to apply one of our inference rules. Let σ be the unconditioned well sorted unifier and S_{R} the set of sorts occurring in the resulting clause after application of σ. Then for the conditioned unifier σ^{c}, we only need to add non-emptiness conditions for sorts S for which we have: there is a variable x_{S}∈I(σ) and S∉S_{R}. It should be clear that this change preserves correctness, because if the sort S is empty in some interpretation there is still a variable of sort S in the clause or we have added the conditions. Completeness is also guaranteed because the resulting clause is smaller.

Solving the example using the modified rules, we again compute a resolvent between (1)1 and (3)1

(6′) {Q(x_{S})}

We have not added the condition f(y_{⊤})< −V, because x_{S} occurs in the resolvent {Q(x_{S})}. Next we built a resolvent between (6′)1 and (4)1

(7′) {f(y_{⊤})< −V }

As the sort S no longer occurs in the resolvent, we must add the condition f(y_{⊤})< −V. Building a resolvent between (7′) and (5)1 refutes the clause set.

(8′) □

The example demonstrates that a tight coupling between unification and the inference rules results in shorter proofs.

7.3 Refinements on the Unification Algorithm

It may happen that the unification algorithm runs in a cycle, i.e. the algorithm does not terminate. Sometimes this is a result of producing infinitely many unifiers (see Section 6.2), but very often it can be easily detected that the loop can not contribute to a solution. Consider the unification problem

Γ_{01} = {x_{D} = x_{LL}, y_{D} = f(x_{LL})}

related to Example 4.2.5. We choose L_{< −}^{C} = {(1)1−(10)1, (15)1−(17)1, (22)1−(39)1} and solve Γ_{01}. Only rule 10 of the unification algorithm is applicable to the second equation which yields the following the seven problems

Γ_{011} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Mo}}
Γ_{012} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Tu}}
Γ_{013} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{We}}
Γ_{014} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Th}}
Γ_{015} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Fr}}
Γ_{016} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Sa}}
Γ_{017} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Su}}

The problems Γ_{011}-Γ_{013} can be solved (see Section 8.2) but the other problems loop forever. For example after applying rule 2 to Γ_{014}, the only applicable rule is rule 13 to the last equation yielding the problems

Γ_{0141} = {x_{D} = x_{LL}, y_{D} = f(x_{Th}), x_{LL} = f(z_{Tu}),
x_{Th} = f(x_{Fr}), z_{Tu} = x_{Fr}}
Γ_{0142} = {x_{D} = x_{LL}, y_{D} = f(x_{Th}), x_{LL} = f(z_{We}),
x_{Th} = f(x_{Fr}), z_{We} = x_{Fr}}
Γ_{0143} = {x_{D} = x_{LL}, y_{D} = f(x_{Th}), x_{LL} = f(z_{Th}),
x_{Th} = f(x_{Fr}), z_{Th} = x_{Fr}}

And again after applying rule 2, rule 13 is applicable to the last equation. Knowing the example, it becomes clear that equations of the form z_{We} = x_{Fr} can not be well sorted solved. This can be detected during the unification process. As there are only finitely many possibilities of combining variables of two different sorts (days of the week), after some more steps an equation will arise which we tried to solve before (modulo renaming). The algorithm stucks in a loop. This fact can be detected and results in the following algorithm.

Algorithm 7.3.1 (Loop Detection) We attach to a unification problem Γ a set of equations E_{Γ}. Initially we put E_{Γ} = Γ. The straightforward way to implement the unification algorithm is to work on a list of open unification problems. Always the first problem is selected, all rules are applied and the new unification problems are appended to the end of the list. Now we increment this unification algorithm by the following rules:

• After the application of the rules 5, 10 to the actual problem Γ, 12, and 13 the new equations are added to E_{Γ}.

• Every time a new equation is created or an equation is changed in the actual problem Γ, it is checked whether it occurs (modulo renaming) in E_{Γ}. If the equation occurs in E_{Γ}, the unification problem is suspended.

• No rules are applied to suspended problems.

• If there are only suspended problems left, all problems are deleted.

• If a problem Γ is solved, the set E_{Γ} is subtracted from all sets E_{Δ} of problems Δ which are not solved and still contained in the list. If after this operation no equation of Δ occurs in E_{Δ}, the suspendation of Δ is undone.

7.4 Reduction

Reduction techniques are an important tool in automated reasoning in order to restrict the search space. The general idea is to delete clauses which are not necessary for the derivation of the empty clause. We will discuss purity, tautology deletion and subsumption within CL_{S}.

7.4.1 Tautology Deletion

A clause is called a tautology if it contains two complementary literals. Obviously a tautology is valid in all interpretations. If CS is an unsatisfiable clause set containing a tautology C then CS \ {C} is still unsatisfiable. Therefore the clause C can be deleted.

In general we have to be careful while deleting tautologies, because application of the rules in a calculus may be restricted in a way such that some proofs can only be found using tautologies [BG90]. But this is not the case for CL_{S}. Thus we can delete tautologies without affecting completeness.

7.4.2 Purity Deletion

A clause C (or a literal) is called pure if no inference rule is applicable to at least one of it’s literals (to the literal). As a consequence this literal cannot be deleted by the application of an inference rule. Therefore the clause containing the literal cannot contribute to a derivation of the empty clause. Thus pure clauses can be deleted.

According to this definition adding purity deletion to our rules results in an (highly) incomplete (but highly restrictive) calculus. On one hand, nearly all clauses containing declarations can be deleted (e.g. see Example 4.2.4). On the other hand, even if we forbid the consideration of declarations as pure literals the rule is still too strong. For example in the clause set

\begin{matrix}(1) & \{Q(a)\} \\ (2) & \{¬Q(a), a< −S\} \\ (3) & \{P (x_{S})\} \\ (4) & \{¬P (y_{S})\} \end{matrix}

the literals a< −S, P (x_{S}) and ¬P (y_{S}) are pure if we choose L_{< −}^{C} = ∅ as the set of declarations considered in unification. But if we delete one of the clauses {P (x_{S})}, {¬P (y_{S})} we are no longer able to derive the empty clause. We can refute the clause set by resolving between (1)1 and (2)1

(5) {a< −S}

Change our set of declarations into L_{< −}^{C} = {(a< −S, ∅)} and derive the empty clause in one resolution step using (3)1 and (4)1

(6) □

The example shows that choosing L_{< −}^{C} is too strong for purity deletion. But it can easily be proved that choosing L_{< −}^{M} for purity deletion and disregarding declarations yields a complete calculus. Note that for the above example we have L_{< −}^{M} = {(a< −S, {¬Q(a)})} and using this set of declarations the literals P (x_{S}) and ¬P (y_{S}) are not pure.

7.4.3 Subsumption

Subsumption is the most important reduction rule for resolution based calculi. If C and D are two clauses and σ a substitution such that σ(C) ⊆ D, then C subsumes D. The clause D can be deleted. The deletion does not affect completeness because if we use D in a refutation we can replace D by C because C contains less literals and is more general.

The above definition is an intuitive definition of subsumption and has to be used carefully. For example, every factor D of a clause C is subsumed by C according to the above definition. But factors are needed in order to guarantee completeness. The crux here is to view clauses as sets of literals. If we view clauses as multisets of literals the application of a substitution to a clause does not merge literals and therefore a factor is no longer subsumed by it’s parent clause. This point is also stressed in [BG90]. From a computational point of view the detection of a clause which can be subsumed (or subsumes) by a different clause is an NP-complete problem [KN86]. Nevertheless subsumption is needed, because the deletion of a subsumed clause may avoid the generation of infinitely many clauses. Additionally, techniques [LO80, Ohl90, Soc91] have been developed in order to make the problem tractable in practise.

In our sorted logic we have to apply subsumption modulo well sorted unifiers (matchers). If we consider conditioned declarations in order to find the appropriate matcher the application of the matcher may add new literals to the clause. This makes the problem of deciding subsumption very hard. Thus we suggest to use L_{< −}^{U} to decide the well sortedness of the matcher. Then the problem has the same complexity than in the unsorted case, because sorted matching can be decided in polynomial time. We will show how to apply subsumption in Section 8.2.

7.5 Combination with Strategies

There are many strategies discussed in the literature (e.g. [CL73, Lov78]). The general idea is to restrict the application of inference rules to “useful steps”. The most famous and mostly applied strategy is the “Set of Support” (in the following SOS) strategy [WRC65]. SOS is implemented in nearly any automated reasoning system based on resolution.

The SOS strategy forbids resolution steps between clauses coming from the axioms. In order to be precise: If we want to prove Ax ⇒ Th where Ax is a set of axioms and Th a set of theorems we show that Ax ∧ ¬Th is unsatisfiable. As it does not make sense to assume Ax to be unsatisfiable, every proof must involve clauses coming from ¬Th. Thus it is sufficient to allow resolution steps between clauses coming from ¬Th and clauses coming from Ax only. In order to put it in other words: We forbid resolution steps between clauses coming from the axioms.

The SOS strategy is complete for unsorted first-order logic. It is not complete in combination with our sorted calculus, as the following example shows. If we want to prove

(Q(a) ∧ ∀x_{⊤} (Q(x_{⊤}) ⇒ x_{⊤}< −S) ∧ ∀x_{S} P (x_{S})) ⇒ ∃y_{S} P (y_{S})

we obtain the clause set

\begin{matrix}(1) & \{Q(a)\} \\ (2) & \{¬Q(x_{⊤}), x_{⊤}< −S\} \\ (3) & \{P (x_{S})\} \\ (4) & \{¬P (y_{S})\} \end{matrix}

where clause (4) comes from the negated theorem. The SOS strategy only allows resolution steps between clause (4) and one of the clauses (1), (2), or (3). Resolution between (3) and (4) produces the unification problem Γ = {x_{S} = y_{S}} which cannot be solved with respect to L_{< −}^{C} = ∅. Thus there is no inference rule applicable. But the clause set is unsatisfiable. From (1) and (2) we derive

(5) {a< −S}

and change L_{< −}^{C} = {a< −S}. Now the previous unification problem Γ is in solved form (we can no longer apply rule 7) and using (4) and (3) we conclude

(6) □

As SOS is s useful strategy (we will solve all examples in Chapter 8 using SOS), we are interested in a (complete) combination of SOS and our sorted calculus. There are several possibilities to overcome incompleteness:

a) We can choose L_{< −}^{M} for unification. The choice results in a complete calculus but as we pointed our at the end of Chapter 6 a consequence of choosing L_{< −}^{M} may be the lost of all advantages of the sorted machinery. Therefore we may allow a mixture of SOS steps with respect to L_{< −}^{M} and steps with respect to L_{< −}^{C}.

b) We can allow steps between clauses coming from the axioms but still use the inference rules with respect to L_{< −}^{C}. For example, we may allow one axiom step after six SOS steps. The axiom steps can be restricted to clauses containing declarations, i.e. we only allow steps between two clauses where at least one clause contains a declaration. c) We derive in the standard SOS way with respect to L_{< −}^{C} until the empty clause

is derived or no rule is applicable. If no step is possible we allow one step between axiom clauses as mentioned in b) and then try to continue with SOS. This strategy is again incomplete in general but tractable in practise.

All examples in Chapter 8 are solved with strategy c). There is no real disadvantage in using strategy a) or b), because the additional steps may lead to shorter proofs (e.g. see [MW92]).

Solving The Examples

Now we will discuss the solutions of the examples introduced in Section 3.3. We will refer to clauses and literals by their number using the format (clause number)literal number. For example in the Schubert’s Steamroller problem (see 4.2.4) (13)2 denotes the literal ¬M(z_{A}, x_{A}) in clause {E(x_{A}, y_{P}), ¬M(z_{A}, x_{A}), ¬E(z_{A}, v_{P}), E(x_{A}, z_{A})}.

Unification problems are denoted by the Greek letter Γ and an index which is a sequence of the digits 0 to 9. The idea is to represent the tree structure arising during the application of the unification algorithm. Thus if we have a problem Γ_{12} we know that Γ_{12} is the second problem stemming from Γ_{1} after the application of a rule of the algorithm. We have used this convention in Section 6.2.

8.1 Schubert’s Steamroller

Schubert’s Steamroller is one of the most famous examples showing the efficiency of sorted deduction. It represents a standard example in automated theorem proving. It can also be solved using techniques different to sorted reasoning, e.g. URresolution (unit resulting resolution [AO83, MOW76]) or other strategies [BLS87]. We just want to show that our approach works in the same way the much simpler logics of [Wal87, SS89] do, if the formulas are simple. The starting clause set computed in Example 4.2.4 is

(1) {x_{W} < −A}  (2) {x_{F} < −A}  (3) {x_{B}< −A}
(4) {x_{C}< −A}  (5) {x_{S}< −A}  (6) {lupo< −W }
(7) {foxy< −F }  (8) {tweety< −B}  (9) {raupy< −C}
(10) {schnecky< −S} (11) {muesli< −G}  (12) {x_{G}< −P }
(13) {E(x_{A}, y_{P}), ¬M(z_{A}, x_{A}), ¬E(z_{A}, v_{P}), E(x_{A}, z_{A})}
(14) {M(x_{C}, z_{B})} (15) {M(y_{S}, z_{B})}  (16) {M(z_{B}, x_{F})}
(17) {M(x_{F} , y_{W})} (18) {¬E(z_{W} , y_{F})} (19) {¬E(z_{W} , x_{G})}
(20) {E(x_{B}, y_{C})}  (21) {¬E(x_{B}, z_{S})} (22) {E(x_{C}, f(x_{C}))}
(23) {f(x_{C})< −P }  (24) {E(x_{S}, g(x_{S}))} (25) {g(x_{S})< −P }
(26) {¬E(x_{A}, y_{A}), ¬E(y_{A}, z_{G})}

For this example we have L_{< −}^{C} = L_{< −}^{M} = L_{< −}^{U} = {(1)1 − (12)1, (23)1, (25)1}. This fact (L_{< −}^{C} = L_{< −}^{M} = L_{< −}^{U}) is characteristic for a representation of the logics of [Wal87, SS89] in our logic. It may happen that Skolemization (see Example 4.2.3) results in conditioned declarations in our logic but in unconditioned declarations in the logic of [Wal87, SS89]. In order to overcome this, we have to optimize the CNF-algorithm 4.2.2 (especially Step 5) by checking the non-emptiness of the sorts involved in Skolemization. The refutation performs as follows (we present a linear proof found by the MKRP [OS91] theorem prover, which uses the logic of [Wal87]):

(27) {E(x_{A}, y_{P}), ¬M(y_{A}, x_{A}), ¬E(y_{A}, v_{P}), ¬E(y_{A}, z_{G})}

Resolution between (26)1 and (13)4 (28) {E(x_{A}, y_{P}), ¬M(y_{A}, x_{A}), ¬E(y_{A}, z_{G})}

Factorization between (27)3 and (27)4 (29) {¬M(y_{A}, x_{W}), ¬E(y_{A}, z_{G})}

Resolution between (28)1 and (19)1 (30) {¬E(x_{F} , z_{G})}

Resolution between (29)1 and (17)1 (31) {¬M(z_{A}, x_{F}), ¬E(z_{A}, v_{P}), E(x_{F} , z_{A})} Resolution between (30)1 and (13)1

(32) {¬E(z_{B}, v_{P}), E(x_{F} , z_{B})} Resolution between (31)1 and (16)1

(33) {¬E(z_{B}, v_{P}), ¬E(x_{B}, z_{G})} Resolution between (32)2 and (26)1

(34) {¬E(x_{B}, z_{G})} Factorization between (33)1 and (33)2

(35) {¬M(z_{A}, x_{B}), ¬E(z_{A}, v_{P}), E(x_{B}, z_{A})} Resolution between (34)1 and (13)1

(36) {¬E(y_{S}, v_{P}), E(x_{B}, y_{S})} Resolution between (35)1 and (15)1

(37) {E(x_{B}, x_{S})} Resolution between (36)1 and (24)1

(38) □

Resolution between (37)1 and (21)1

Unification for this example is straightforward, as we only have declarations occurring in unit clauses and all sorts are non-empty from the beginning.

8.2 The Lion and the Unicorn

The Lion and the Unicorn example can be seen as a descendant of Schubert’s Steamroller. It is more difficult, because the sorts are not interpreted as finite sets in the initial model. Therefore the techniques developed in [AO83, MOW76] are not successful and the mechanism given in [BLS87] cannot be applied. We will discuss the problem at the end of this section in greater detail. Let us now just prove the theorem. Here is the clause set given after optimization (see Section 7.1.2):

(1) {mon< −Mo}  (2) {tue< −Tu}  (3) {wed< −We}
(4) {thu< −Th}  (5) {fri< −Fr}  (6) {sat< −Sa}
(7) {sun< −Su}  (8) {x_{Mo}< −LL}  (9) {x_{Tu}< −LL}
(10) {x_{We}< −LL}  (11) {x_{Th}< −| LL}  (12) {x_{Fr}< −| LL}
(13) {x_{Sa}< −| LL}  (14) {x_{Su}< −| LL}  (15) {x_{Th}< −LU}
(16) {x_{Fr}< −LU}  (17) {x_{Sa}< −LU}  (18) {x_{Su}< −| LU}
(19) {x_{Mo}< −| LU} (20) {x_{Tu}< −| LU}  (21) {x_{We}< −| LU}
(22) {x_{Mo}< −D}  (23) {x_{Tu}< −D}  (24) {x_{We}< −D}
(25) {x_{Th}< −D}  (26) {x_{Fr}< −D}  (27) {x_{Sa}< −D}
(28) {x_{Su}< −D}  (29) {x_{LL}< −D}  (30) {x_{LU} < −D}
(31) {lion< −C}  (32) {uni< −C}  (33) {f(x_{Mo})< −Su}
(34) {f(x_{Tu})< −Mo} (35) {f(x_{We})< −Tu} (36) {f(x_{Th})< −We}
(37) {f(x_{Fr})< −Th} (38) {f(x_{Sa})< −Fr} (39) {f(x_{Su})< −Sa}
(40) {x_{D}< −LL, ¬Lies(lion, x_{D}, y_{D}), y_{D}< −LL}
(41) {x_{D}< −LL, Lies(lion, x_{D}, y_{LL})}
(42) {¬Lies(lion, x_{LL}, y_{LL})}
(43) {Lies(lion, x_{LL}, y_{D}), y_{D}< −LL}
(44) {x_{D}< −LU, ¬Lies(uni, x_{D}, y_{D}), y_{D}< −LU}
(45) {x_{D}< −LU, Lies(uni, x_{D}, y_{LU} )}
(46) {¬Lies(uni, x_{LU} , y_{LU} )}
(47) {Lies(uni, x_{LU} , y_{D}), y_{D}< −LU}
(48) {¬Lies(lion, x_{D}, f(x_{D})), ¬Lies(uni, x_{D}, f(x_{D}))}

We choose L_{< −}^{C} = {(1)1 − (10)1, (15)1 − (17)1, (22)1 − (39)1} and refute the problem using an SOS strategy. The initial set of support consists of the theorem clause {¬Lies(lion, x_{D}, f(x_{D})), ¬Lies(uni, x_{D}, f(x_{D}))} only. There are two resolution possibilities for the literal ¬Lies(lion, x_{D}, f(x_{D})). We can resolve (48)1 and (43)1 or (48)1 and (41)1. We start examination of sorted unification between (48)1 and (43)1. The original unification problem is

Γ_{0} = {lion = lion, x_{D} = x_{LL}, y_{D} = f(x_{D})}

Applying the rules 5 (to the first equation) and 2 (using the second equation) we get

Γ_{01} = {x_{D} = x_{LL}, y_{D} = f(x_{LL})}

Here only rule 10 is applicable to the second equation which yields the following the seven problems

Γ_{011} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Mo}}
Γ_{012} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Tu}}
Γ_{013} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{We}}
Γ_{014} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Th}}
Γ_{015} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Fr}}
Γ_{016} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Sa}}
Γ_{017} = {x_{D} = x_{LL}, y_{D} = f(x_{LL}), x_{LL} = x_{Su}}

The problems Γ_{014}-Γ_{017} can be deleted by applying Algorithm 7.3.1 to the problems (see also Section 7.3). Applying rule 3 (using the third equation) once we get the three solved problems

Γ_{0111} = {x_{D} = x_{Mo}, y_{D} = f(x_{Mo}), x_{LL} = x_{Mo}}
Γ_{0121} = {x_{D} = x_{Tu}, y_{D} = f(x_{Tu}), x_{LL} = x_{Tu}}
Γ_{0131} = {x_{D} = x_{We}, y_{D} = f(x_{We}), x_{LL} = x_{We}}

These three problems yield the three resolvents

(49) {¬Lies(uni, x_{Mo}, f(x_{Mo})), f(x_{Mo})< −LL}
(50) {¬Lies(uni, x_{Tu}, f(x_{Tu})), f(x_{Tu})< −LL}
(51) {¬Lies(uni, x_{We}, f(x_{We})), f(x_{We})< −LL}

The clauses (50) and (51) are subsumed by the clauses (8) and (9) respectively. Thus we only add (49) to the set of support. Building a resolvent between (48)1 and (41)1 is analogous to the previous step. Three clauses are generated, two can be subsumed and thus the new set of support contains

(49) {¬Lies(uni, x_{Mo}, f(x_{Mo})), f(x_{Mo})< −LL}
(52) {¬Lies(uni, x_{Th}, f(x_{Th})), x_{Th}< −LL}

The first literal of clause (49) is pure with respect to L_{< −}^{C}. The literal (49)1 is not pure with respect to L_{< −}^{M}, because (x_{D}< −LU, {Lies(uni, x_{D}, y_{LU} )})∈L_{< −}^{M}. In section 7.4.2 we explained that we must not delete the clause but because no inference rule is applicable to the literal, we continue with clause (52). Again there are two candidates for the literal (52)1: (47)1 and (45)1. The unification problem resulting from (45)1 cannot be well sorted solved, because f(x_{Th})∉T_{L< −^{C},LU} . Therefore the only possible step is to resolve (52)1 and (47)1 leading to

(55) {x_{Th}< −LL, f(x_{Th})< −LU}

The only resolution possibility for (55)1 is (11)1 and we obtain

(56) {f(x_{Th})< −LU}

Finally for (56)1 the only applicable step is resolution with (21)1 and we result in the empty clause

(57) □

We needed 6 resolution steps to refute the clause set and the initial branching rate of the search tree is 8 (with a SOS strategy). We constructed 9 clauses to explore the search space where 4 clauses are deleted by subsumption. In [WO90] we refuted the problem after 15 steps. Our new approach is faster because it uses sorted unification instead of adding negative declarations which are deleted by resolution.

The “Lion and the Unicorn” example is non trivial for unsorted theorem provers. An unsorted theorem prover needs 25 resolution steps to refute the clause set and the initial branching rate is 17 (with a SOS strategy). Especially if we increase the nesting depth of the f function in the theorem,

{¬Lies(lion, x_{D}, f(f(x_{D}))), ¬Lies(uni, x_{D}, f(f(x_{D})))}

the search space can become arbitrarily complex in unsorted logic whereas our sorted calculus has no problem, because the effect of the nesting depth on the complexity of the unification problem can be bound by some polynomial. For example, if we use the above theorem, the first unification problem is

Γ_{0} = {lion = lion, x_{D} = x_{LL}, y_{D} = f(f(x_{D}))}

After eliminating the first equation with rule 5, application of rule 2 using the second equation and using the sorted rule 10 and rule 3 we again get seven problems:

Γ_{011} = {x_{D} = x_{LL}, y_{D} = f(f(x_{LL})), x_{Mo} = f(x_{LL})}
Γ_{012} = {x_{D} = x_{LL}, y_{D} = f(f(x_{LL})), x_{Tu} = f(x_{LL})}
Γ_{013} = {x_{D} = x_{LL}, y_{D} = f(f(x_{LL})), x_{We} = f(x_{LL})}
Γ_{014} = {x_{D} = x_{LL}, y_{D} = f(f(x_{LL})), x_{Th} = f(x_{LL})}
Γ_{015} = {x_{D} = x_{LL}, y_{D} = f(f(x_{LL})), x_{Fr} = f(x_{LL})}
Γ_{016} = {x_{D} = x_{LL}, y_{D} = f(f(x_{LL})), x_{Sa} = f(x_{LL})}
Γ_{017} = {x_{D} = x_{LL}, y_{D} = f(f(x_{LL})), x_{Su} = f(x_{LL})}

Again four problems can be deleted applying Algorithm 7.3.1, namely Γ_{013} to Γ_{016}. The other problems can be solved in the same way than before. Thus the additional nesting depth of the f does not cause additional unification problems. Therefore the effect of the nesting to the complexity of the unification problem can be bound polynomially.

In contrast the increased nesting of the f function causes an exploding search space for an unsorted theorem prover. We gave the examples to OTTER (version 2.0, binary resolution) and got the following statistics.

Nesting Depth Clauses generated
1  64600
2  181486
3  1367151

That means OTTER generated 1367151 clauses in order to prove the theorem clause

{¬Lies(lion, x_{D}, f(f(f(x_{D})))), ¬Lies(uni, x_{D}, f(f(f(x_{D}))))}

and was not able to succeed with nesting depth 4 in reasonable time. We tested OTTER also with UR-resolution and gave the prover the clauses (1) to (7) as initial SOS. UR-resolution performed much better:

Nesting Depth Clauses generated
1  1664
2  2943
3  4761
4  6971
5  9627
6  12675

8.3 Condensed Detachment

We solve the problem using a set of support strategy. The problem is not a hard problem, e.g. OTTER [McC90b, McC90a] can solve the problem in less than one second. But we will show that in the sorted formalization the problem can be solved without any search. Here is the final clause set from Section 7.1.1.

\begin{matrix}(1) & \{i(x_{P} , y_{⊤}))< −| P, y_{⊤}< −P \} \\ (2) & \{i(i(x_{⊤}, y_{⊤}), i(i(y_{⊤}, z_{⊤}), i(x_{⊤}, z_{⊤})))< −P \} \\ (3) & \{i(i(n(x_{⊤}), x_{⊤}), x_{⊤})< −P \} \\ (4) & \{i(x_{⊤}, i(n(x_{⊤}), y_{⊤}))< −P \} \\ (5) & \{i(a, a)< −| P \} \end{matrix}

The initial set of support consists of the clause {i(a, a)< −| P } only. The set L_{< −}^{C} = {i(i(x_{⊤}, y_{⊤}), i(i(y_{⊤}, z_{⊤}), i(x_{⊤}, z_{⊤})))< −P, i(i(n(x_{⊤}), x_{⊤}), x_{⊤})< −P, i(x_{⊤}, i(n(x_{⊤}), y_{⊤}))< −P } and it contains no conditioned declarations. Therefore we skip the additional notations needed to represent conditioned objects. The only applicable step is resolution with (1)2, because unification with one of the literals (2)1, (3)1 or (4)1 results in a function symbol clash. The corresponding unification problem is

Γ_{0} = {y_{⊤} = i(a, a)}

which is still in solved form, as i(a, a)∈T_{L< −^{C},⊤}. Thus we add the new clause

(6) {i(x_{P} , i(a, a))< −| P }

to the set of support. The new clause cannot be resolved with clauses (2) and (4) because of a function clash and unification with the literal (3)1 results in the unification problem

Γ_{1} = {x_{P} = i(n(x_{⊤}), x_{⊤}), x_{⊤} = i(a, a)}

which can not be well sorted solved, because i(n(i(a, a)), i(a, a))∉T_{L< −^{C},P}. Again the only possible step is resolution with clause (1) yielding

(7) {i(x_{P} , i(x′_{P} , i(a, a)))< −| P }

Trying to build a resolvent between (7) and (3) or (4) again leads to unification problems which cannot be well sorted solved. Resolution with clause (2) gives the unification problem

Γ_{2} = {x_{P} = i(x_{⊤}, y_{⊤}), x′_{P} = i(y_{⊤}, z_{⊤}), x_{⊤} = a, z_{⊤} = a}

Applying rule 2 of the unification algorithm using the equations x_{⊤} = a and z_{⊤} = a twice, we obtain

Γ_{21} = {x_{P} = i(a, y_{⊤}), x′_{P} = i(y_{⊤}, a), x_{⊤} = a, z_{⊤} = a}

We don’t have i(a, y_{⊤})∈T_{L< −^{C},P} or i(y_{⊤}, a)∈T_{L< −^{C},P}. Application of rule 10 to the equation x_{P} = i(a, y_{⊤}) using the declaration i(x_{⊤}, i(n(x_{⊤}), y_{⊤}))< −P yields

Γ_{211} = {\{x_{P} = i(a, y_{⊤}), x′_{P} = i(y_{⊤}, a), x_{⊤} = a, z_{⊤} = a, \atop y_{⊤} = i(n(x′_{⊤}), y′_{⊤}), x′_{⊤} = a\}}

Following rule 2 we use the new equations y_{⊤} = i(n(x′_{⊤}), y′_{⊤}) and x′_{⊤} = a as substitutions and result in

Γ_{2111} = {\{x_{P} = i(a, i(n(a), y′_{⊤})), x′_{P} = i(i(n(a), y′_{⊤}), a), \atop x_{⊤} = a, z_{⊤} = a, y_{⊤} = i(n(a), y′_{⊤}), x′_{⊤} = a\}}

The first equation is now well sorted solved, i.e. i(a, i(n(a), y′_{⊤}))∈T_{L< −^{C},P}. But for the second equation we still have i(i(n(a), y′_{⊤}), a)∉T_{L< −^{C},P}. Applying rule 10 using the declaration i(i(n(x_{⊤}), x_{⊤}), x_{⊤})< −P solves this last problem.

Γ_{21111} = {x_{P} = i(a, i(n(a), y′_{⊤})), x′_{P} = i(i(n(a), y′_{⊤}), a), ; x_{⊤} = a, z_{⊤} = a, y_{⊤} = i(n(a), y′_{⊤}), x′_{⊤} = a, ; i(i(n(a), y′_{⊤}), a) = i(i(n(x′′_{⊤}), x′′_{⊤}), x′′_{⊤})}

After applying the rules 5, 3 and 2 to the equation i(i(n(a), y′_{⊤}), a) = i(i(n(x′′_{⊤}), x′′_{⊤}), x′′_{⊤}) and it’s descendants we finish in the solved problem

Γ_{211111} = {x_{P} = i(a, i(n(a), a)), x′_{P} = i(i(n(a), a), a), ; x_{⊤} = a, z_{⊤} = a, y_{⊤} = i(n(a), a), x′_{⊤} = a, ; y′_{⊤} = a, x′′_{⊤} = a)}

and derive

(8) □

Note that the solution of the unification problem Γ_{2} is unique and computationally simple. Comparing our solution to the proof found by OTTER (version 2.0, binary resolution), we needed only 3 steps to refute the clause set, while OTTER made 5 steps. The missing 2 steps occur in the solution of the unification problem Γ_{2}. The most important difference is that the sorted proof was found without any search, i.e. we did not generate useless resolvents. OTTER produced 60 clauses to find the empty clause. Here is OTTER’s solution to the unsorted formalization:

(1) {¬P (i(x, y)), ¬P (x), P (y)}
(2) {P (i(i(x, y), i(i(y, z), i(x, z))))}
(3) {P (i(i(n(x), x), x))}
(4) {P (i(x, i(n(x), y)))}
(5) {¬P (i(a, a))}

(6) {¬P (i(x, i(a, a))), ¬P (x)} Resolution between (5)1 and (1)2

(7) {¬P (x), ¬P (i(x′, i(x, i(a, a)))), ¬P (x′)} Resolution between (6)1 and (1)2

(8) {¬P (i(x, a)), ¬P (i(a, x))} Resolution between (7)2 and (2)1

(9) {¬P (i(a, i(n(a), a)))} Resolution between (8)1 and (3)1

(10) □ Resolution between (9)1 and (4)1

Conclusion

We have presented a sound and complete calculus for the logic L_{S}. This logic L_{S} is currently the most general sorted logic known as it allows sort declarations to be used arbitrarily as ordinary atoms. Nevertheless deductions in the calculus CL_{S} are efficient and the calculus is a conservative extension of existing approaches.

All known sorted calculi [Wal87, SS89, Fri89, BHPS89, Coh87] allow only declarations of the kind S ⊑ T (expressing that S is a subsort of T) or t: S (expressing that the term t has sort S). Translating these declarations into L_{S} results in the unit clauses x_{S}< −T and t< −S, respectively. Hence the sort information for these logics which is used in the unification algorithm corresponds to a set of unit clauses containing declarations in L_{S}. As there are only unit clauses after the translation we have L_{< −}^{U} = L_{< −}^{C}. Hence, all chosen declarations have an empty condition part. For declarations with empty condition part the definition of conditioned well sorted terms simplifies to the definition of well sorted terms (see Section 1.2.1 and Definition 6.1.2). Therefore the new notion of well sortedness is exactly the same notion as in the existing logics. Thus the unification algorithm using conditioned well sortedness collapses to the known unification algorithms using well sortedness and the new calculus has exactly the same behaviour as the simpler sorted calculi. Here we have the very nice feature that the calculus CL_{S} for the general logic L_{S} is as efficient as special calculi designed for sublanguages.

For clause sets containing declarations in non unit clauses the calculus must be compared to unsorted resolution as all approaches known so far can not exploit conditioned declarations for sorted reasoning. In Chapter 8 we showed that the CL_{S} calculus improves efficiency significantly, if one place predicates (sorts) are involved in the reasoning process.

An open theoretical question is the incorporation of equality into L_{S}. It is well know that this is in general not without problems [SS89]. But we believe that our main idea, i.e. not to separate the information about sorts from the rest of the formulas is a good basis to overcome these problems.

Bibliography

[AB70] R. Anderson and W.W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. Journal of the ACM, 17:525–534, July 1970.

[AO83] G. Antoniou and H.J. Ohlbach. Terminator. In A. Bundy, editor, Proc. of 8th International Joint Conference on Artificial Intelligence, IJCAI-83, pages 916–919, 1983.

[BG90] L. Bachmair and H. Ganzinger. On restrictions of ordered paramodulation with simplification. In 10th International Conference on Automated Deduction, pages 427–441. Springer Verlag, 1990.

[BHPS89] C. Beierle, U. Hedstueck, U. Pletat, and J. Siekmann. An order sorted predicate logic with closely coupled taxonomic information. LILOG-Report 86, IBM Germany, Scientific Center, 1989. To appear in Artificial Intelligence.

[BLS87] W. Bibel, R. Letz, and J. Schumann. Bottom-up enhancements of deductive systems. In Conference on Artificial Intelligence and Information - Control Systems of Robots 1987. North-Holland, 1987.

[BS85] R.J. Brachmann and J.G. Schmolze. An overview of the KL-ONE knowledge representation system. Cognitive Science, 9(2):171–216, 1985.

[Bue91] H.J. Buerckert. Constraint resolution. Lecture Notes in Artificial Intelligence. Springer Verlag, 1991.

[CL73] C.L. Chang and R.C.T. Lee. Symbolic Logic and Mechanical Theorem Proving. Computer Science and Applied Mathematics. Academic Press, 1973.

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

[Fri89] 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.

[Gal86] J.H. Gallier. Logic for Computer Science. Harper & Row, 1986.

[KN86] D. Kapur and P. Narendran. Np-completeness of the set unification and matching problems. In 8th International Conference on Automated Deduction, pages 489–495. Springer Verlag, 1986.

[LO80] E. Lusk and R. Overbeek. Data structures and control architectures for the implementation of theorem proving programs. In 5th International Conference on Automated Deduction, pages 232–249. Springer Verlag, 1980.

[Lov78] D. Loveland. Automated Theorem Proving: A Logical Basis, volume 6 of Fundamental Studies in Computer Science. North-Holland, 1978.

[McC90a] W. McCune. Otter 2.0. In 10th International Conference on Automated Deduction, pages 663–664. Springer Verlag, 1990.

[McC90b] W. McCune. Otter 2.0 users guide. Report ANL-90 9, Argonne National Laboratory, March 1990.

[Mer77] D. Meredith. In memoriam carew arthur meredith (1904-1976). Notre Dame Journal of Formal Logic, 18(513-516), 1977.

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

[MOW76] J.D. McCharen, R. Overbeek, and L. Wos. Complexity and related enhancements for automated theorem-proving programs. Computers and Mathematics with Applications, 2:1–16, 1976.

[MW92] W. McCune and L. Wos. Experiments in automated deduction with condensed detachment. In 11th International Conference on Automated Deduction. Springer Verlag, 1992.

[Ohl90] H.J. Ohlbach. Abstraction tree indexing for terms. In Proceedings of the 9th European Conference on Artificial Intelligence, pages 479–484. Pitman Publishing, London, August 1990.

[OS91] H.J. Ohlbach and J.H. Siekmann. The markgraf karl refutation procedure. In J.L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 41–112. MIT Press, 1991.

[OSS85] H.J. Ohlbach and M. Schmidt-Schauss. The lion and the unicorn. Journal of Automated Reasoning, 1(3):327–332, 1985.

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

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

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

[Smu78] R. Smullyan. What is the name of this book ? Prentice-Hall, 1978.

[Soc90] R. Socher. Simplification and Reduction for Automated Theorem Proving. PhD thesis, Universitaet Kaiserslautern, 1990. Partially published in JAR.

[Soc91] R. Socher. Optimizing the clausal normal form transformation. Journal of Automated Reasoning, 7(3):325–336, 1991.

[SS89] M. Schmidt-Schauss. Computational aspects of an order sorted logic with term declarations. Lecture Notes in Artificial Intelligence. Springer Verlag, 1989.

[Sti85] M. Stickel. Theory resolution. Journal of Automated Reasoning, 1(4):333–355, 1985.

[Sti86] M. Stickel. Schubert’s steamroller problem: Formulations and solutions. Journal of Automated Reasoning, 2(1), 1986.

[Wal84] C. Walther. A mechanical solution of schubert’s steamroller by manysorted resolution. In Proceedings of the 4th AAAI, pages 330–334, 1984. revised version in Artificial Intelligence (26)2:217-224, 1985.

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

[WO90] 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.

[WRC65] L. Wos, G.A. Robinson, and D.F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM, 12(4):536–541, 1965.