Apuntes de Lógica y Programación Lógica

Jaime Lipton

Universidad Politécnica de Madrid 1 de Diciembre, 1997

Contents

I Induction, Algebras and Elements of Logic 2

1 Preliminaries: Induction, Closure 3 1.1 The induction schemes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Inductively defined structures and term algebras. . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Closure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.4 Lattices, Continuity and Fixed Points . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

II Notes on Horn Clause Programs and SLD Resolution (Release 0.93) (Notas para el curso de Doctorado sobre el λProlog, UPM, 1997) 11

2 Horn Clause Programs: The Classical Theory 12

2.1 Propositional Horn Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.1.1 SLD proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.1.2 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

2.2 Herbrand’s Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.2.1 A thumbnail review of completeness theorems for predicate logic . . . . . . . . . . 17 2.2.2 Completeness for Π_{1}^{0}-sentences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

2.3 Predicate Logic Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.4 Fixpoint Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

3 Uniform Proofs 22 3.1 Cut elimination and Uniform Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

Part I

Chapter 1

Induction, Algebras and Elements of Logic Preliminaries: Induction, Closure

1.1 The induction schemes

We begin by reviewing the principle of mathematical induction in various forms. We first consider induction on the natural numbers. We will need to discuss properties P (x) of natural numbers x. For example

P (x) ≡^{def} x is prime .

For the time being we will not make precise what we mean by a property. Once we introduce formal logic, a property will be a formula in predicate logic. Properties of natural numbers are closely related to sets of natural numbers: if S is a subset of ℕ say the set of prime numbers, then a statement of membership in S

x ∈ S

is a way of saying “x is prime.” The set of numbers with property P is written

{x ∈ ℕ |P (x)}.

Definition 1.1.1 Let P be a property of natural numbers. Then the following formula is called the induction axiom for P

Ind_{P} :  [ \underbrace{P (0)}_{if 0 has property P}  ^{&}_{and}  \underbrace{∀x}_{for every x}  (\underbrace{P (x) → P (x + 1)}_{P (x) implies P (x + 1)}) ] \overrightarrow{}_{then}  \underbrace{∀xP (x).}_{P holds for every x.}

Expressed informally, the axiom says: if we establish that

• P (0) is true, and

• whenever P (x) is true then P (x + 1) is true.

then we have shown that P (x) holds for every natural number x. We distinguish between the induction axiom Ind_{P} and the induction scheme ( Ind) which is the (infinite) set of axioms Ind_{P}, one for every property P.

Now we look at alternative formulations of induction that will prove useful.

Definition 1.1.2 We define course-of-values induction for the property P to be the axiom

COV_{P} :  ∀x[(∀y < xP (y)) → P (x)] → ∀xP (x)  (1.1)

i.e. if we can show that P is a property satisfying the condition:

whenever it holds for every y < x it must also hold for x then P is true of all x.

Note that it is not necessary to establish P (0) since this actually follows from the definition.

Definition 1.1.3 Let P be a property of natural numbers. The least number principle for P is the axiom: if there is any number x for which P holds then there is a smallest one. Written in the rather dry style of first-order logic:

LN_{P} ∃x(P (x)) → ∃x[P (x)^{&} ∀y(P (y) → x ≤ y)].  (1.2)

Equivalently, LN_{P} says: every nonempty subset of ℕ has a least element.

As with Ind we can also define the COV - scheme to be the collection of axioms COV_{P} for every P and the LN-scheme to be the set of axioms LN_{P}^{1}

Theorem 1.1.4 The following are equivalent (as schemes):

1. Ind

2. COV

3. LN

proof. Exercise!

We can generalize the least number principle to a condition on any partial order (of any size) so as to guarantee that a suitable rephrasing of the COV scheme will continue to hold.

Definition 1.1.5 A partial order A = ⟨A, ≤_{A}⟩ is said to be well-founded if every nonempty subset S of A has an ≤_{A}-minimal element, that is to say, there is an element a ∈ S such that for no other x ∈ S do we have x ≤_{A} a.

Theorem 1.1.6 (transfinite induction) Let ⟨A, ≤_{A}⟩ be a well-founded partial order. Then for any property P

(∀x ∈ A)[(∀y <_{A} xP (y)) → P (x)] → (∀x ∈ A) P (x)

proof. Exercise.

Problem 1 A relation R on a set A is said to be well-founded if every nonempty subset S of A has an R-minimal member. Show that this condition is equivalent to saying that A has no infinite descending R-chain, i.e. for any countable sequence a_{1}, …, a_{n}, …, if

a_{2}Ra_{1} and a_{3}Ra_{2} and ⋯

then for some n and every i ≥ n we have a_{i} = a_{n}

1.2 Inductively defined structures and term algebras.

We define a signature Σ to be a sequence

Σ = ⟨c_{1}, c_{2}, ⋯; f_{1}, f_{2}, ⋯⟩

of constants Σ_{K} = ⟨c_{1}, c_{2}, ⋯⟩ and of function symbols Σ_{F} = ⟨f_{1}, f_{2}, ⋯⟩ each of which has a corresponding natural number called its arity. Arities are often not displayed, but when we want to do so we will use exponent-notation, as in ⟨a^{0}, b^{0}, c^{1}, f^{3}, g^{4}⟩, where arity 0 identifies constants^{2} A signature often captures the essential algebraic structure of some area of mathematics under study, e.g. for arithmetic, Σ = ⟨0, 1, +^{2}, ×^{2}⟩. In logic programming, signatures are created by the user through the text of the logic program. In other programming languages, user defined data constructors and destructors play a similar role.

1Warning: we are being very informal about what a property is here. These definitions, like those of COV and Ind will be made precise when we define first-order properties.

2In fact a constant can be thought of as a function of arity 0.

In this course we will usually only consider finite or countably infinite signatures. This is tacitly assumed in all relevant theorems unless otherwise stated.

Definition 1.2.1 Let Σ = {c_{1}, c_{2}, ⋯, f_{1}, f_{2}, ⋯} be a signature. A Σ-algebra

𝔄 = ⟨A, c_{1}^{𝔄}, c_{2}^{𝔄}, ⋯, f_{1}^{𝔄}, f_{2}^{𝔄}, ⋯⟩

is a set A (sometimes written | 𝔄 | and called the carrier set or underlying set of 𝔄), together with the following family of functions and constants:

• For each constant symbol c in Σ, a constant c^{𝔄} in A.

• For each function symbol f of arity n in Σ, a function f^{𝔄} : A^{n} → A.

Let 𝔄,𝔅 be two Σ-algebras. A Σ-algebra morphism φ : 𝔄 → 𝔅 is a function from | 𝔄 | to | 𝔅 | which “respects the Σ-structure”, that is to say, satisfying

1. For each constant c in Σ, φ(c^{𝔄}) = c^{B},

2. For each function symbol f in Σ of arity n and any a_{1}, …, a_{n} ∈ A,

φ(f^{𝔄}(a_{1}, …, a_{n})) = f^{B}(φ(a_{1}), …, φ(a_{n}))

Before looking at examples we will need to define the set T_{Σ} of Σ-terms.

Definition 1.2.2 Let Σ be a signature, and X a set of variables (a set of symbols disjoint from the signature Σ). The set of open Σ-terms over X is given by the following inductive definition.

1. If c is a constant in Σ then c is a term.

2. If x is a variable, x is a term.

3. If t_{1}, …, t_{n} are terms and f is a function symbol in Σ of arity n then ft_{1} ⋯ t_{n} is a term (sometimes also written f(t_{1}, …, t_{n})).

4. Nothing else is a term.

If a term has no variables it is called a ground term. We use the notation T_{Σ} to denote the set of of ground Σ-terms, and T_{Σ}(X) to denote the set of open terms over the set of variables X.

The terms t_{1}, …, t_{n} are called immediate subterms of ft_{1} ⋯ t_{n}.

The set of terms (open or ground) is inductively defined. The main significance of this in practice is that we can prove properties of terms by induction on this definition, so-called structural induction.

Definition 1.2.3 (Structural Induction) Suppose P is a property of terms such that

1. P (c) is true for every constant.

2. P (x) is true for every variable.

3. If f is a function symbol of arity n and t_{1}, …, t_{n} are terms, and P (t_{1}), …, P (t_{n}) are true, then P (ft_{1} ⋯ t_{n}) is also true. Said differently: if all immediate subterms of a term have the property P then so does the term.

Then every term has the property P.

Remark 1.2.4 Suitably formulated, this principle is a consequence of ordinary induction on the natural numbers. Observe that if we set

T_{Σ}^{0} = Σ_{K} ∪ X
T_{Σ}^{n+1} = T_{Σ}^{n} ∪ {ft_{1} ⋯ t_{n} : t_{j} ∈ T_{Σ}^{n} ^{&} f ∈ Σ_{F} }

then

T_{Σ} = ⋃ T_{Σ}^{n}.

We can then establish structural induction by showing, by induction on the natural numbers, that if the premisses 1 and 2 in the definition of structural induction hold, then P (t) is true for every member of T_{Σ}^{n} for every n. This is true for T_{Σ}^{0} by 1, and if P holds for every term in T_{Σ}^{n} it must hold for every term in T_{Σ}^{n+1} by premiss 2.

It only remains to add that, as stated, the property P does not appear to be a first-order property of natural numbers, but of terms as well. We can either accept this as a strengthening of induction on ℕ , or we can resort to Gödel-numbering to define terms as natural number codes.

Now we need some examples of Σ-algebras. Let’s pick a familiar signature, namely that of arithmetic: Σ = ⟨0, 1, +^{2}, ×^{2}⟩. It will be important in this example to carefully distinguish the constant symbol 0, which has no a priori meaning, from the natural number 0. We consider two Σ-algebras.

