A Full Formalization of SLD-Resolution in the Calculus of Inductive Constructions.
This paper presents a full formalization of the semantics of definite programs, in the calculus of inductive constructions. First, we describe a formalization of the proof of first-order terms unification: this proof is obtained from a similar proof dealing with quasi-terms, thus showing how to relate an inductive set with a subset defined by a predicate. Then, SLD-resolution is explicitely defined: the renaming process used in SLD-derivations is made explicit, thus introducing complications, usually overlooked, during the proofs of classical results. Last, switching and lifting lemmas and soundness and completeness theorems are formalized. For this, we present two lemmas, usually omitted, which are needed. This development also contains a formalization of basic results on operators and their fixpoints in a general setting. All the proofs of the results, presented here, have been checked with the proof assistant Coq.
Introduction
This paper is concerned with programming languages semantics. Its aim is
to formalize SLD-resolution in the calculus of inductive constructions (Coq).
First, terms and substitutions are dened, and the unication theorem, constantly
used in the denition of the semantics of denite programs, is proved
from a similar theorem for quasi-terms [26]. Then, we present the formal
denitions of syntactic objects used in logic programming (atoms, queries,
clauses, etc) and we introduce their interpretation schemes. Last, declarative
and operational semantics of denite programs are introduced, and the
proofs of fundamental results of the theory of logic programming are formalized
(lifting and switching lemmas, soundness and completeness theorems).
The reader is assumed to be familiar with the terminology and the basic
results on the semantics of logic programs, as introduced in [2, 19].
Of course, there exists an extensive literature on logic programming [3,
2, 17, 19, 28] where all these theorems are proved, and one can wonder
about the usefulness of such a formalization. For this, recall that formalizing
a proof rst consists in giving formal denitions of the objects used,
then explicitely stating a priori the hypotheses needed, and last inferring the
conclusion. Therefore, since our proofs have been encoded using the Coq
proof assistant, all objects and properties are explicitely dened as well as
all hypotheses needed for these proofs. Each step of a proof also explicitely
results from denitions or applications of induction schemes, lemmas, or the-
orems. This makes a dierence from the initial proofs, which can be found
in many books on logic programming. Hence, formalizing proofs brings us
at a level of detail that is often left to the reader, and we will see that if we
take into account some details, often considered as minor in more informal
presentations, proofs are getting a bit complicated. Furthermore, we will
see that some assumptions, usually overlooked, are required in some of the
theorems proved. The main diculty of this development is concerned with
the denition of the variable renaming process used in an SLD-derivation,
which is made explicit, thus introducing some complications, usually omit-
ted. For instance, we will see that the proof of the completeness theorem
is more delicate than it seems and requires, from a formal point of view,
several technical lemmas. Few papers are devoted to these details; however,
in [27], J. C. Shepherdson points out inaccuracy in some of the basic results
in the theory of logic programming and presents a discussion about the role
of standardizing apart in SLD-resolution. Let us give the most famous ex-
ample, coming from this paper, and showing how a classical result can be
incorrectly stated: in a famous book [19], J. W. Lloyd gives the fundamental
theorem of completeness of SLD-resolution in the following form:
Let P be a denite program and G a
denite goal. For every correct answer  for P [fGg, there exists
a computed answer  for P [ fGg and a substitution
such that
.
In 1994, J. C. Shepherdson wrote about this theorem: This is not true [27]
and gave a very simple counterexample. Of course, it is true that we can nd
two substitutions  and
such that
G; however, although  and
act only on the variables occurring in G, this does not imply that
can
be restricted to yield
. Another typical example is the lifting lemma
generally stated as follows:
be a program, N a goal and  a substitu-
tion. Suppose that there exists an SLD-refutation of P [ fNg
with the sequence of mgu's  . Then, there exists an SLD-
refutation of P [ fNg with the sequence of mgu's  0
n such
that  0
0 is more general than
No assumptions on the substitution  are supposed here. However, in order
to formalize the corresponding proof, which builds the derivation starting
from N , we have to assume some hypotheses. Let x be a variable occurring
in the domain of  and in N that does not occur in N . Whereas x can be
used in the renamed clauses during the derivation starting from N , it cannot
be used during the derivation starting from N . Hence, in order to exactly use
the same sequences of variant clauses (which is always suggested) in the two
derivations, we have to suppose that no variable used for the renaming of the
input clauses in the derivation starting from N occurs in N . Furthermore,
for similar reasons, in order to prove  0
we have to suppose
that no variable used for the renaming of the input clauses in the derivation
starting from N occurs in the domain of . A similar problem happens
during the proof of the switching lemma asserting that if during an SLD-
derivation, two atoms L 1 and L 2 are successively selected, then they can also
be selected in the reverse order and the derived states are the same up to
renaming of variables.
| {z }
| {z }
Here again, if we want to exactly use the same variants of C 1 and C 2 in
the two derivations, some assumptions are required. By hypotheses (coming
from the initial derivation), we have
However, if we
want to select L 2 before L 1 with C 2 , C 2 must satisfy
But nothing in the switching lemma ensures such a property, and, depending
on the standardization apart used for SLD-derivations, it is possible that a
variable occurring in R 0 but not occurring in R 1 , occurs in C 2 . To avoid
this problem, C 1 and C 2 must satisfy
holds if we use the standardizing apart coming from [2]). Hence, formalizing
a proof brings us to a greatest level of detail. Most of problems are due to
variables occurring in the input clauses (variants of clauses used in the resolution
steps) coinciding with other variables in the derivation. Surprisingly,
another problem comes from the necessity of an explicitation a priori of all
the assumptions needed to obtain a proof. Curiously, even if this requirement
seems natural, it is a common practice in logic programming, to suppose,
during the proofs (on paper) of most of basic results, some assumptions
on the variables occurring in the clauses used, without any justication. Of
course, there exists an independence result asserting that the existence of a
derivation does not depend on the choice of variables in the input clauses
(even if this choice is very important during the proofs), and these results
are still correct. However, these properties on variables have to be formally
proved from this independence result, and, furthermore, they can only express
properties on the objects occurring in the theorem (for instance, we
cannot suppose during a proof that a clause does not share variables with a
goal built in the proof if this goal does not appear in the theorem).
Standard semantics ( la Herbrand) of denite programs deals with well-known
objects: substitutions and renaming. However, several non-equivalent
denitions for these objects can be found in the literature, thus introducing
some confusion (for example, the meaning of renaming is often assumed
simpler than its formal denition implies). In [15], H. P. Ko and M. E. Nadel
point out that dierent authors give subtley dierent denitions of substitu-
tions. They cite six non-equivalent denitions and point out the implication
for the is an instance relation, thus giving dierent versions of the lifting
lemma. Therefore, substitutions are not as simple as they might rst ap-
pear, and this motivates some authors, as R. S. Kemp and G. A. Ringwood
in [14], to take the instance relation as primitive rather than taking substi-
tutions. There is also a confusion in the literature concerning the denition
of most general uniers (mgu in short). In [18], J. L. Lassez, M. J. Maher,
and K. Marriot compare four non-equivalent denitions of mgu. Of course,
logic programming is concerned with these problems and is also subject to
such confusions. For an SLD-derivation
the following denitions for the renaming process required in an SLD-deriv-
ation can be found:
and the confusion arises because all these conditions in fact dene dierent
hypotheses. There are at least two reasons for these conditions. First, the
standardization apart is needed in order to be able to unify the selected
atom with the head of the variant of the clause used. The last reason is
to obtain the most general possible answer (substitution). Therefore, this
formalization settles down the problem of variable renaming, which has long
been a cause of errors in the eld of logic programming.
Description of Coq
We use here version 6.2 of the proof assistant Coq [4], which allows the interactive
development of formal proofs. Coq is based on a logical framework
known as the calculus of inductive constructions [5], which is an extension of
a typed -calculus supporting dependent types and polymorphic types. The
basic idea underlying this logical framework, based on the Curry-Howard
isomorphism [9, 17], is that a proof of a proposition can be seen as a functional
object. For instance, a proof of a proposition of the form A ) B is a
function mapping every proof of A to a proof of B. The type of this function
is isomorphic to the proved proposition, so types and proposition are
identied, as are objects and proofs. Furthermore, this framework allows the
denition of inductive and co-inductive types (which are specied by their
constructors). A classical example of an inductive type is the denition of
natural numbers, which is dened in the system Coq by
Inductive
Three induction principles are (automatically) generated by this denition:
nat_id :(P:nat->s)(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n)
(id; s) is either (ind,Prop) or (rec,Set) or (rect,Type). A classical
example of a co-inductive type is the type of innite sequences, formed with
elements of type A, or streams for shorter. In Coq, it can be introduced by
CoInductive Set Stream [A:Set]:=cons:A->(Stream A)->(Stream A).
Note that there is no induction principle for co-inductive types. Coq also
allows the denition of mutually recursive types. We shall use here two
distinct sorts: Prop is the type of logical propositions; Set is the type of data
type specications. The type of Prop and Set is Type. Constructing a proof
within Coq is an interactive process: given a goal, the user species which
deduction rule should be applied, and Coq does all the computations. The
theorem prover solves successive subgoals with tactics (i.e., functions that
build a proof of a given goal from proofs of more elementary subgoals).
Goal
apply a tactic
Subgoal n
3 Terms and Unication
The rst step of this development consists naturally in formalizing uni-
cation of terms. The unication algorithm deals with two sets: terms and
substitutions. Let us rst present their formal denitions. Given a functional
signature  (i.e., a countable set with an arity function ar) and a countable
set X of variable symbols, terms (T  [X]) can be dened by induction as
follows:
if f is a functional symbol in  such that l is a list
of terms of length n, then tf(f; l) is a term.
At the same time, we introduce the dependent type L n; [X] of lists of terms
of length n (T  [X] and L n; [X] are mutually recursive).
Substitutions (S T ) are dened as applications from X to T [X]. Recall
now that given two terms t 1 and t 2 , if for a substitution s, we have
called a unier of t 1 and t 2 (unif_t). s is called a minimal
unier (min_unif_t), if for every unier s 0 of t 1 and t 2 , we have s  s 0 (i.e.,
there exists a substitution s 0 such that s 0 which is denoted by the
predicate less_subst_t). A unier s of t 1 and t 2 is called a most general
unier if it is minimal, idempotent (i.e. 8x 2 X which is
denoted by the predicate idempotent_t) and relevant to t 1 and t 2 (i.e., every
variable occurring in the domain of s also occurs in the list formed by t 1 and
and every variable occurring in the range of s also occurs in the
list formed by t 1 and t 2 (under_lt)). These denitions are extended to lists
of terms.
Instead of formalizing unication on terms by following the standard
approach (based on the unication algorithm), and since a similar (formal)
proof, dealing with quasi-terms, has been obtained by J. Rouyer [26], we have
transposed the unication property from quasi-terms to terms. Originally,
quasi-terms were introduced by Z. Manna and R. J. Waldinger in order
to illustrate their technique for program synthesis: in [21], an unication
algorithm has been derived by proving that its specication can be satised.
This proof has been veried within the Cambridge LCF theorem prover [10],
by L. C. Paulson [23]. A similar proof has been obtained by J. Rouyer [26]
for quasi-terms dened as follows:
are used to obtain variable quasi-terms, constant quasi-
terms and functional quasi-terms, ConsArg is used to build non-empty lists
of quasi-terms (terms and lists of terms are merged in a single data type).
For instance, the term f(x; a; g(x)) is obtained as follows
More precisely, J. Rouyer has proved that if there exists an unier for q 1
and q 2 , then if these two quasi-terms are well formed, this unier, which is
a quasi-substitution, is indeed a substitution. Clearly, T [X] is a proper
subset of Q [X] (ConsArg(ConsArg(x; x); x) is neither a term nor a list of
terms), and, in order to transpose the unication property, we have to dene
a mapping f from well-formed quasi-terms (i.e., quasi-terms representing
terms) to terms. However, Coq does not incorporate the notion of partiality:
any function is total. The current solution we have taken in this development
consists in considering simultaneously a quasi-term and the proof that it is
well formed. Hence, a predicate P on Q [X] characterizing well-formed
quasi-terms is dened. Depending on the type of P , two approaches are
possible. The rst one corresponds to a programming language
the type of P is dened recursively on the structure
of the quasi-term q considered. When q is not well formed, we use the
applied to Q [X] and to a proof of the
proposition False obtained from q and the proof that it is well-formed. The
second approach corresponds to a proofs language approach: the type of
dened recursively on the structure of the proof
that the quasi-term considered is well formed.
In addition to the interest of the unication theorem, we are motivated by
developing an approach based on the reusability of formal proofs. Therefore,
this development shows how to dene partial functions. More precisely, we
outline how from
two inductively dened sets,
a predicate P on E 1 , such that there exists a bijection between E 2 and
we can dene the following functions:
The two characteristics of this problem are as follows:
1 is dened by a predicate, that does not allow any (direct) denition
of functions or predicates on E P
1 . Therefore, every expression of the
stands for 8e
2. We just know the bijection between
such that
Furthermore, we would like to have
The function f 21 is easy to obtain, seeing that every e 2 in E 2 is in relation
with an element in E 1 . Furthermore, for every e 2 in
The denition of f 12 is rather critical because of the denition, by a pred-
icate, of the domain of f 12 . The technique used here consists in dening
inductively for every e 1 in E 1 , the collection P[e 1 of the
proofs of P logically equivalent, only P[e 1
has a computational content). Of course, for every e 1 in E P
1 , there must
exist a proof of P In this way, we are in position to dene,
recursively on the structure of such a proof, the function
Y
such that 8e 1 Hence, according to these def-
initions, proofs can be viewed as objects (data structures) of a mathematical
collection (inhabiting the Set type) with an explicit algorithmic content, thus
allowing to proceed by induction over these proofs or to dene recursive functions
on the structure of these proofs. Since E 2 is isomorphic to a subset
of our aim is to map result about E 1 to a result about E 2 by proving
only few conservativity lemmas. Let U 1 and U 2 be two formal properties,
respectively on E 1 and E 2 (quasi-unication and unication), such that
and assume that the property U 1 holds on E 1 . Given the two functions f 12
and f 21 , we can prove the property U 2 on E 2 , by the following reasoning. Let
e 2 be an element in by hypothesis, we have U 1 (f 21 (e 2 )), and there exists
a proof p for f 21
And the claim now follows, since
. In this manner, we have proved the unication theorem
without really working on unication, but by proving only few conservativity
lemmas (for a full presentation of this proof, see [13]).
Theorem 3.1 (Unication) Given two terms t 1 and t 2 , either t 1 and t 2
are not uniable, or they are and there exists an idempotent minimal unier
relevant to these terms.
4 Objects Used in Logic Programming
We present in this section the formal denitions of the objects used in logic
programming, and we introduce, for each of them, an interpretation schema.
First, let  be a relational signature. The collection At; [X] of atoms
is inductively dened as follows: if p is a predicate symbol in  such that
l is a list of terms of length n, then pl(p; l) is an atom. Then,
queries, denite clauses, denite programs, and Horn clauses are dened from
atoms by
(arity ar):fun -> nat
Mutual inductive
ar f)) -> Term
with list_term : nat -> Set :=
cons: (n:nat)Term -> (list_term n)->(list_term (S n)).
subst := var -> Term.
Inductive Unification_t[t1,t2:Term]:Set:=
(cons (S O) t1 (cons O t2 nil)))
(cons (S O) t1 (cons O t2 nil)))
->(Unification_t t1 t2).
Inductive quasiterm : Set :=
V:var->quasiterm | C:fun->quasiterm |
Root:fun->quasiterm->quasiterm |
ConsArg: quasiterm->quasiterm->quasiterm.