1. Let 𝔑 = ⟨ℕ, 0^{𝔑}, 1^{𝔑}, +^{𝔑}, ×^{𝔑}⟩ be the so-called “standard model”, with carrier set the natural numbers ℕ, and with the usual interpretations: 0^{𝔑} = 0, 1^{𝔑} = 1 and +^{𝔑}, ×^{𝔑} ordinary addition and multiplication.

2. Now we consider the so-called term algebra T_{Σ}, given by:

T_{Σ} = ⟨T_{Σ}, 0^{T_{Σ}}, 1^{T} , ⊕, ⊗⟩

where T_{Σ} is the set of ground terms over Σ, and 0^{T_{Σ}} = 0, and 1^{T_{Σ}} = 1 (i.e. 0 and 1 are interpreted as themselves viewed as atomic terms) and

⊕(t_{1}, t_{2}) = +t_{1}t_{2}
⊗(t_{1}, t_{2}) = ×t_{1}t_{2}

We now give the definition of (open) term algebra for arbitrary signatures.

Definition 1.2.5 Let Σ = ⟨c_{1}, c_{2}, …; f_{1}, f_{2}, …⟩ be a signature and X a set of variables. We define the Σ-algebra T_{Σ}(X) = ⟨utcx; c_{1}^{T_{Σ}(X)}, c_{2}^{T_{Σ}(X)}; f_{1}^{T_{Σ}(X)}, f_{2}^{T_{Σ}(X)}, …⟩ by:

c_{j}^{T_{Σ}(X)} = c_{j}
f_{j}^{T_{Σ}(X)}(t_{1}, …, t_{n}) = ft_{1} ⋯ t_{n}

Note that if we let X = ∅ this gives the definition of the algebra of ground terms.

Theorem 1.2.6 For any signature Σ, and any Σ-algebra 𝔄, there is a unique Σ-morphism ι_{𝔄} from T_{Σ} to 𝔄.

If X is a set of variables and η : X → |𝔄| an arbitrary function (called an 𝔄-environment for X) then there is a unique Σ-morphism T_{Σ}(X) ^{η̂} 𝔄 such that for every x in X, η̂(x) = η(x). In diagram form:

X  \overline{\begin{matrix}⊂ \\  \end{matrix}}T_{Σ}(X)  T_{Σ}(X)

[figure: η]

[figure: |𝔄|; η̂; . . . . . . . . .; 𝔄; η̂; . . . . . . . . .]

where the right hand diagram shows that the map η̂ is a Σ-morphism.

This property of T_{Σ}(X)is often stated thus: T_{Σ}is a free Σ-algebra over X. proof: Exercise

Yet another way to state the freeness property of T_{Σ}(X)is as follows:

For every map of sets X ^{η} U(𝔄), where U(𝔄) is the underlying set of 𝔄, there is a unique Σ-morphism T_{Σ}(X) ^{η̂} 𝔄 and conversely.

This information is displayed thus:

\frac{X ^{η} U(𝔄)}{T_{Σ}(X) ^{η̂} 𝔄}.

This is called an adjoint situation and the operator T_{Σ} is said to be a left adjoint of the operator U.

1.3 Closure

A set S is said to be closed under an operation if the operation can be applied to any members of S and produce an output in S. Sometimes sets are not closed under some natural operation, and we must construct a minimal extension that will be closed, called a closure. Here are the definitions.

Definition 1.3.1 Let S be a set, A a subset of S and f a k-ary function on S. Then we say A is closed under f if for every k-tuple a_{1}, …, a_{k} of elements from A, we have f(a_{1}, …, a_{k}) ∈ A.

Some examples: the subset {1, 2, 3} of ℕ is not closed under addition: 2 + 3 is not in the set, we have to go outside it for answers. If the set were our universe of discourse we would have to call + a partial or incomplete operation. On the other hand, the set {−1, 0, 1} is closed under multiplication.

Suppose we started with {2, 4, 6} and wanted to add only the numbers required to make it closed under addition. We would have to add 2 + 2, 2 + 2 + 2, 6 + 6 + 4, 4 + 4, etc. Would we have to add all the natural numbers?

Definition 1.3.2 Let S be a set, A a subset, and F a set of functions on S. We define Â to be the closure of A under F if it satisfies:

1. A ⊆ Â.

2. Â is closed under every function in F.

3. Â is the smallest such set: if B contains A and is closed under all functions in F then Â ⊆ B.

How do we know such a set always exists? You can construct it, from below, or from above. First from above.

Theorem 1.3.3 Let S be a set, A a subset, and F a set of functions on S. Then Â is the intersection of all closed subsets of S containing A.

Problem 2 Show that Â has the three required properties.

Let S, A, F be as in the theorem. Define

A_{0} = A  (1.3)
A_{n+1} = A_{n} ∪ {f(a_{1}, …, a_{k}) : f ∈ F and a_{1}, …, a_{k} ∈ A_{n}}  (1.4)

then we claim:

Theorem 1.3.4 Â = ⋃_{0}^{∞} A_{n}.

Problem 3 Prove the preceding theorem. To establish Â ⊆ ⋃_{0}^{∞} A_{n} show that ⋃_{0}^{∞} A_{n} is a closed subset of S. Then since Â is the intersection of all such, it must be smaller. To show the opposite contanment, prove, by induction on n, that each A_{n} ⊆ Â.

These notions can be stated in terms of algebras.

Definition 1.3.5 Let 𝔄 be a Σ-algebra, and E ⊆ |𝔄|. Then the subalgebra 𝔄(E) of 𝔄 generated by E is the smallest subalgebra of 𝔄 containing E.

It is easily seen that the algebra generated by E exists: it is the intersection of all subalgebras of 𝔄 containing E. If we denote by 𝔄_{K} and 𝔄_{F} the sets of constants c^{𝔄} and functions f^{𝔄} of 𝔄 corresponding to the constant and function symbols in Σ, it is precisely the closure of E ∪ 𝔄_{K} in |𝔄| under 𝔄_{F}.

We can also give a bottom-up description of 𝔄(E), using the approximations

𝔄^{0}(E) = E ∪ 𝔄_{K}
𝔄^{n+1}(E) = 𝔄^{n}(E) ∪ {f^{𝔄}(x_{1}, …, x_{m}) : x_{i} ∈ 𝔄^{n}(E)^{&} f ∈ Σ, m = arity of f}.

Lemma 1.3.6 Let 𝔄 be a Σ-algebra, and E ⊆ |𝔄|.

𝔄(E) = ⋃ 𝔄^{n}(E).

We conclude this section with a discussion of generating sets.

Definition 1.3.7 Let 𝔄 be a Σ-algebra, and E ⊆ |𝔄|. Then E is said to generate 𝔄 if

𝔄(E) = 𝔄.

Observe that generating sets always exist: 𝔄 is generated by |𝔄|. If we think of |𝔄| itself (or any generating set G) as a set of variables (or “fresh constants”), then the identity map of sets Id : |𝔄| → |𝔄| (or the inclusion G ⊆ 𝔄) induces a unique Σ-morphism

T_{Σ}(|𝔄|) Îd 𝔄

(or T_{Σ}(G) ˆ⊆ 𝔄), which is easily seen surjective. Thus:

Theorem 1.3.8 Every Σ-algebra is the image of a free algebra on some set.

1.4 Lattices, Continuity and Fixed Points

Definition 1.4.1 A lattice L = ⟨S, ≤⟩ is a partially ordered set in which every pair of members has a least upper bound (lub, or ⋁) and a greatest lower bound (glb, or ⋀). A lattice is complete if any subset of L has a ⋁ and a ⋀. A subset X of L is directed if every finite subset of X has an upper bound in X. A function

f : L → L

is monotone if for every x, with x ≤ y we have f(x) ≤ f(y). It is continuous if for every directed subset X ⊆ L

f(⋁ X) = ⋁(f(X)).

Note that a complete lattice always has a least (⊥) and greatest element (⊤).

Theorem 1.4.2 (Tarski-Knaster) Let L be a complete lattice, ⊥ its least element. and f : T → T. If f is monotone it has a least fixpoint lfp(T) and a greatest fixpoint gfp(T). If f is continuous then

lfp(T) = ⋃_{n∈ω} T^{n}(⊥)

where T^{n+1}(X) means T (T^{n}(X)) and T^{0}(X) = X. proof: Exercise.

Observe that the powerset of any set X is a complete lattice with the order relation given by ⊆, ⋁ given by ∪, ⋀ by ∩, greatest element by X, and least element by ∅.

Now we apply these ideas to algebras. First observe that if 𝔄 is a Σ-algebra and E ⊂ 𝔄 then Sub(𝔄, E), the collection of subalgebras of 𝔄 containing E is a complete lattice, with minimal element 𝔄(E), maximal element 𝔄, glb given by intersection, and lub by closure of unions, i.e. by the subalgebra generated by the union. Also the set ℘(𝔄, E) of subsets of 𝔄 containing E ∪ 𝔄_{K} is a complete lattice with the containment order.

Lemma 1.4.3 Let 𝔄 be a Σ-algebra and E ⊂ 𝔄. Then the operator

S_{𝔄} : ℘(𝔄, E) → ℘(𝔄, E)

given by

S_{𝔄}(X) = X ∪ {f^{𝔄}(x_{1}, …, x_{m}) : x_{i} ∈ X ^{&} f ∈ Σ, m = arity of f}.

is continuous.

We then have the following consequence of the Tarski-Knaster theorem and of lemma 1.3.6:

Theorem 1.4.4 Let 𝔄 be a Σ-algebra and E ⊂ 𝔄. Then

𝔄(E) = lfp(S_{𝔄})

proof: Exercise.

We have come very close to showing that every closure of a generating subset (such as the set of terms or the subalgebra generated by some set) is an inductively defined set (e.g. the bottom-up description of lemma 1.3.6), and hence the least fixed point of some continuous operator.

The set of terms in T_{Σ}(X)is the closure of Σ_{K} ∪ X under a suitably defined set of functions corresponding to the symbols in Σ_{F}, from Σ^{∗}, the set (in fact, monoid) of strings over Σ, to itself.

Problem 4 Describe the class of functions with respect to which T_{Σ}(X)is the closure of Σ_{K} ∪ X in Σ^{∗}. Describe the continuous operator on ℘(Σ^{∗}, Σ_{K} ∪ X) whose least fixed point is T_{Σ}(X).

CHAPTER 1. PRELIMINARIES: INDUCTION, CLOSURE 10

Part II

Notes on Horn Clause Programs

and SLD Resolution

(Release 0.93)

(Notas para el curso de Doctorado sobre el λProlog, UPM, 1997)

Horn Clause Programs: The Classical Theory

2.1 Propositional Horn Programs

We begin with a study of Propositional Logic Horn clause programs. We will then “lift” the results obtained in this section to predicate logic via a powerful theorem due to Herbrand.

Definition 2.1.1 A (propositional) Horn Clause is a formula of the form

A_{1} ∧ A_{2} ∧ ⋯ ∧ A_{n} → B  (2.1)

where B and the A_{i} are atoms , i.e. propositional letters. The case n = 0 reads

→ B  (2.2)

which, by convention is logically equivalent to the proposition B and to the Horn clause

⊤ → B.  (2.3)

Such a clause is also called a fact, the typical clause (2.1) being called a rule.

Notation and Conventions We will also adopt the convention (lifted from resolution notation) that Horn clauses without consequents

A_{1} ∧ A_{2} ∧ ⋯ ∧ A_{n} →

are equivalent to

A_{1} ∧ A_{2} ∧ ⋯ ∧ A_{n} → ⊥

and hence to

¬(A_{1} ∧ A_{2} ∧ ⋯ ∧ A_{n})

and in particular the empty Horn clause “ → ” denotes the false proposition ⊥. We will often drop the conjunction symbols in Horn clause programs, writing

A_{1}, A_{2}, …, A_{n} → B

The sequence of atoms A_{1}, A_{2}, …, A_{n} is called the tail or antecedent of the clause, and B the head or consequent. When talking specifically about the Prolog programming language we’ll write these implications in reverse:

                                   B:- A1, A2,. . .,An.

Definition 2.1.2 A (propositional) Horn clause program P is a finite set of Horn clauses. A goal or query of a Horn clause program is either an atom Q or a conjunction of atoms. We say a Horn clause program satisfies its goal if the goal is a logical consequence of the program

P ⊧ Q.

The language of a program (or of a program together with its query) is the set of propositional letters occurring in it.

In the rest of this section we will be exploring a single specialized rule of inference known as SLD resolution used to establish that a goal is a logical consequence of a given program.

We will prove the rule sound and complete for the particular fragment of logic we are working with: premisses must be sets of Horn formulas, and theorems can only be atoms or conjunctions thereof.

We will often write a program P in the form

Γ_{1}, Σ → A, Γ_{2}  (2.4)

where the Horn clause Σ → A, is called the distinguished Horn clause in the expression (2.4), i.e. the one we wish to single out for discussion. In this expression, Σ denotes any tail, including the empty one, and Γ_{1} and Γ_{2} denote (possibly empty) sequences of Horn clauses (which may be either facts or rules). Similarly, a typical goal will be written Δ_{1}, Q, Δ_{2} where the Δ_{i} are (possibly empty) sequences of literals and Q, an atom, is the distinguished subgoal.

When discussing a Program together with its goal we will write

⟨Γ | Q_{1}, … Q_{n}⟩

or simply ⟨Γ | Δ⟩ where Δ is a sequence of atoms. Such an expression is called a configuration. There is a temptation to read this as a sequent, which should be avoided, since commas on the right hand side of a sequent are conjunctive, they denote “and”s. Relationships between this notation, SLD proofs and the sequent calculus of Gentzen will be discussed below.

2.1.1 SLD proofs

We will define an SLD-step as a rewriting of configurations, that is to say, a certain binary relation between configurations, and then use this to define a method of proof.

Definition 2.1.3 Let Γ_{1}, Σ → Q, Γ_{2} be a program and Δ_{1}, Q, Δ_{2} a goal. Then the following transition between configurations is called an SLD-step:

⟨Γ_{1}, Σ → Q, Γ_{2}|Δ_{1}, Q, Δ_{2}⟩ ⇒^{SLD} ⟨Γ_{1}, Σ → Q, Γ_{2}|Δ_{1}, Σ, Δ_{2}⟩  (2.5)

The binary relation ⟨P |G_{1}⟩ ⇒^{∗} ⟨P |G_{n}⟩ holds if there is a sequence of 0, 1, or more SLD steps

⟨P_{1}| G_{1}⟩ ⇒^{SLD} ⋯ ⇒^{SLD} ⟨P_{1}|G_{n}⟩

that is to say, ⇒^{∗} is the reflexive, transitive closure of ⇒^{SLD} . A finite sequence of SLD steps from ⟨P |G⟩ to a configuration of the form ⟨P | ⟩ is called an SLD-proof of the goal (or sequence of goals) G from the program or premisses P. If such a sequence exists we write

P ⊢_{SLD} G.

with the understanding that (unlike sequents) the commas in G denote conjunctions. We will sometimes write (G)^{∧} to mean the conjunction of the atoms in G, and then, more accurately, say

P ⊢_{SLD} (G)^{∧}.

Backchaining: A good description of the SLD step (2.5) is given by the statement: choose a subgoal, and replace it by the antecedent of some clause in the program whose head matches it. In this sense, SLD resolution looks somewhat like a sequence of backwards reduction steps that attack a problem by breaking it into subproblems and then continuing to do the same with these until trivially solvable problems are reached. As such it is a (bare bones) formalization of an approach to problem solving that is central in mathematics and computer science (and in many other domains). What we need to establish now is that it is not only a legitimate strategy within the world of computer science applications, but a correct and sufficiently powerful method of proof, i.e. that it is sound and complete with respect to the usual semantics for propositional logic.

Theorem 2.1.4 (Soundness)

Γ ⊢_{SLD} G ⇒ Γ ⊧ G

Proof: By induction on the length of the SLD deduction ⟨Γ|G⟩ ⇒^{∗} ⟨Γ| ⟩. If the proof is of length 1, then, G must be an atom and one SLD-step from ⟨Γ|G⟩ produces the empty goal. That is to say, there is an SLD-step

⟨Γ_{1}, Σ → G, Γ_{2}|G⟩ ⇒^{SLD} ⟨Γ_{1}, Σ → G, Γ_{2}|Σ⟩  (2.6)

with Σ empty. Thus, ⊤ → G (equivalently, the fact G) is a member of Γ and any valuation making Γ true makes G true, i.e. Γ ⊧ G. Now suppose the theorem holds for all SLD-derivable goals θ from Γ in ≤ n steps, and suppose there is an n + 1 step derivation of G from Γ. Then for some atom Q in G we have G = Δ_{1}, Q, Δ_{2} and, for some sequence of atoms Σ, the premiss must contain a Horn clause whose head is Q, that is to say, Γ = Γ_{1}, Σ → Q, Γ_{2} and the deduction is

⟨Γ_{1}, Σ → Q, Γ_{2}|Δ_{1}, Q, Δ_{2}⟩ ⇒^{SLD} ⟨Γ_{1}, Σ → Q, Γ_{2}|Δ_{1}, Σ, Δ_{2}⟩  (2.7)

followed by n more SLD-steps ending with ⟨Γ| ⟩. Thus, Γ_{1}, Σ → Q, Γ_{2} ⊢_{SLD} (Δ_{1}, Σ, Δ_{2})^{∧} in n steps, and by the induction hypothesis

Γ_{1}, Σ → Q, Γ_{2} ⊧ (Δ_{1}, Σ, Δ_{2})^{∧}.  (2.8)

But then if σ is a valuation making Γ true, since Γ = Γ_{1}, Σ → Q, Γ_{2}, we must have σ(Σ → Q) = ⊤ and by (2.8) σ(Δ_{1}, Σ, Δ_{2}) = ⊤ so, in particular, σ(Σ) = ⊤, so σ(Q) = ⊤. But then

σ((Δ_{1}, Q, Δ_{2})^{∧}) = ⊤

hence Γ ⊧ G which is what we wanted to show.

It may not be entirely surprising to learn that SLD-proof steps are sound. A moment’s thought shows they are essentially modus ponens (or more accurately, the left-arrow rule in the sequent calculus) carried out in reverse. The conclusion of the rule

\frac{Γ ⊢ (Σ)^{∧} Γ, A ⊢ A}{Γ, (Σ)^{∧} → A ⊢ A}

can be established provided the premiss Γ ⊢ (Σ)^{∧} can be established. Hence the name “backchaining” for SLD-steps. Once again we caution the reader to remember that a sequence of goals Σ in the expression

⟨Γ|Σ⟩

corresponds to a conjunction of goals in the sequent calculus, not to a sequence of formulas, since commas on the right of a ⊢ signify disjunctions.

2.1.2 Completeness

Now we establish a somewhat more surprising fact, namely the completeness of SLD-derivation for the Horn Clause fragment of propositional logic. We know by the standard completeness theorem for propositional logic that if a formula G is true in every valuation making a set P of premisses true then there is a proof of G from P. But if P is a finite set of Horn clauses, and G a conjunction of atoms, we can guarantee that an SLD proof exists.

First we need a few definitions and technical lemmas.

Let Γ be a Horn clause program over the language L and Q an atom. We now define an operation (Γ)^{Q} on the program that removes Q from the program altogether, giving us a new program over a smaller language L \ {Q}.

Definition 2.1.5 (Q-reduction)

(Γ_{0}, Σ → H, Γ_{1})^{Q} = Γ_{0}^{Q}, Σ^{Q} → H, Γ_{1}^{Q}  if H ≢ Q  (2.9)
(Γ_{0}, Σ → Q, Γ_{1})^{Q} = Γ_{0}^{Q}, Γ_{1}^{Q}  (2.10)

If Σ is empty or (equivalently) the symbol ⊤ then Σ^{Q} is the same as Σ. If Σ is an atom or a sequence of atoms:

(Δ_{0}, H, Δ_{1})^{Q} = Δ_{0}^{Q}, H, Δ_{1}^{Q}  if H ≢ Q  (2.11)
(Δ_{0}, Q, Δ_{1})^{Q} = Δ_{0}^{Q}, Δ_{1}^{Q}  (2.12)

We establish a few properties of this translation. We use the symbol Γ ⊧_{L} G to mean: for every valuation V defined on the propositional letters in L, if V makes every formula in Γ true then V makes G true.

Lemma 2.1.6 Let Γ be a Horn program and G a sequence of atoms.

Γ ⊧_{L} G ⇒ Γ^{Q} ⊧_{_{L}\Q} G^{Q}

proof: Suppose Γ ⊧_{L} G and V is a valuation defined over L \ Q making Γ^{Q} true. Then extend V to a valuation V̂ over L by assigning V̂ (Q) = ⊤. We claim that V̂ makes the original program Γ true. The clauses in Γ differ from those in Γ^{Q} in one of two ways: either

1. they are of the form Σ → Q and were removed altogether from Γ^{Q} or

2. they are of the form Δ_{0}, Q, Δ_{1} → H where the Q in the tail has been removed in Γ^{Q}.

Any implication with a true consequent is true, so V̂ makes clauses of the first kind true. The addition of a true antecedent Q to a true implication Δ_{0}, Δ_{1} → H preserves its truth (exercise!), so clauses of the second type are also validated by V̂. But then by the hypothesis Γ ⊧_{L} G the valuation V̂ makes G true. But then clearly V makes G^{Q} true, which is what we wanted to show.

An equally important property of Q reduction is that it preserves SLD-deduction when reversed i.e. when Q is restored.

Definition 2.1.7 Let P be a program, P = Γ, Γ_{0}, Σ → H, Γ_{1} and (for some atom Q) let P^{Q} = Γ_{0}^{Q}, Σ^{Q} → H, Γ_{1}^{Q}. In other words, Γ consists of the (possibly empty) sequence of clauses of the form Σ′ → Q which we removed under Q reduction, and Σ^{Q} → H is a distinguished Horn clause whose head H is not Q. Let

⟨Γ_{0}^{Q}, Σ^{Q} → H, Γ_{1}^{Q}|Δ_{0}^{Q}, H, Δ_{1}^{Q}⟩ ⇒^{SLD} ⟨Γ_{0}^{Q}, Σ^{Q} → H, Γ_{1}^{Q}|Δ_{0}^{Q}, Σ^{Q}, Δ_{1}^{Q}⟩

be an SLD-step of the Q-reduced program. Then

⟨Γ, Γ_{0}, Σ → H, Γ_{1}|Δ_{0}, H, Δ_{1}⟩ ⇒^{SLD} ⟨Γ, Γ_{0}, Σ → H, Γ_{1}|Δ_{0}, Σ, Δ_{1}⟩

is called the Q-lifting of the original SLD-step. Notice that it is itself a legitimate SLD-step.

Although programs and goals are sequences, they are sets up to logical equivalence that is to say, any switching (exchange) of atoms A, B to B, A in a sequence and any elimination of repetitions, leads to a logically equivalent program (although not necessarily to one which will behave in the same way !). So we will lose no generality in the following lemmas by assuming that any literal occurring in a sequence of subgoals occurs exactly once. However, the reader can simply interpret the Q in ⟨Γ|Q⟩ as standing for a sequence of Q’s if he or she prefers.

Lemma 2.1.8 The Q-lifting of each step of an SLD derivation

⟨Γ^{Q}|G^{Q}⟩ ⇒^{∗} ⟨Γ^{Q}| ⟩

results in an SLD derivation of

⟨Γ|G⟩ ⇒^{∗} ⟨Γ|Q⟩

or

⟨Γ|G⟩ ⇒^{∗} ⟨Γ| ⟩.

proof: exercise.

We’re now ready to prove completeness.

Theorem 2.1.9

Γ ⊧ G ⇒ Γ ⊢_{SLD} G

proof: We prove this theorem by induction on the number of atoms in the language L of Γ ∪ {G}. We first note that Γ must have a fact, i.e. a clause of the form → Q. For if not then one could contradict the hypothesis Γ ⊧ G by defining a valuation V to be false on at least one atom in every tail of every Horn clause of Γ and at least one atom in G. This would make every clause in Γ true, and G false.

We use this Q (occurring as a fact) to reduce the program. By lemma (2.1.6)

Γ^{Q} ⊧_{_{L}\Q} G^{Q}

But the Q reduction of Γ and G has one less atom in its language, so by induction hypothesis we have

Γ^{Q} ⊢_{SLD} G^{Q}

that is to say an SLD derivation

⟨Γ^{Q}|G^{Q}⟩ ⇒^{∗} ⟨Γ^{Q}| ⟩.

By lemma (2.1.8) we have a derivation

⟨Γ|G⟩ ⇒^{∗} ⟨Γ| ⟩

if Q does not occur in G, (in which case we are done), or if not, a derivation

⟨Γ|G⟩ ⇒^{∗} ⟨Γ|Q⟩  (2.13)

where Q may occur multiply in the final configuration. But we chose Q because it was the head of a fact → Q in Γ so one more SLD step (for each occurrence of Q) produces

⟨Γ|Q⟩ ⇒^{∗} ⟨Γ| ⟩.

Attaching this to the derivation (2.13) produces and SLD proof of G from the original program Γ as we wanted to show.

2.2 Herbrand’s Theorem

We now proceed to study the predicate logic case. We continue to develop the classical point of view and obtain a variant of the original completeness theorem due to Apt, Van Emden, Hill, Clark (see [4] for the full story).

2.2.1 A thumbnail review of completeness theorems for predicate logic

Recall that the completeness theorem for predicate logic states, for any set of (first-order) sentences Γ and any sentence A:

Γ ⊧ A  ⟺  Γ ⊢ A

where Γ ⊧ A means any model of Γ is a model of A. This has a number of classically equivalent statements.

Lemma 2.2.1 The following statements are equivalent.

1. For every set of sentences Γ and every sentence A, Γ ⊧ A ⇒ Γ ⊢ A.

2. Every consistent set of sentences Γ has a model.

proof: Exercise.

We now look at a completeness theorem for a restricted class of sentences.

2.2.2 Completeness for Π_{1}^{0}-sentences

A Π_{1}^{0}-sentence is one with only universal quantifiers when written in Prenex form:

(∀x_{1}) ⋯ (∀x_{n})φ(x_{1}, …, x_{n})

where φ(x_{1}, …, x_{n}) is quantifier-free.

Definition 2.2.2 Let L be a language and Σ the set of constants and function symbols in L. A term model or Herbrand model for L is a model H whose underlying set is the free Σ-algebra, i.e. the set of ground terms over L, with function symbols and constants in Σ interpreted “as themselves”, i.e., for every f of arity n and constant symbol c in Σ

f^{H}(t_{1}, …, t_{n}) := ft_{1} ⋯ t_{n}  and  c^{H} := c.

(Note that such models are not unique: Any of the infinitely many possible assignments of relations R^{H} on H to the relation symbols in L is allowed.)

Theorem 2.2.3 Every consistent set Γ of Π_{1}^{0}-sentences has a Herbrand model.

proof: We first use the completeness theorem for first order logic to assert the existence of a model 𝔄 for Γ. We use 𝔄 to define the Herbrand model. The domain and interpretation of functions and constants has been spelled out. All that is missing is the interpretation of the relation symbols. For each n-ary relation symbol R in L define

R^{H}(t_{1}, … t_{n})  ⟺  𝔄 ⊧ R(t_{1}, … t_{n}).

Let us call the resulting model H_{A} . We now show that every sentence γ in Γ is true in H_{A} . We first claim that every ground quantifier free formula θ is true in 𝔄 if and only if it is true in H_{A} . The proof (of the claim) is by induction on the structure of θ. Notice that the induction hypothesis is that the full statement of the claim (the “if and only if”) holds for all simpler formulas.

\underline{atoms}: If θ is atomic the claim holds by the definition of the model.

\underline{and}: Suppose θ is ψ ∧ χ. Then 𝔄 ⊧ θ if and only if 𝔄 ⊧ ψ and 𝔄 ⊧ χ. By induction hypothesis, this is equivalent to H_{A} ⊧ ψ and H_{A} ⊧ χ and therefore to H_{A} ⊧ ψ ∧ χ.