Table

1: Terms, substitutions, and unication.
In order to be able to give an interpretation of these objects, it is necessary
to attach some meaning to each of the symbols occurring in them. Therefore,
let us dene the interpretations of the signature [. For this, let ' n [A] be
the dependent polymorphic type of lists of elements of type A of length n,
and bool the set of booleans (with its usual operators,
order to dierentiate them from the operators :, ^, _ on Prop). We dene
two collections of mappings: F n [A] is formed by mappings from ' n [A] to A,
and P n [A] is formed by mappings from ' n [A] to bool. According to these
denitions, interpretations, over a domain D, are dened, in a classical way,
by
I
Y
F ar(f) [D] I
Y
Hence, given an interpretation I, over D, of  (resp. ), a n-ary function f
predicate p) is interpreted by a mapping f I
bool). We are now in position to give the following interpretation
At; [X] Inductive atom : Set :=
pl:(p:predic)(list_term (arity_p p))->atom.
Inductive request : Set :=
true_req:request|
cons_req:atom->request->request.
C; [X] Definition clause:Set:=(atom*request).
Inductive program : Set :=
nil_pgm:program|
cons_pgm:clause->program->program.
Inductive horn : Set :=
hp:program->horn|
hr:request->horn->horn.

Table

2: Syntactic objects.
schemes. First, we dene A X as the collection of valuations over A (mappings
from X to A). Then, terms (and lists of terms) are interpreted as follows:
let I be an interpretation of , over a domain D, a term t (resp. a list of
terms l of length n) is interpreted by an application
dened by
f I (l I (v)) if
l I
where nil_' and cons_' are the constructors of ' n [D] and cons is a constructor
of L n; [X]. Henceforth, we will nd it more convenient to write I
to denote an interpretation of  [  I  [D]  I  [D]). An object
clause, .) is interpreted by an application
dened by
I (l I (v))
r I
false if
(: b a I
true if
a I
I (v)) if
ri I (v) = a I (v) _ b r I (v)
true if
c I (v)
I (v) if
r I (v)
Inductive
[D:Set][n:nat](LIST D n)->D.
I  [D] Definition f_i : Set -> Set :=
[D:Set](f:fun)(f_n D (arity ar f)).
A X Definition valuation:Set->Set:=[A:Set](var->A).
Fixpoint Interp_t [D:Set;I:(f_i D);t:Term]
:(valuation D)->D:=[v:(valuation D)] Case t of
[f:fun][l:(list_term (arity ar f))]
((I f) (apply_l D I (arity ar f) l v)) end
with apply_l [D:Set;I:(f_i D);n:nat;l:(list_term n)]
(valuation D) -> (LIST D n) :=
[v:(valuation D)]<[n:nat](LIST D n)>Case l of
(NIL D)
[n0:nat][t0:Term][l0:(list_term n0)]
(CONS D n0 (Interp_t D I t0 v) (apply_l D I n0 l0 v))
end.
bool Inductive bool:Set:= true:bool | false:bool.
[D:Set][n:nat](LIST D n) -> bool.
I  [D] Definition p_i :Set -> Set :=
[D:Set](p:predic)(p_n D (arity_p p)).