\underline{not}: 𝔄 ⊧ ¬θ if and only if 𝔄 |̸= θ. By induction hypothesis (𝔄 ⊧ θ if and only H_{A} ⊧ θ) this is equivalent to H_{A} |̸= θ, i.e. H_{A} ⊧ ¬θ. This establishes the claim.

Now we can prove that for any Π_{1}^{0}-sentence φ (in particular those in Γ)

𝔄 ⊧ φ  ⇒  H_{A} ⊧ φ.

For if φ is (∀x_{1}, ⋯, x_{n})α(x_{1}, ⋯, x_{n}) then 𝔄 ⊧ φ implies that for every d_{1}, …, d_{n} ∈ A 𝔄 ⊧ α(d_{1}, ⋯, d_{n}) so in particular, for every set of ground terms t_{1}, …, t_{n} over the language 𝔄 ⊧ α(t_{1}, ⋯, t_{n}). But then, by what we have just shown about ground quantifier free formulas, every such α(t_{1}, ⋯, t_{n}) holds in H_{A} . But then (∀x_{1}, ⋯, x_{n})α(x_{1}, ⋯, x_{n}) must also hold in H_{A} since all of the members of the underlying set A are terms.

Now we restrict our attention further to (predicate logic) Horn Clauses

(∀x_{1}, ⋯, x_{n})(A_{1}(t⃗_{1}) ∧ ⋯ A_{n}(t⃗_{n}) → B(v⃗))

where the t⃗_{i} are tuples of terms whose free variables are among x_{1}, ⋯, x_{n}.

Lemma 2.2.4 Let P be a finite set of Horn clauses and G = (∃x_{1}, ⋯, x_{n})Q_{1}(s⃗_{1}) ∧ ⋯ Q_{m}(s⃗_{m}) a closed query, that is to say the existential closure of a conjunction of atoms (henceforth abbreviated ∃xQ). Then

P ⊢ ∃xQ  ⟺  every term model of P is a model of ∃xQ.

Lemma 2.2.5 Every program P has at least one term model. In fact P has a least term model if we order term models by the extension of the interpreted relations:

H_{1} ⪯ H_{2} ≡^{def} for every relation symbol R R^{H_{1}} ⊆ R^{H_{2}}

We call this minimal model 𝔐_{P}, the least Herbrand model for P.

Lemma 2.2.6 Let P be a program and G = ∃xQ a query. Then

P ⊢ ∃xQ  ⟺  𝔐_{P} ⊧ Q.

Lemma 2.2.7 Let P and G be as in the preceding lemmas, i.e. G = (∃x)Q Suppose P ⊧ G. Then there is a a ground instance Qθ of Q and a finite sequence of ground substitutions θ_{1}, …, θ_{n} and a sequence of clauses (possibly with repetitions) C_{1}, …, C_{n} of P such that

C_{1}θ_{1}, …, C_{n}θ_{n} ⊧ Qθ.

proof: By the preceding lemmas P ⊧ G is equivalent to 𝔐_{P} ⊧ G. Since G is of the form ∃xQ this is equivalent to 𝔐_{P} ⊧ Q(d) for some tuple of terms d. But Q(d) holds in the least Herbrand model iff it holds in every term model, so P ⊧ G iff for some (tuple of) ground terms d, Q(d) holds in every term model of P. Let S be the set of all ground instances of the clauses in C. Then in any term model M, M ⊧ P iff every sentence in S holds in M. Thus, by the same arguments as in the preceding lemmas, any model of S is a model of Q(d), i.e.

S ⊧ Q(d).

By the compactness theorem, some finite subset of S logically implies Q(d). But this is what we wanted to show.

We are now ready to look at SLD-proofs in predicate logic.

2.3 Predicate Logic Programs

Definition 2.3.1 Let program mean a finite set of (predicate logic) Horn clauses written without quantifiers, and query a conjunction of atoms, written as a sequence of atoms. We will view a program as a notation for the corresponding set of sentences obtained by taking the universal closure of each Horn clause, and a query a notation for its existential closure. Thus, as all variables are tacitly bound, they may be renamed when convenient, so as to avoid clashes with the variables in other clauses. Such a renaming is called standardizing clauses apart.

As before, if P is a program and G a query, we call ⟨P |G⟩ a configuration. If A and A′ are both atomic formulas with the same relation symbol, we say they are variants of one another.

For the definition of substitution, unifier, mgu we refer the reader to [4] or [6].

We now adopt the following notation conventions. If C is a Horn clause, we will write e.g. C(d) to mean the Horn clause resulting from substituting d for the free variables of the matrix of C. Also, given two substitutions θ and φ we say θ ≤ φ if there is a substitution γ such that

θ = φγ

i.e. if γ is more general than θ.

Definition 2.3.2 Let Γ_{1}, Σ → Q, Γ_{2} be a program and Δ_{1}, Q′, Δ_{2} a goal, where Q′ is a variant of Q with no variables in common (i.e. whose variables have been standardized apart). Then the following transition between configurations is called an SLD-step with substitution θ:

⟨Γ_{1}, Σ → Q, Γ_{2}|Δ_{1}, Q′, Δ_{2}⟩ ⇒^{θ} ⟨Γ_{1}, Σ → Q, Γ_{2}|Δ_{1}θ, Σθ, Δ_{2}θ⟩  (2.14)

provided θ is a unifier of Q and Q′ i.e. Qθ = Q′θ. We will also use ⇒^{SLD} to denote this relation in the predicate case. The binary relation ⟨P_{1}|G_{1}⟩ ⇒^{∗} ⟨P_{n}|G_{n}⟩ holds if there is a sequence of 0, 1, or more SLD steps

⟨P_{1}| G_{1}⟩ ⇒^{θ_{1}} ⋯ ⇒^{θ_{n}} ⟨P_{1}|G_{n}⟩

that is to say, ⇒^{∗} is the reflexive, transitive closure of ⇒^{SLD} . A finite sequence of SLD steps from ⟨P |G⟩ to a configuration of the form ⟨P | ⟩ is called an SLD-proof of the goal (or sequence of goals) G from the program or premisses P. If such a sequence exists we write

P ⊢_{SLD} G.

If

⟨P_{1}| G_{1}⟩ ⇒^{θ_{1}} ⋯ ⇒^{θ_{n}} ⟨P_{1}|G_{n}⟩

is a sequence of SLD-steps with substitutions θ_{1}, …, θ_{n} we call this sequence the substitution sequence of the derivation. If the derivation is a proof, i.e. if G_{n} is the empty goal, we call the composition θ of θ_{1}, …, θ_{n} (with domain restricted to the free variables of G) the SLD answer substitution for the proof P ⊢_{SLD} G. If all the θ_{1}, …, θ_{n} are mgu’s then θ is called a computed answer substitution

Definition 2.3.3 A substitution θ is called a correct answer substitution for P, G if

P ⊧ ∀(Gθ)

where ∀(ψ) is the universal closure of ψ.

By adapting the argument for the propositional case we can easily establish:

Theorem 2.3.4 (Soundness of SLD proofs)

(a) Every SLD answer substitution is correct. In particular:

(b) P ⊢_{SLD} G ⇒ P ⊧ G.

We need a technical lemma to exploit Herbrand’s theorem to give us completeness for predicate SLD resolution as a “corollary” of the propositional case.

Lemma 2.3.5 (Lifting Lemma) Suppose P ⊢_{SLD} Gθ with substitution sequence θ_{1}, …, θ_{n}. Then there is an SLD derivation of the same length of P ⊢ G with a substitution sequence φ_{1}, …, φ_{n} made up exclusively of mgu’s satisfying

θθ_{1} ∘ ⋯ ∘ θ_{n} = φ_{1} ∘ ⋯ ∘ φ_{n}.

Corollary 2.3.6 If P, G has an SLD derivation with substitution sequence θ_{1}, …, θ_{n}, it has one of the same length with a substitution sequence φ_{1}, …, φ_{n} made up exclusively of most general unifiers. Furthermore

θ_{1} ∘ ⋯ ∘ θ_{n} ≤ φ_{1} ∘ ⋯ ∘ φ_{n}.

Now we have all the pieces in place to prove completeness of SLD proofs for the predicate Horn case.

Theorem 2.3.7 (Completeness of SLD proofs) Suppose P ⊧ G where P is a program and G a query. Then P ⊢_{SLD} G. In fact every correct answer substitution θ for P, G is an SLD answer substitution and is an instance of some computed answer substitution (obtained from a proof using only most general unifiers).

proof: By lemma (2.2.7) if P ⊧ G then there is a a ground instance Gθ of G and a finite sequence of ground substitutions θ_{1}, …, θ_{n} and a sequence S of clauses (possibly with repetitions) C_{1}, …, C_{n} of P such that

C_{1}θ_{1}, …, C_{n}θ_{n} ⊧ Gθ.  (2.15)

When premiss and conclusion are ground, the meaning of (2.15) is the same as its meaning in propositional logic, taking every ground atomic instance of a predicate as a different propositional letter. But then by the completeness theorem for propositional SLD resolution, there is an SLD proof

C_{1}θ_{1}, …, C_{n}θ_{n} ⊢_{SLD} Gθ.  (2.16)

Assume that the θ_{i} and C_{i} have been numbered in the order in which these clauses were used in the corresponding SLD derivation. That is to say

⟨S | G_{1}⟩ ⇒^{SLD} ⋯ ⟨S |G_{i}⟩ ⇒^{SLD} ⋯ ⟨S |G_{n}⟩