Table

3: Interpretations of  [ .
An interpretation I, over a domain D, is said to be a model of an object
(atom, query, .), if for every valuation v, over D, we have
In this case, we write (depending on the interpretation schema used
for a query r, we write either I r or j= I ~ r). Note that, whereas given a
valuation v 2 D X , the proposition true is decidable, since D can be
an innite set, the proposition I o is not necessarily decidable. This will
introduce many complications in the following. To terminate, we dene the
relation of logical consequence (j=) between a Horn clause and a query as
follows:
General interpretation schema of
Definition Interp_O :(D:Set)(f_i D)->(p_i D)->O->
(valuation D)->bool:=[D:Set][If:(f_i D)][Ip:(p_i D)][o
[v:(valuation D)]  Case o of I end.
[p0:predic][l0:(list_term (arity_p p0))]
request
false
(orb (neg (Interp_p D If Ip l0 v)) (Interp_r D If Ip r0 v))
request
true
(andb (Interp_p D If Ip l0 v)) (Interp_rn D If Ip r0 v))
clause
[a:atom][r:request]
(orb (Interp_r D If Ip r v) (Interp_p D If Ip a v))
true
(andb (Interp_c D If Ip c0 v) (Interp_P D If Ip p0 v))
[p:program](Interp_P D If Ip p v)
(andb (Interp_r D If Ip r0 v) (Interp_h D If Ip h0 v))
I
Definition O_valid:(D:Set)(f_i D)->(p_i D)->O->Prop:=
((v:(valuation D))(Interp_O D If Ip l v)=true).
request -> Prop :=
(h_valid D If Ip h)->(reqn_valid D If Ip r) ).