where G_{1} is Gθ, G_{n} is the empty goal, and G_{i+1} = Δ_{0i}, Σθ_{i}, Δ_{1i} was obtained from G_{i} = Δ_{0i}, A′, Δ_{1i} by replacing a ground atom A′ in G_{i} by the tail Σθ_{i} of the clause

C_{i}θ_{i} ≡ Σ_{i}θ_{i} → Aθ_{i}

where A′ and A are variants of the same predicate and Aθ_{i} = A′. Since every atom in Δ_{0i}, A′, Δ_{1i} is ground, the following is a predicate SLD step using the original program P:

⟨P |Δ_{0i}, A′, Δ_{0i}⟩ ⇒^{SLD} ⟨P |Δ_{0i}, Σθ_{i}, Δ_{1i}⟩

since the right hand side is identical to ⟨P |Δ_{0i}θ_{i}, Σθ_{i}, Δ_{1i}θ_{i}⟩. Using this analysis of each step of the original proof we can show by induction on the length of (2.16) that any proof in propositional logic of the form (2.16) can be similarly transformed to a predicate logic SLD proof of Gθ from P of the same length with substitution sequence θ_{1}, …, θ_{n}. By the lifting lemma (2.3.5) there is an SLD derivation of the same length of P ⊢ G with a substitution sequence φ_{1}, …, φ_{n} satisfying

θθ_{1} ∘ ⋯ ∘ θ_{n} ≤ φ_{1} ∘ ⋯ ∘ φ_{n}.  (2.17)

consisting only of mgu’s. Now suppose that θ is a correct answer substitution, and Gθ is ground. Then, using the same argument as above with this particular θ in (2.15) we obtain an SLD proof of G using φ_{1}, …, φ_{n} and satisfying (2.17). But since Gθ is ground, we may assume the domain of the θ_{i} is disjoint from the free variables of G. Hence if we restrict to these variables

θθ_{1} ∘ ⋯ ∘ θ_{n} = θ

and the conclusion (2.17) becomes θ ≤ φ_{1} ∘ ⋯ ∘ φ_{n}, i.e. the correct answer substitution is an instance of the mgu computed answer substitution, as we wanted to show.

2.4 Fixpoint Semantics

Definition 2.4.1 Let P be a program, L_{P} its language and H be its Herbrand universe. Define the Herbrand Base B_{P} to be the set of all ground instances of atomic formulas in the language L_{P}. We now define a function T_{P} from the power set ℘(B_{P}) of the Herbrand base to itself as follows. For each set X ∈ ℘(B_{P})

T_{P} (X) = X ∪ {A′ : Σ′ → A′is a ground instance of a clause in P ^{&} Σ′ ∈ X}

We will now look at operators on the Herbrand base induced by a program.

Now we observe that the powerset of any set is a complete lattice (see section 1.4) with the order relation given by ⊆, lub given by ∪ and least element ϕ. It is an easy exercise to show that for any program P the operator T_{P} defined above is continuous. We can now give a simple characterization of the least Herbrand model based on the Tarski-Knaster theorem covered in the section on lattices 1.4.

Theorem 2.4.2 lfp(T_{P}) is the least Herbrand model 𝔐_{P} of P.

This allows us to give a simple alternative proof of the completeness theorem for SLD proofs. For if

P ⊧ Gθ

where Gθ = A_{1} ∧ ⋯ ∧ A_{n} is ground, then by lemma (2.2.6) 𝔐_{P} ⊧ A_{i} for each i. By (2.4.2) each A_{i} is a member of lfp(T_{P}) = ⋃_{n}(T^{n}(ϕ)). Thus for some m ∈ ω every A_{i} is in T^{m}(ϕ).

Lemma 2.4.3 Let A be a ground atom. Then

A ∈ T^{m}(ϕ) ⇒ P ⊢_{SLD} A

proof: By induction on m. The base case m = 0 is vacuous. Suppose the theorem holds for m and A ∈ T^{m+1}(ϕ). If A ∈ T^{m}(ϕ) we are done. If not then there must b a clause Σ → H and a ground substitution θ such that for every literal B in Σφ, B ∈ T^{m}(ϕ) and Hφ = A. Let Σφ = B_{1}φ, …, B_{r}φ. By induction hypothesis, for each B_{i}φ

P ⊢_{SLD} B_{i}φ

i.e. ⟨P | B_{i}φ⟩ ⇒^{∗} ⟨P | ⟩. We leave it to the reader to show that these proofs can be glued to obtain a legal SLD-sequence ⟨P | B_{1}φ, …, B_{r}φ⟩ ⇒^{∗} ⟨P | ⟩. But then, one more SLD-step yields

⟨P | Hφ⟩ ⇒^{SLD} ⟨P | B_{1}φ, …, B_{r}φ⟩ ⇒^{∗} ⟨P | ⟩.

By gluing together the proofs for each A_{i} in the same way we did in the proof of the lemma we obtain P ⊢_{SLD} Gθ. We can then use the lifting lemma (2.3.5) in the same way as before to show that if P ⊢_{SLD} G for any (not necessarily ground) G then there is an SLD derivation of ∀(G) and the substitutions may be assumed mgu’s.

Uniform Proofs

What has been achieved so far? We have isolated a fragment of first order logic, the Horn clause fragment, which enjoys certain important properties. Queries which are logical consequences of such programs are derivable in an efficient manner using a certain proof strategy. Since each step of the derivation is a valid one (soundness) our answers must be correct. Since the code itself is a piece of logic, the program is a logical specification of the relation we are trying to compute. This matter deserves some comment.

Writing a correct program is always a question of producing executable code that lives up to some description of the desired program behavior. This is certainly one of the most important problems on the software side of computer science. The passage from specifications to code is fraught with problems. There are a number of ways that language designers have responded to the challenge. We can look upon logic programming as an attempt to chart this passage by going to an extreme: identifying a specification language that is already a programming language. In fact, ideally, (if we ignore departures from the theory which violate soundness, and if we push aside considerations of computational complexity) logic programs are executable specifications.

Unfortunately these departures and considerations are too important to ignore. If we program without using any algorithmic ideas, such as stack variables and tail recursion, or try to ignore the details of the execution, our programs are hopelessly inefficient. But many present day programming solutions to this force us away from the declarative approach to programming. How then do we increase expressive power and efficiency, how do we allow the programmer to input good programming ideas into declarative code, while maintaining this wonderful correspondence between logical content of code and its behavior?

This question has no definitive answer and it probably never will. But there has been considerable progress over the past twenty years since prolog was first introduced. Constraints, metaprogramming, typing, and many other features have been introduced into the field. But perhaps the most significant theoretical gain has been to identify what components in the abstract, a language should have, to qualify as a logic programming language. This advance, due to Miller, Nadathur, Scedrov, Pfenning, Felty and others, has led to a whole family of programming languages and a very promising integration of typetheoretic and functional programming features into the field of logic programming. This we explore in the next section.

3.1 Cut elimination and Uniform Proofs

We now explore an alternative approach to completeness of logic programming derivations based on results of Gentzen in the 1930’s that has a number of advantages. It gives a unified and constructive theoretical framework for studying and generalizing many of the features of the preceding sections. In particular it permits a broad definition of logic programming language as a set of sentences and proof rules in some fragment of logic enjoying certain abstract properties. Armed with this definition we are able to identify three nontrivial extensions of Horn clause logic that provide a net increase in expressiveness of programs without sacrificing declarative content.

In order to speak in a general way about logic programs we adopt some notational conventions. To specify a logic programming language we start with the set T of terms and F of formulas. We then identify two subsets of F , the set D of program clauses and the set G of possible goals or queries. We reserve the notation A for atomic formulas (not including ⊥ or ⊤), D for a member of D and G for a member of G . A finite subset P of G is referred to as a logic program.

We will usually define G and D by simultaneous induction. We illustrate by giving a formal definition of Horn clauses and Prolog queries in this notation.

G := ⊤ | A | G_{1} ∧ G_{2} | G_{1} ∨ G_{2} | ∃xG  (3.1)
D := A | G → A | D_{1} ∧ D_{2} | ∀xD  (3.2)

It is easy to show that every formula in D is logically equivalent to a Horn Clause program (disjunctions in tails are removable, and free variables occurring in a tail but not in the head of a clause may be existentially quantified in the tail).

In fact the above definition is closer to programming practice, in which e.g. explicit disjunctions (;) are allowed in the tail of a clause.

We now define a proof system based on a variant of Gentzen’s sequent calculus. A sequent is an expression of the form Γ ≫ Θ where Γ, Θ are finite sets of formulas. Thus repetitions can never occur, and no explicit rules for contraction

\frac{Γ ≫ Θ, A, A}{Γ ≫ Θ, A}  \frac{Γ, A, A ≫ Θ}{Γ, A ≫ Θ}

or exchange

\frac{Γ ≫ Θ_{1}, A, B, Θ_{2}}{Γ ≫ Θ_{1}, B, A, Θ_{2}}  \frac{Γ_{1}, A, B, Γ_{2} ≫ Θ}{Γ_{1}, B, A, Γ_{2}, A ≫ Θ}

are needed. Γ is called the antecedent and Θ the consequent or succedent of the sequent Γ ≫ Θ.

Definition 3.1.1 A sequent Γ ≫ Θ is said to be initial if either ⊤ ∈ Θ or Γ ∩ Θ contains ⊥ or some atomic formula A. A proof is either an initial sequent or a tree with initial sequents at its leaves, built from smaller proofs by the use of the rules of inference in the following table.

\frac{B, C, Γ ≫ Θ}{B ∧ C, Γ ≫ Θ} ∧-L  \frac{Γ ≫ Δ, B  Γ ≫ Δ, C}{Γ ≫ Δ, B ∧ C} ∧-R

\frac{Γ, B ≫ Δ  Γ, C ≫ Δ}{Γ, B ∨ C ≫ Δ} ∨-L  \frac{Γ ≫ Θ, B}{Γ ≫ Θ, B ∨ C} ∨-R \frac{Γ ≫ Θ, C}{Γ ≫ Θ, B ∨ C} ∨-R

\frac{Γ ≫ Θ, B  Γ, C ≫ Δ}{Γ, B → C ≫ Δ ∪ Θ} →-L  \frac{Γ, B ≫ C, Θ}{Γ ≫ B → C, Θ} →-R

\frac{Γ, P [t/x] ≫ Θ}{Γ, ∀xP ≫ Θ} ∀-L  \frac{Γ ≫ Θ, P [c/x]}{Γ ≫ Θ, ∀xP} ∀-R∗

\frac{Γ, P [c/x] ≫ Θ}{Γ, ∃xP ≫ Θ} ∃-L∗  \frac{Γ ≫ Θ, P [t/x]}{Γ ≫ Θ, ∃xP} ∃-R

Rules marked with ∗ have the usual side condition: c must not occur in the conclusion of the rule.

\frac{Γ ≫ Θ, ⊥}{Γ ≫ Θ, B} ⊥-R  \frac{Γ ≫ B, Δ  Γ, B ≫ Θ}{Γ ≫ Δ ∪ Θ} CUT

Exercise: Show that the definition of initial sequent makes the rule of weakening unnecessary. That is to say, show that the rule

\frac{Γ ≫ Θ}{Γ ∪ Δ ≫ Θ}

is derivable in our system.

We now define three kinds of proofs using the above rules:

Definition 3.1.2 If the sequent B ≫ C is the final sequent in a proof, we say it is derivable and write B ⊢ C. We distinguish three kinds of proofs using the rules given above:

1. A C-proof is any proof using the rules. We indicate that Γ ≫ G is derivable using a C-proof by writing Γ ⊢_{C}G.

2. An I-proof is a C-proof in which only singleton sets are allowed as consequents in any sequent occurrence. We write e.g. Γ ⊢_{I}G.

3. An M-proof is an I-proof in which no instance of the ⊥ − R rule occurs.

The terms C,I,M refer to classical, intuitionistic and minimal logic respectively.

Our main purpose in this chapter is to show that for suitably restricted sets of antecedents and succedents I-proofs may be replaced by highly constrained derivations such as SLD-proofs, the search for which are easily automated. Furthermore they permit a straightforward representation of recursively defined functions in a declarative manner. Just what such “special” proofs should look like is what this section is all about. Before we begin to make this precise we state two powerful theorems due to Gentzen which are the first and most important steps towards identifying constrained searches for proofs that will not sacrifice completeness.

Theorem 3.1.3 (Cut Elimination, Gentzen 1931) A sequent Γ ≫ B has a C-proof,I-proof or Mproof iff it has one which is cut-free, i.e. which does not make use of the CUT rule.

proof: See e.g. [3, 2, 7]

An immediate consequence is

Corollary 3.1.4 (Gentzen) If Γ ≫ Θ has a C-proof, I-proof or M-proof iff it has one in which every formula occurring in the proof is a subformula of some member of Γ ∪ Θ.

Convention: We will now drop the CUT rule from the proof system of def (3.1.1). Henceforth, when we say proof or I-proof, etc., we mean cut-free.

We are now ready to define the special kind of proof that we are looking for in a logic programming language.

Definition 3.1.5 A uniform proof is an I-proof in which for each occurrence of a sequent Γ ≫ G, either G is atomic or the sequent is a conclusion of a right rule. In more detail:

A uniform proof is an I-proof such that for each formula occurrence of a sequent Γ ≫ G, the following holds:

1. If G is ⊤ the sequent is initial.

2. If G is B ∧ C then the sequent is the conclusion of a ∧ − R rule.

3. If G is B ∨ C then the sequent is the conclusion of a ∨ − R rule.

4. If G is ∃xP then the sequent is the conclusion of a rule of the form

\frac{Γ ≫ Θ, P [t/x]}{Γ ≫ Θ, ∃xP} ∃-R

for some term t.

5. If G is B → C then the sequent is the conclusion of an → −R rule.

6. If G is ∀xP then the sequent is the conclusion of a rule of the form

\frac{Γ ≫ Θ, P [c/x]}{Γ ≫ Θ, ∀xP} ∀-R

for some constant c not occurring in the sequent.

If Γ ≫ G has a uniform proof we write Γ ⊢_{O}G.

The notation Γ ⊢_{O}G, due to Miller et al. [5] is intended to suggest that uniformity of proofs gives us an operational interpretation of the logical conectives. For example, to find a uniform proof of sequent Γ ≫ A ∨ B we search for Γ ≫ A or Γ ≫ B. In uniform proofs, logical connectives can be viewed as different kinds of search-directives, and proof search becomes a form of programming. But these definitions are of no use to us unless we know that by restricting attention to uniform proofs we will not sacrifice completeness. We want to be sure some choice of search pattern will actually lead to success if the sequent made up by the program and query is provable. In general this is not possible, however. For example, in full first order logic there are sequents which are provable, but not via a uniform proof. Consider the sequent

{¬(¬p ∧ ¬q)} ≫ p ∨ q.

It has a classical proof, but has no uniform proof: neither p nor q follow from the antecedent. Another example is

¬p(a) ∨ ¬p(b) ⊢_{C}∃x¬p(x).

We are therefore interested in isolating fragments (of first, higher order, and other logics) in which restriction to uniform proofs will not sacrifice completeness, as in the Horn clause case.

Definition 3.1.6 An abstract logic programming language is a triple ⟨D , G , ⊢⟩ such that for all finite subsets P of D and all formulas G of G

P ⊢ G  ⟺  P ⊢_{O}G.

Our first example is provided by Horn clause programs in the form given in (3.1). Let fohc= ⟨D , G , ⊢_{C}⟩.

Theorem 3.1.7 fohc is an abstract logic programming language.

The reader of these notes has already seen two proofs. But we supply a third, by far the most perspicuous, drawing as it does on cut elimination and on other ideas that work with all the logic programming languages!

We begin with a number of lemmas:

Lemma 3.1.8 Let Γ ⊂ D and Θ ⊂ G be finite sets of formulas.

1. Suppose Γ ⊢_{C}Θ. Then every sequent Δ ≫ Φ occurring in a (cut free) proof of Γ ≫ Θ satisfies Δ ⊂ D and Φ ⊂ G ∪ {⊥}.

2. There is no C-proof of Γ ≫ ⊥.

3. If there is a C-proof of Γ ≫ Θ then a proof exists in which the ⊥ − R rule does not occur. proof: The first assertion of the lemma is that at any intermediate stage in the proof of Γ ≫ Θ antecedents and consequents are (almost) in the same syntactic classes D,G as the final program and query. To show this we need to prove a slightly stronger claim, namely that if Θ ⊂ G ∪ ⊥ then every sequent Δ ≫ Φ occurring in a (cut free) proof of Γ ≫ Θ satisfies Δ ⊂ D and Φ ⊂ G ∪ {⊥}.

The proof is by induction on the length of the given C-proof. Suppose the proof is atomic. Then Γ ≫ Θ is initial and there are no other sequents in the proof. For the inductive case, assume the result holds for all shorter proofs. By Gentzen’s theorem, inspection of our proof system shows that if a right ∀ or → rule occurs in the proof, then these connectives must show up in the final sequent on the right, contradicting the fact that Θ is contained in G ∪ ⊥. Thus, ∧-R, ∨-R, ∃-R, ⊥-R are the only right rules that could occur in the proof. Similarly, the only left rules that could occur aree ∧-L, →-L and ∀-L. Suppose the last rule used in a C-proof of Γ ≫ Θ is

\frac{Γ ≫ C_{1}, Θ  Γ ≫ C_{2}, Θ}{Γ ≫ C_{1} ∧ C_{2}, Θ}  (3.3)

By assumption C_{1} ∧ C_{2} ∈ G . But then both of C_{1}, C_{2} are in G . Thus both sequents in the premiss of 3.3 satisfy the hypothesis of the claim, so, by inductive hypothesis, the sequents Δ ≫ Φ appearing in the proofs of Γ ≫ C_{1}, Θ and Γ ≫ C_{2}, Θ satisfy Δ ⊂ D and Φ ⊂ G ∪ {⊥}, so the proof 3.3 as a whole has this property as well.

Suppose the last rule used in a C-proof of Γ ≫ Θ is

\frac{Γ, P [t/x] ≫ Θ}{Γ, ∀xP ≫ Θ} ∀-L  (3.4)

Then ∀xP is in D, hence so is P. The reader can show D is closed under substitution (all atoms are in D), so Γ, P [t/x] ⊂ D. Thus the premiss of 3.4 also satisfies the hypothesis of the claim, and by induction hypothesis, has a proof containing only the required sequents.

In the →-L case,

\frac{Γ ≫ Θ, B  Γ, C ≫ Δ}{Γ, B → C ≫ Δ ∪ Θ} →-L  (3.5)

if the consequent satisfies the requirements, and , B → C ⊂ D, then B ∈ G and C ∈ D, so once again the premisses of the last rule both satisfy the hypothesis of the claim.

In the ⊥-R case,

\frac{Γ ≫ Θ, ⊥}{Γ ≫ Θ, B} ⊥-R  (3.6)

if the consequent of the conclusion is a subset of G ∪ {⊥} then so is the consequent of the premiss Θ, ⊥. So the induction hypothesis applies to the subproof of 3.6 ending with Γ ≫ Θ, ⊥.