Table

4: Interpretations and models.
5 SLD-Resolution
The logical approach of denite programs can be split in two parts: the
declarative semantics determines what can be computed; the operational semantics
(given by SLD-resolution) describes how it is computed. Execution
of denite programs is based on a combination of two mechanisms: replacement
and unication. This form of computing is a specic form of theorem
proving, called SLD-resolution (for Selection Linear Denite).
5.1 Resolution and Transitions
The resolution rule is an inference rule that denes a deductive relation,
C be the denite clause C + C in the program P ,
is an atom, called the head of C, and C a query, called the
body of C, R a query and r a renaming substitution such that no variable
occurring in r(C) also occurs in R. We can write the resolution rule in the
following abbreviated manner:
is a mgu of R =n and r(C
where R =n stands for the (n+ 1)-th atom of R (at_n_req), and where R[n
r(C )] is the query obtained by replacing in R, the (n 1)-th atom by
the query r(C ) ((change_n_r n (rsubst_req r (body_c C)) R)). In each
resolution step, two choices are made: the choice of the selected atom and
the choice of the input clause whose head unies with the selected atom.
Therefore, the resolution rule can be viewed as a rule that moves from a state
to another, dened as follows. First, we introduce SR as the collection of
mappings from X to X (the classical properties on substitutions are extended
to SR ) and a predicate P R on SR , characterizing the renaming substitutions
r such that
occurring in the domain of r also occurs in the range of r
(r is idempotent).
A resolution state is a pair :R, where  is a substitution and R a query.
We give now the formal denitions of the renaming conditions that have to
be satised during a transition  i :R i
. First, the initial resolution
state  i :R i must satisfy  i R Then, the renaming substitution r has
to rename all the variables occurring in C and only these variables; this is
denoted by PRC (r; C). Last, we dene two predicates satised when no variable
occurring in the range of r also occurs in the domain of  i (P RS
in the query R i (P RR We are now in position to dene the predicate
P , on the collection of transitions, by
where MGU(; a 1 ; a 2 ) (at_mgu) means that  is a most general unier of a 1
and a 2 .
5.2 SLD-Resolution and Derivations
A nite valid SLD-derivation is a nite sequence of composable transitions
satisfying the predicate
also
Hence, derivations can be dened inductively,
from , as lists. Most of proofs of properties of SLD-resolution are obtained
by induction over a derivation by using a left induction schema. However,
during the soundness proof, we shall need the right one. Hence, we dene
two collections of derivations as follows (D l and D r are isomorphic):
D l ::= d l
c (D l ;
| {z }
left induction
| {z }
right induction
Two functions are dened, in order to relate these two sets. As we did for the
transitions, we now dene a predicate, on D l , characterizing valid derivations
(sequence of composable transitions satisfying the predicate P and an
additional renaming condition). For this, we introduce the following deni-
tions. Two transitions e 1
f and e 2
f are said to be composable
. A function #, on D l ,
that computes the list of variables occurring in the input clauses of a deriva-
tion, is dened. The predicate P D , on D l , can now be recursively dened
by
t (t) and P (t), then P D (d)
Resolution states Definition state:Set:=(subst*request).
(Fst and Snd are projections on a product type.)
SR Definition rename:=var->var.
Definition good_rename:rename->Prop:=[sr:rename]
(((y:var)(x=y)->(rdom sr x)->(rdom sr y)->
(sr x)=(sr y))^((rdom sr x)->(rrange sr x))).
Definition rename_c:rename->clause->Prop:=
PRR
Definition rename_out_req:rename->request->Prop:=
PRS
Definition rename_out_dom:rename->subst->Prop:=
((x:var)(rdom r x)->(s (r x))=(tv (r x))).
Inductive trans:Set:=trans_cons:state->program->nat->
clause->rename->subst->atom->state->trans.
Inductive rsl [ei:state;p:program;n:nat;
c:clause;r:rename;s:subst;a:atom;ef:state]:Prop:=rsl_init:
(le (S n) (Length_r (Snd ei)))
(rsubst_at r (head_c c)))
(*H4*) ->(good_rename r)
(([x:var](Subst_t s ((Fst ei) x))), (subst_req s
->(rsl ei p n c r s a ef).
Definition RSL:trans->Prop:=[t:trans] Case t of
[a:atom][ef:state](rsl ei p n c r s a ef) end.

Table

5: Transitions.
D l
Inductive deriv:Set :=
deriv_cons : deriv -> trans -> deriv.
Inductive
deriv_f_cons : trans -> deriv_f -> deriv_f.
Inductive couple_trans_ok [t1:trans;t2:trans]:Prop:=
couple_trans_ok_init:(p_trans t1)=(p_trans t2)->
(state_end_t t1)=(state_init_t t2)->(RSL t1)->(RSL t2)
->(couple_trans_ok t1 t2).
Fixpoint list_var_c_d [d:deriv]:listv:=
Case d of
(var_cl (rsubst_cl (sr_trans t0) (c_trans t0)))
[d1:deriv][t1:trans](Appv (list_var_c_d d1)
(var_cl (rsubst_cl (sr_trans t1) (c_trans t1)))) end.
Fixpoint Deriv_ok [d:deriv]:Prop:= Case d of
((couple_trans_ok (end_d d2) t2)^(Deriv_ok d2)^
->(rrange (sr_trans t2) x))) end.

Table

Derivations.
where t d stands for the last transition of d 0 , R stands for the initial
query of d, and r stands for the renaming substitution used during the
transition t 0 .
These denitions allow a full formalization of classical properties of SLD-
resolution, presented in the next section.
6 Basic Results
SLD-resolution denes a relation satisfying several important properties.
The logical ones are soundness and completeness; two others are particular
to this form of computation: lifting and switching lemmas.
6.1 Two Classical Lemmas
6.1.1 Switching Lemma
At each resolution step of a derivation, an atom and a clause must be selected.
The following well-known lemma ensures that the non-determinism in the
choice of atom does not matter: this is called don't care non-determinism.
Lemma 6.1 (Switching) If during a valid derivation, two atoms A and B
are successively selected, then they can also be selected in the reverse order,
and the derived states are the same up to renaming of variables.
This lemma is proved by decomposing the two transitions:
s id :R 0
| {z }
d
s id stands for the identity substitution tv). Furthermore, note that we suppose
the rst selected atom is before the second in the query R, that's why
we have the assumption This proof (presented in details
in [12]) is classical and requires constantly the denition of the variable renaming
process used during a valid derivation. Note that we explicitely
build, during this proof, the substitution relating the two derived states, thus
allowing us to assert they are the same up to renaming of variables.
6.1.2 Lifting Lemma
The lifting lemma is another classical lemma and is used during the completeness
proof. As we said in the introduction, we have to assume some
additional conditions on the renaming used, in order to prove it.
Lemma 6.2 (Lifting) Let d : s id :R
be a valid derivation. If for
a nite list of variables l, we have dom()  l, then if
there exists a valid derivation s id :R
, such that    and for a
query R f , we have R
The proof is obtained by induction over the derivation (using a left induction
schema). Here again, the two derived states are explicitely related (for
a full presentation, see [12]).
6.2 Two Fundamental Properties
Answers and solutions dene the operational and declarative semantics of
denite programs. Given a denite program P , the solutions to a query
(Deriv_ok d) -> (Fst (state_init_d d))=tv
-> (Snd (state_init_d d))=(subst_req eta r) ->
->(rrange (sr_trans t) x)))
(p_trans t1)=(p_trans
(Fst
(Ex [rf:request]((Snd (state_end_d d0))=
(subst_req (Fst (state_end_d d0)) rf)
^(Snd (state_end_d d))=(subst_req (Fst (state_end_d d))
(subst_req eta rf))))
([x:var](Subst_t (Fst (state_end_d d)) (eta x)))))).
(Deriv_ok (deriv_cons (deriv_cons d t1) t2)) ->
(le (plus (n_trans t1) (Length_r (body_c (c_trans t1))))
(n_trans t2))->
(Fst (state_init_d d))=tv ->
((Deriv_ok (deriv_cons (deriv_cons d
(n_trans t3)=(S (minus (n_trans t2)
(Length_r (body_c (c_trans
(n_trans t4)=(n_trans
((Snd (state_end_d (deriv_cons (deriv_cons d t1) t2)))=
(subst_req r (Snd (state_end_d
(deriv_cons (deriv_cons d
(Snd (state_end_d (deriv_cons (deriv_cons d t3) t4)))))
-> (Ex [v:var] (r x)=(tv v)))))))).

Table

7: Lifting and switching lemmas.
(Fst (state_init_d d))=tv->(Snd (state_end_d d))=true_req
(subst_req (answer d) (Snd (state_init_t (head_d d))))).

Table

8: Soundness of SLD-resolution.
R are the substitutions  such that h p (P )
a declarative description of the desired output from denite program and
query. Conversely, we have the operational counterpart of solutions: answers.
If s id :R
is a valid derivation, then  is an answer to R.
6.2.1 Soundness of SLD-Resolution
The soundness theorem expresses that every answer to a query is also a
solution to this query.
Theorem 6.1 (Soundness) If, from a denite program P and a query R,
we get the valid derivation s id :R
The corresponding proof requires the notion of free transitions that are
transitions satisfying the resolution rule, except that the uniers used are
not necessarily most general uniers. Hence, the condition  on the
initial step (condition (*H5*) of the predicate rsl) does not necessarily hold.
This proof is obtained by using a right induction schema.
6.2.2 Completeness of SLD-Resolution
Let us now turn to the formalization of the completeness theorem of SLD-
resolution: if there exists a solution to a query, then there exists an answer
to this query (in this form, the completeness theorem is weaker than the
usual completeness theorem and the soundness theorem proved; we don't
relate here the solution with the answer). As usual, we need some new
denitions and lemmas rst: let us summarize them.
First, we have to dene Herbrand interpretations with respect to our
denitions. For this, we dene inductively the collection, T [;], of ground
terms (Ground_Term) that are terms not containing variables, obtained using
only function symbols occurring in  (this set is also called the Herbrand
universe of ). At the same time, the collection, L n; [;], of lists of ground
terms is dened. Similarly, we dene the collection, At; [;], of ground
atoms (Ground_Atom), which can be formed by using relation symbols from
with ground terms from the Herbrand universe of  as arguments (this
set is also called the Herbrand base of  [ ). We also dene S ; , as the
collection of ground substitutions (Ground_subst), which are mappings from
X to T [;] (which exactly corresponds to T [;] X ). Furthermore, to avoid
some uninteresting complications, we assume, from now, on that the signature
used, contains a constant (i.e., a 0-ary function symbol); hence the
above-dened sets are nonempty (in [8], J. H. Gallier discusses in detail the
need for at least one constant symbol in  in the context of the Herbrand
theorem).
We can now introduce the denition of the Herbrand interpretation of
, written H. For every f 2 , f H is a mapping from ' ar(f) [T  [;]] to T [;]
dened by:
where tfg is the unique constructor of ground terms and where l 0 has type
L ar(f) [;] and is obtained from l. Using this denition, we dene a Herbrand
interpretation of  [  as any interpretation over ground terms, based on
H. Since, for Herbrand interpretations, the assignment to constants and
functions is xed, it seems possible to identify a Herbrand interpretation I
of  [  with a subset of the Herbrand base, dened by a predicate (I),
characterizing the ground atoms a, such that I a
However, note that specications of I and (I) correspond to two dierent
kinds of specications: whereas for every Herbrand interpretation I and
every ground atom a, the proposition I a is decidable, for an arbitrary
predicate p, on At; [;], the proposition p(a) is not. Therefore, later, we'll
use in theorems, which need to get from a predicate on the Herbrand base,
a Herbrand interpretation, this proposition as an assumption (we will use
this assumption only as a mapping). Fixpoint characterization of the least
Herbrand model and completeness of SLD-resolution will be obtained only at
the cost of this strong assumption, implicitly suggested by the identication:
Type.
For every denite program P , we dene, by a predicate on At; [;], the
least Herbrand model of P as the intersection of all Herbrand models of
According to this denition, and from [28], we prove that M
)g. We wish now to obtain a deeper characterization
of this set using xpoint concepts. To study Herbrand models of
denite programs, R. Kowalski and M. van Emden associate with a denite
program P , an operator T P , called immediate consequence operator, which
provides the link between the declarative and operational semantics of de-
nite programs. Using the identication of a Herbrand interpretation with a
predicate on the Herbrand base, this operator is usually dened as follows.

Table

9: Declarative semantics.
Let P be a denite program, p a predicate on At; [;], and a a ground atom.
If for a clause c occurring in P and for a ground substitution  such that
then T P (p)(a). Since it is possible that some variables occur in the atoms a 0 ,
we cannot establish the decidability of T P (p), even if we know the decidability
of p: given an (not necessarily ground) atom and a Herbrand interpretation,
we cannot prove the decidability of the proposition this interpretation is a
model of this atom, needed to evaluate atoms not necessarily ground in
the body of the clause aected by T P .
Since Herbrand models of a program P are exactly the xpoints of T P , we
formalize some results on operators and their xpoints in a general setting.
In fact, T P is easily seen to be upward continuous, and it follows that its
least xpoint is T "!
P and is equal to M P .
us turn to the denition of the operational counterpart of the
least Herbrand model: the success set of a denite program, dened by a
predicate S P on the Herbrand base, characterizing the ground atoms a such
that there exists an SLD-refutation starting from a. From the two technical
lemmas presented in the end of this section, we prove that M P is equal to
S P and, under the assumption that every predicate on the Herbrand base is
decidable, we are now in position to prove the completeness theorem in the
following
Theorem 6.2 (Completeness) Let P be a denite program, R a non-empty
query, and  a solution for R. Then, there exists the following valid
derivation s id :R
operators
A:Set Definition PA:=A->Prop. Definition OP:=PA->PA.
Inductive ORD:Set:= Fixpoint ORD_FIRST [n:nat]:ORD:=
Case n of
So:ORD->ORD | Oo
Lo:(nat->ORD)->ORD. [p:nat](So (ORD_FIRST p)) end.
ordinal powers
Fixpoint
[a:A]False
[l:(nat -> ORD)]([a:A](Ex [n:nat]((POF f (l n)) a))) end.
Theorem

Table

10: Operators, ordinals, and xpoints.
One delicate step in the proof of the completeness theorem of SLD-resolution
is concerned with the combination of derivations. This proof is made by
induction over the length of the initial query, and the following argument is
always used:
has a refutation
Because each B i is ground, these refutations
can be combined into a refutation of P [
However, the combination of derivations is rather delicate, and the way it is
made is never given. Therefore, during the formalization of this proof, we
need a (technical?) lemma, whose proof is not so immediate and shows (in
a constructive way) how the nal refutation can be obtained from the initial
ones. Of course, in order to ensure the good properties on the variables
occurring in the nal refutation, we have to be able to rename the initial
refutations.
First, we have the following variant lemma, which is seldom stated and
whose proof is not immediate. It is proved, in a dierent form, in [2] and
stated in [20].
Lemma 6.3 (Variant lemma) Let l be a list of variables and d 1 the valid
derivation s id :R
There exists a valid derivation d 2 :s id :R
Inductive Tp
Inductive Success [p:program;a:Ground_Atom]:Prop :=
(p_deriv d)=p->(Deriv_ok d)->
(Fst (state_init_d d))=tv->(Snd (state_init_d d))=
(cons_req (Ground_to_atom a) true_req)->
(Snd (state_end_d d))=true_req-> (Success p a).
(r=true_req)-> (semantic_csq (hp p) (subst_req s r))->
(Fst (state_init_d
(Snd (state_end_d

Table

11: Completeness of SLD-resolution.
, such that no variable occurring in #(d 2 ) also occurs in l. Furthermore,
for a substitution s r such that dom(s r )  var(R 2 ), we have R
In other words, the existence of a derivation does not depend on the choice
of variables in the input clauses: it suces that the good properties hold.
Formalizing this lemma consists in building from a derivation d 1 starting
from R and from a nite set of variables Z, a derivation d 2 starting from R
such that no variable occurring in the input clauses of d 2 also occurs in Z.
R
| {z }
Z
| {z }
d2
As a (not so immediate) consequence, we obtain the following lemma.
Lemma 6.4 (Combination of derivations) Let P be a denite program,
R be a nonempty query, and  be a ground substitution. If every atom
occurring in R is in the success set of P , then, there exists a valid derivation
s id :R
Proof. We proceed by induction over R. For
the claim is obvious. For induction hypothesis,
if for every atom a 0 occurring in r, we have S P (a 0 ), then, there exists a
valid derivation s id :r
Moreover, by hypothesis, we have
By the induction hypothesis, we can build the valid derivation
I :r ; . Furthermore, by (1), we have S P (a) and, by denition, there exists
a valid derivation d
is a ground substitution,
we can prove, by induction over d 1 , that d 3 : s id :c r (a; r)
I :a is also
a valid derivation. Moreover, from d 2 and by Lemma 6.3, there exists a
valid derivation d 4 :  I :a
now, by induction over d 4 , we prove that d 5 :  I :a
valid derivation. Hence, by combining d 3 and d 5 , which is suitable for the
renaming conditions, one obtains the valid derivation s id :c r (a; r)
which settles the claim.  J
As we said, the formal completeness proved is weaker than the soundness
theorem proved: we don't relate the solution and the answer. This is
due to the following usual step in the proof:
be the variables of N . Enrich the
language of P by adding new constants a
be
the substitution fx 1 =a there exists an SLD-
refutation of P [ f
Ng (. By textually replacing in this refutation
a i by x i , for
This operation cannot be formalized by using our denitions (which do not
allow to add new constants in the functional signature or to textually replace
constants by variables and variables by constants). A possible solution
could consists in following the S-semantics approach developed in [7] which
allows variables in the Herbrand base.
7 Related Work
As we said, unication on quasi-terms has been formalized by L. C. Paulson
[23] using LCF and by J. Rouyer [26] using Coq. Concerning the deni-
tion of partial functions, C. Dubois and V. Vigui Donzeau-Gouge [6] have
recently proposed a method to generate automatically the predicate P characterizing
the domain of a partial function f from equations dening f in
a ML-style. Formal completeness proofs have been envisaged by several au-
thors. In [24], H. Persson presents a formalization, using the proof assistant
ALF, of a constructive completeness proof for intuitionistic predicate logic
w.r.t. models based on formal topology. In [11], J. Harrison discusses about
a formalization in HOL of basic rst-order model theory including Compact-
ness, Lowenheim-Skolem, and Uniformity theorems. In [16], J. L. Krivine
describes a formalization in second order-logic of an intuitionistic proof of
the completeness theorem of classical logic. Finally, note that in the area of
formal methods applied in logic programming, and starting from an operational
semantics for Prolog, the soundness and completeness proofs, for
each renement step toward the Warren Abstract Machine (WAM), have
been elaborated by C. Pusch [25] with the theorem prover Isabelle.
8 Conclusion
In order to prove formal properties about programs, it seems natural to
give a formal specication of their operational semantics. In this paper,
SLD-resolution has been formalized, and fundamental properties of this form
of computation have been proved (more than 600 technical lemmas have
been formalized during this development). The proofs we have machine-checked
are based on those in J. W. Lloyd's book [19] and then follow the
traditional we have chosen to take as the referential notion of
truth a semantical notion (an alternative could consist in taking another
referential notion like natural deduction or sequent calculus).
First, note that, instead of proving the unication theorem by following
the unication algorithm, as J. Rouyer did in [26], we have used his result on
quasi-terms to obtain our proof. The technique proposed is based on dening
a bijection between terms and quasi-terms satisfying a given predicate and
proving the preservation of the unication property. In this way, we have
proved the unication theorem without really dealing with unication theory,
thus avoiding a heavy proof requiring to handle sophisticated theories. This
construction is interesting because it represents an alternative to the classical
approach and shows how to take advantage of a previous formal proof, even
if the desired proof does not exactly deal with the same objects. Whereas
the unication theorem proved in [26] requires about 140 lemmas, only 75
lemmas have been proved in our development. This shows the interest that
a proofs library be provided.
In more informal presentations, variable renaming problems are often
ignored; however, these problems cannot be ignored here. As we said, the
results presented here have been proved in the calculus of inductive construc-
tions, thus making a dierence from the proofs one can nd in many books on
logic programming. The main dierence is concerned with the renaming process
used in an SLD-derivation: it is made explicit. A typical example is the
proof of the completeness theorem that requires a variant lemma (assert-
ing that the existence of an SLD-derivation does not depend on the choice of
variables in the input clauses used) and a lemma on combination of derivations
(which explicitely allows this operation), whose proofs are rather long.
Therefore, formalizing SLD-resolution introduces many complications. Even
if combining some SLD-derivations seems to be easy, this operation requires
several renamings in order to satisfy the standardization apart assumed
in the denition of a derivation. Usually, these lemmas are implicitly used
without any proof or any justication. Not surprisingly, a full formalization
of these proofs shows how minor details could be crucial. An interesting
discussion about these ne points, at the foundations of logic programming,
can be found in [15, 27]. Of course, the main problems come from the explicitation
of all the substitutions used during the unication and the variable
renaming processes: substitutions are a quite hard matter to deal with. In
[1], substitutions are said to be the minence grise of the -calculus, this can
also be said for SLD-resolution. Like SLD-resolution for clauses; -reduction
denes a relation on -terms, and it may be interesting to compare properties
of these relations. Whereas -reduction is conuent, SLD-resolution
just satises the switching property, which is weaker than conuence. Fur-
thermore, the variables renaming process used in an SLD-derivation can be
viewed as an implicit -conversion: the renaming is made explicit and allows
a full formalization of SLD-derivations, along the lines of the calculus
of explicit substitutions [1] for -reduction (the -calculus is a renement
of the -calculus, where substitutions are manipulated explicitely, and provides
a link between the classical -calculus and concrete implementations).
The renaming process required in an SLD derivation plays an essential role
in logic programming: it constitutes an important step in the denition of
operational semantics of denite programs from the declarative reading of
Horn clauses.

Acknowledgments

Many thanks to Ren Lalement for enlightening discussions
about this work, as well as the anonymous referees for some very
useful comments.



--R

Explicit substitutions.
Logic programming.
Contributions to the theory of logic programming.
Project Coq.
The calculus of constructions.
A step towards the mechanization of partial functions: domains as inductive predicates.
Declarative modeling of the operational behavior of logic languages.
Logic for computer science
Proofs and Types
Edinburgh LCF
Formalizing basic
Formalization of SLD-resolution in the calculus of inductives constructions

Reynolds and Heyting models of logic programs.
In Koichi Furukawa
Une preuve formelle et intuitionniste du thorme de compltude de la logique classique.
Computation as Logic.

Foundations of Logic Programming.
Partial evaluation in logic program- ming
Deductive synthesis of the uni
Logic Programming and Prolog.
Verifying the uni
Constructive completeness of Intuitionistic Predicate Logic: A formalization in Type theory.

Dveloppement de l'algorithme d'uni
The role of standardising apart in logic programming.
The semantics of predicate logic as a programming language.
--TR
calculus of inductive constructions;SLD-resolution;standardization apart;formal proofs;semantics of logic programs