The remaining cases of the induction are left as an exercise.

Now we give a syntactic proof of the second claim, namely that programs are always consistent. Let S be the set of all C-proofs of Γ ≫ ⊥ and suppose π is a proof in S of minimal height. Then π cannot be a one-line proof, with its sole sequent initial, since this would require ⊥ ∈ Γ which contradicts Γ ⊂ D. The last rule used in π must be one of →-L, ∀-L or ∧-L, since the other rules would have introduced other formulas on the right or taken the antecedent out of D. But this is impossible since (as the reader can check) in all these cases, some premise would be of the form Γ′ ≫ ⊥ with Γ′ ⊂ D (by part 1 of the lemma) but with a shorter proof, contradicting minimality of π.

Now we prove the third claim of the lemma. Since, by claim 2, no sequent in the proof can be of the form Δ ≫ ⊥, if ⊥-R occurs in the proof, the premise of the rule must have some other formula in its consequent, i.e., it must be of the form

\frac{Δ ≫ Ψ, ⊥}{Δ ≫ Ψ, C}  (3.7)

for some nonempty set of formulas Ψ. We now show the same conclusion (Δ ⊢_{C}Ψ, C) can be reached without the use of this rule. That is to say, we show that any proof of a sequent 3.7 with antecedent in D and consequent in G whose last rule is ⊥-R can be replaced by a ⊥-R free proof of the same sequent. We argue by induction on the height of the given proof.

Base case: If the proof is of minimal height 2, then the premiss Δ ≫ Ψ, ⊥ is initial. But ⊥ cannot occur in Δ ⊂ D so Δ and Ψ have some atom in common. Thus Δ ≫ Ψ is initial, and so Δ ≫ Ψ, C is also initial.

Induction case: Suppose the claim true for all shorter proofs and that (3.7) is the last rule used. Since Δ ⊂ D and Ψ ⊂ G the only rules that could have led to Δ ≫ Ψ, ⊥ as a conclusion are the left →, ∀ and ∧ rules, or the right ∨, ∧, ∃ rules. But in each of these cases the ⊥ must appear in some premiss. For example, suppose the rule applied immediately before (3.7) was ∀-L.

\frac{Δ′, B[c/x] ≫ Ψ, ⊥}{\frac{Δ′, ∀xB ≫ Ψ, ⊥}{Δ′, ∀xB ≫ Ψ, C}}

But then we could have reached this conclusion by applying ⊥-R first, followed by ∀-L:

\frac{Δ′, B[c/x] ≫ Ψ, ⊥}{\frac{Δ′, B[c/x] ≫ Ψ, C}{Δ′, ∀xB ≫ Ψ, C}}

Now apply the induction hypothesis to the subproof ending with Δ′, B[c/x] ≫ Ψ, C to obtain a proof π of this sequent without any occurrences of the ⊥-R rule. Then

\frac{⋮ π}{Δ′, ∀xB ≫ Ψ, C}

is a proof of the original sequent without ⊥-R. Notice that what we have just done is to establish that ⊥-R is permutable with ∀-L. We need only check that this permutability also holds with →, ∧-L and ∨, ∧, ∃-R rules. The argument for the remaining cases is left to the reader.

Lemma 3.1.9 Suppose Γ ⊂ D, Θ ⊂ G and Γ ⊢_{C}Θ. Then there is a formula G′ ∈ Θ such that Γ ≫ G′ has an M-proof.

proof: We can assume that ⊥-R does not occur anywhere in the proof and that for every sequent Δ ≫ Φ in the proof Δ ⊂ D and Φ ⊂ G .

Now we establish the lemma by induction on the height of the deduction Γ ⊢_{C}Θ. Suppose the height is 1, i.e., Γ ≫ Θ is initial. Then Γ ⊢_{M}G for some G ∈ Γ by definition of initial proof, and by the fact that initial sequents constitute M-proofs.

Suppose the result holds for all deductions of smaller height and consider the last rule used in the proof of Γ ≫ Θ. Since Θ ⊂ G the only right rules that could have occurred were →, ∃, ∧, ∨ and, similarly the only left rules →, ∧, ∀. We consider several, and leave the remaining clauses to the reader. Suppose the last rule was ∨-R and that for some Δ, B, C we have Θ = Δ ∪ {B ∧ C} and:

\frac{Γ ≫ Δ, B Γ ≫ Δ, C}{Γ ≫ Δ, B ∧ C}

By induction hypothesis on the shorter proofs of the sequents above the line, either there is a D ∈ Δ and an M-proof of Γ ≫ D or there is an M-proof of both Γ ≫ B and Γ ≫ C. But then one step of ∧-R gives us an M-proof of B ∧ C from Γ. Thus in all cases we have the conclusion of the theorem.

Corollary 3.1.10 If Γ ⊂ D and G ∈ G then

Γ ⊢_{C}G ⇒ Γ ⊢_{M}G.

Theorem 3.1.11 Suppose (Δ, G) is in fohc. If Δ ≫ G is derivable it has a uniform proof.

proof: By induction on the degree: the pair (| G |, ∂) where ∂ is the depth of the proof tree, and | G | is the depth of the goal formula. Pairs are ordered lexicographically. The induction hypothesis for a proof of an fohc endsequent of degree d will be that if any fohc endsequent of degree less than d has a proof, it has a uniform proof.

If ∂ is 0, then the proof is already uniform. If G is atomic and the depth is greater than 0, then the last step in the proof of Δ ≫ G is uniform. Its immediate subproof (the one whose endsequent is the premiss of the last rule) has the same goal and smaller depth, hence degree. By the induction hypothesis this subproof may be replaced by a uniform proof tree with the same endsequent. But then the resulting proof of (| G |, ∂) is uniform.

Now suppose the goal G of the endsequent is nonatomic. If the last rule is a right rule, one can back up one step to the immediate subproof or subproofs of that rule. These subproofs have lower degree, so by induction hypothesis, can be replaced by uniform proofs. But then the resulting proof of the original goal is now uniform, since it has uniform subproofs and has a uniform last rule.

This leaves us with the cases where the goal G is nonatomic, but the last rule used in the proof of Δ ≫ G is a left rule.

Since the proof of Δ ≫ G is cut-free, and only certain connectives may occur in fohc programs and goals, the left rule invoked at the last step must be one of {→_{L}, ∀_{L}, wedge_{L}}, and the goal must have principal connective among {∨, wedge, →, ∃}. This leaves us with twelve cases to consider. We will look at the →_{L} cases and leave the rest to the reader.

\underline{(→_{L}, ∧)}: Suppose G is of the form G_{1} ∧ G_{2} and the last step in the proof is →_{L}.

\frac{Δ ≫ A Δ, B ≫ G_{1} ∧ G_{2}}{Δ, A → B ≫ G_{1} ∧ G_{2}}

The right-hand subproof has the same goal and smaller depth, hence smaller degree. By induction hypothesis it may be replaced by a uniform proof. In such a proof the last step would be ∧ − intro.

\frac{Δ ≫ A \frac{Δ, B ≫ G_{1} Δ, B ≫ G_{2}}{Δ, B ≫ G_{1} ∧ G_{2}}}{Δ, A → B ≫ G_{1} ∧ G_{2}}

But now we may first apply the →_{L} rule to the subproofs of Δ ≫ A and Δ, B ≫ G_{i} followed by ∧_{R}:

\frac{\frac{Δ ≫ A  Δ, B ≫ G_{1}}{Δ, A → B ≫ G_{1}}  \frac{Δ ≫ A  Δ, B ≫ G_{2}}{Δ, A → B ≫ G_{2}}}{Δ, A → B ≫ G_{1} ∧ G_{2}}

The two immediate subproofs of Δ, A → B ≫ G_{1} ∧ G_{2} are of smaller degree and may also be replaced by uniform proofs, rendering the entire proof uniform.

For the remaining cases we use the same sort of argument. We illustrate the relevant transformations.

(→ −L, ∨ − R)
\frac{Δ ≫ A  \frac{Δ, B ≫ G_{1}}{Δ, B ≫ G_{1} ∨ G_{2}}}{Δ, A → B ≫ G_{1} ∨ G_{2}} ↦ \frac{Δ ≫ A  Δ, B ≫ G_{1}}{\frac{Δ, A → B ≫ G_{1}}{Δ, A → B ≫ G_{1} ∨ G_{2}}}

(∀ − L, ∃ − R)^{\frac{Δ, B[ξ/x] ≫ G[t/x]}{\frac{Δ, B[ξ/x] ≫ ∃xG}{Δ, ∀xB ≫ ∃xG}}  ↦  \frac{Δ, B[ξ/x] ≫ G[t/x]}{\frac{Δ, ∀xB ≫ G[t/x]}{Δ, ∀xB ≫ ∃xG}}}

Bibliography

[1] Doets, Kees, [1994] From Logic to Logic Programming, MIT.

[2] Girard, J.-Y.,[1989] Proof Theory and Complexity, Bibliopolis.

[3] Girard, J-Y, Lafont, Y, Taylor[1990]Proofs and Types, Cambridge University Press.

[4] Lloyd, [1989]The Foundations of Logic Programming,2nd ed., Springer.

[5] Miller, D., Nadathur, G., Pfenning, F., Scedrov, A. [1991], “Uniform Proofs as a Foundation for Logic Programming”, Annals of Pure and Applied Logic, vol. 51, North-Holland.

[6] Shore, R. and Nerode, A.[1994] Logic and Applications, Springer.

[7] Takeuti, G. Proof Theory, North-Holland.