On completeness of logic programs?
Wlodzimierz Drabent
Institute of Computer Science, Polish Academy of Sciences, and
IDA, Linköpings universitet, Sweden
drabent at ipipan dot waw dot pl

arXiv:1411.3015v1 [cs.LO] 11 Nov 2014

November 10, 2014
Abstract. Program correctness (in imperative and functional programming) splits in logic programming into correctness and completeness.
Completeness means that a program produces all the answers required
by its specification. Little work has been devoted to reasoning about
completeness. This paper presents a few sufficient conditions for completeness of definite programs. We also study preserving completeness
under some cases of pruning of SLD-trees (e.g. due to using the cut).
We treat logic programming as a declarative paradigm, abstracting from
any operational semantics as far as possible. We argue that the proposed
methods are simple enough to be applied, possibly at an informal level, in
practical Prolog programming. We point out importance of approximate
specifications.
Keywords: logic programming, program completeness, declarative program-

ming, approximate specification.

1

Introduction

The notion of partial program correctness splits in logic programming into correctness and completeness. Correctness means that all answers of the program
are compatible with the specification, completeness – that the program produces
all the answers required by the specification.
In this paper we consider definite clause programs, and present a few sufficient
conditions for their completeness. We also discuss preserving completeness under
pruning of SLD-trees (by e.g. using the cut). We are interested in declarative
reasoning, i.e. abstracting from any operational semantics, and treating program
clauses as logical formulae. Our goal is simple methods, which may be applied –
possibly informally – in actual practical programming.
Related work. Surprisingly little work was devoted to proving completeness of
programs. Hogger [12] defines the notion of completeness, but does not provide
any sufficient conditions. Completeness is not discussed in the important monograph [1]. Instead, a characterization is studied of the set of computed instances
?

Accepted, without the appendix, for post-conference proceedings of LOPSTR 2014
(24th International Symposium on Logic-Based Program Synthesis and Transformation. Canterbury, UK, September 2014), to appear in 2015 in Springer LNCS.

of an atomic query, in a special case when the set is finite and the answers are
ground. In the paper [15] of Kowalski completeness is discussed, but the example proofs concern only correctness. As a sufficient condition for completeness
of a program P he suggests P ` TS , where TS is a specification in a form of
a logical theory. The condition seems impractical as it fails when TS contains
auxiliary predicates, not occurring in P . It also requires that all the models of P
(including the Herbrand base) are models of the specification. But it seems that
such specifications often have a substantially restricted class of models, maybe
a single Herbrand model, cf. [4].
Deville [4] provides an approach where correctness and completeness of programs should follow from construction. No direct sufficient criteria for completeness, applicable to arbitrary programs, are given. Also the approach is not
declarative, as it is based on an operational semantics of SLDNF-resolution.
Stärk [18] presents an elegant method of reasoning about a broad class of
properties of programs with negation, executed under LDNF-resolutions. A tool
to verify proofs mechanically was provided. The approach involves a rather complicated induction scheme, so it seems impossible to apply the method informally
by programmers. Also, the approach is not fully declarative, as the order of literals in clause bodies is important.
A declarative sufficient condition for program completeness was given by Deransart and Maluszyński [3]. The approach presented here stems from [10], the
differences are discussed in the full version of this paper [9]. The main contribution since the former version [7] is proving completeness of pruned SLD-trees.
The author is not aware of any other work on this issue.
Preliminaries. We use the standard notation and definitions [1]. An atom whose
predicate symbol is p will be called a p-atom (or an atom for p). Similarly, a
clause whose head is a p-atom is a clause for p. In a program P , by procedure p
we mean the set of the clauses for p in P .
We assume a fixed alphabet with an infinite set of function symbols. The
Herbrand universe will be denoted by HU, the Herbrand base by HB, and the sets
of all terms, respectively atoms, by T U and T B. For an expression (a program)
E by ground(E) we mean the set of ground instances of E (ground instances of
the clauses of E). MP denotes the least Herbrand model of a program P .
By “declarative” (property, reasoning, . . . ) we mean referring only to logical reading of programs, thus abstracting from any operational semantics. In
particular, properties depending on the order of atoms in clauses will not be
considered declarative (as they treat equivalent conjunctions differently).
By a computed (respectively correct) answer for a program P and a query Q
we mean an instance Qθ of Q where θ is a computed (correct) answer substitution
[1] for Q and P . We often say just answer as each computed answer is a correct
one, and each correct answer (for Q) is a computed answer (for Q or for some
its instance). Thus, by soundness and completeness of SLD-resolution, Qθ is an
answer for P iff P |= Qθ.
Names of variables begin with an upper-case letter. We use the list notation
of Prolog. So [t1 , . . . , tn ] (n ≥ 0) stands for the list of elements t1 , . . . , tn . Only a
2

term of this form is considered a list. (Thus terms like [a, a|X], or [a, a|a], where
a is a constant, are not lists). The set of natural numbers will be denoted by N;
f : A ,→ B states that f is a partial function from A to B.
The next section introduces the basic notions of specifications, correctness
and completeness. Also, advantages of approximate specifications are discussed.
After a brief overview of proving correctness, we discuss proving program completeness. Sect. 4 deals with proving that completeness is preserved under pruning. We finish with a discussion. For missing proofs, more examples etc see [9].

2

Correctness and completeness

Specifications. The purpose of a logic program is to compute a relation, or
a few relations. A specification should describe these relations. It is convenient
to assume that the relations are over the Herbrand universe. To describe such
relations, one relation corresponding to each procedure of the program (i.e. to
a predicate symbol), it is convenient to use a Herbrand interpretation. Thus a
(formal) specification is a Herbrand interpretation, i.e. a subset of HB.
Correctness and completeness. In imperative and functional programming,
correctness usually means that the program results are as specified. In logic
programming, due to its non-deterministic nature, we actually have two issues:
correctness (all the results are compatible with the specification) and completeness (all the results required by the specification are produced). In other words,
correctness means that the relations defined by the program are subsets of the
specified ones, and completeness means inclusion in the opposite direction. In
terms of specifications and the least Herbrand models we define:
Definition 1 Let P be a program and S ⊆ HB a specification. P is correct
w.r.t. S when MP ⊆ S; it is complete w.r.t. S when MP ⊇ S.
We will sometimes skip the specification when it is clear from the context. We
propose to call a program fully correct when it is both correct and complete.
If a program P is fully correct w.r.t. a specification S then, obviously, MP = S.
A program P is correct w.r.t. a specification S iff Q being an answer of P
implies S |= Q. (Remember that Q is an answer of P iff P |= Q.) The program
is complete w.r.t. S iff S |= Q implies that Q is an answer of P . (Here our
assumption on an infinite set of function symbols is needed [9].)
It is sometimes useful to consider local versions of these notions:
Definition 2 A predicate p in P is correct w.r.t. S when each p-atom of
MP is in S, and complete w.r.t. S when each p-atom of S is in MP .
An answer Q is correct w.r.t. S when S |= Q.
P is complete for a query Q w.r.t. S when S |= Qθ implies that Qθ is an
answer for P , for any ground instance Qθ of Q.
Informally, P is complete for Q when all the answers for Q required by the
specification S are answers of P . Note that a program is complete w.r.t. S iff it
is complete w.r.t. S for any query iff it is complete w.r.t. S for any query A ∈ S.
3

Approximate specifications. Often it is difficult, and not necessary, to specify
the relations defined by a program exactly; more formally, to require that MP is
equal to a given specification. Often the relations defined by programs are not exactly those intended by programmers. For instance this concerns the programs
in Chapter 3.2 of the textbook [19] defining predicates member/2, append/3,
sublist/2, and some others. The defined relations are not those of list membership, concatenation, etc. However this is not an error, as for all intended queries
the answers are as for a program defining the intended relations. The exact semantics of the programs is not explained in the textbook; such explanation is
not needed. Let us look more closely at append/3.
Example 3. 1. The program APPEND
app( [H|K], L, [H|M ] ) ← app( K, L, M ).

app( [ ], L, L ).

does not define the relation of list concatenation. For instance, APPEND |=
app([ ], 1, 1). In other words, APPEND is not correct w.r.t.
0
SAPPEND
= { app(k, l, m) ∈ HB | k, l, m are lists, k ∗ l = m },

where k ∗ l stands for the concatenation of lists k, l. It is however complete w.r.t.
0
SAPPEND
, and correct w.r.t.
0
SAPPEND = { app(k, l, m) ∈ HB | if l or m is a list then app(k, l, m) ∈ SAPPEND
}.
0
Correctness w.r.t. SAPPEND and completeness w.r.t. SAPPEND
are sufficient to
show that APPEND will produce the required results when used to concatenate
or split lists. More precisely, the answers for a query Q = app(s, t, u), where t is
a list or u is a list, are app(sθ, tθ, uθ), where sθ, tθ, uθ are lists and sθ ∗ tθ = uθ.
(The lists may be non-ground.)
2. Similarly, the procedures member/2 and sublist/2 are complete w.r.t
specifications describing the relation of list membership, and the sublist relation. It is easy to provide specifications, w.r.t. which the procedures are correct.
For instance, member/2 is correct w.r.t. SMEMBER = { member(t, u) ∈ HB | if
u = [t1 , . . . , tn ] for some n ≥ 0 then t = ti , for some 0 < i ≤ n }.
3. The exact relations defined by programs are often misunderstood. For
instance, in [5, Ex. 15] it is claimed that a program P rog1 defines the relation
of list inclusion. In our terms, this means that predicate included of P rog1 is
correct and complete w.r.t.


l1 , l2 are lists,
included (l1 , l2 ) ∈ HB
.
every element of l1 belongs to l2

However the correctness does not hold: The program contains a unary clause
included ([ ], L), so P rog1 |= included ([ ], t) for any term t,
The examples show that in many cases it is unnecessary to know the semantics of a program exactly. Instead it is sufficient to describe it approximately. An approximate specification is a pair of specifications Scompl , Scorr ,
4

for completeness and correctness. The intention is that the program is complete
w.r.t. the former, and correct w.r.t. the latter: Scompl ⊆ MP ⊆ Scorr . In other
words, the specifications Scompl , Scorr describe, respectively, which atoms have
to be computed, and which are allowed to be computed. For the atoms from
Scorr \ Scompl the semantics of the program is irrelevant. By abuse of terminology, Scorr or Scompl will sometimes also be called approximate specifications.
Proving correctness We briefly discuss proving correctness, as it is complementary to the main subject of this paper. The approach is due to Clark [2].
Theorem 4 (Correctness). A sufficient condition for a program P to be correct w.r.t. a specification S is
for each ground instance H ← B1 , . . . , Bn of a clause of the program,
if B1 , . . . , Bn ∈ S then H ∈ S.
Example 5. Consider a program SPLIT and a specification describing how the
sizes of the last two arguments of s are related (|l| denotes the length of a list l):
s([ ], [ ], [ ]).

(1)

s([X|Xs], [X|Y s], Zs) ← s(Xs, Zs, Y s).

(2)

S = { s(l, l1 , l2 ) | l, l1 , l2 are lists, 0 ≤ |l1 | − |l2 | ≤ 1 }.
SPLIT is correct w.r.t. S, by Th. 4 (the details are left for the reader, or see [9]).
A stronger specification for which SPLIT is correct is shown in Ex. 11.
The sufficient condition is equivalent to S |= P , and to TP (S) ⊆ S.
Notice that the proof method is declarative. The method should be well
known, but is often neglected. For instance it is not mentioned in [1], where a
more complicated method, moreover not declarative, is advocated. That method
is not more powerful than the one of Th. 4 [10]. See [10,9] for further examples,
explanations, references and discussion.

3

Proving completeness

We first introduce a notion of semi-completeness, and sufficient conditions under
which semi-completeness of a program implies its completeness. Then a sufficient
condition follows for semi-completeness. We conclude the section with a way of
showing completeness directly without employing semi-completeness.
Definition 6 A level mapping is a function | |: HB → N assigning natural
numbers to atoms.
A program P is recurrent w.r.t. a level mapping | | [1] if, in every ground
instance H ← B1 , . . . , Bn ∈ ground(P ) of its clause (n ≥ 0), |H| > |Bi | for all
i = 1, . . . , n. A program is recurrent if it is recurrent w.r.t. some level mapping.
A program P is acceptable w.r.t. a specification S and a level mapping
| | if P is correct w.r.t. S, and for every H ← B1 , . . . , Bn ∈ ground(P ) we
have |H| > |Bi | whenever S |= B1 , . . . , Bi−1 . A program is acceptable if it is
acceptable w.r.t. some level mapping and some specification.
5

The definition of acceptable is more general than that of [1], which requires
S to be a model of P . Both definitions make the same programs acceptable [9].
Definition 7 A program P is semi-complete w.r.t. a specification S if P is
complete w.r.t. S for any query Q for which there exists a finite SLD-tree.
Less formally, the existence of a finite SLD-tree means that P with Q terminates under some selection rule. For a semi-complete program, if a computation
for a query Q terminates then all the required by the specification answers for
Q have been obtained. Note that a complete program is semi-complete. Also:
Proposition 8 (Completeness) Let a program P be semi-complete w.r.t. S.
The program is complete w.r.t S if
1. for each query A ∈ S there exists a finite SLD-tree, or
each A ∈ S is an instance of a query Q for which a finite SLD-tree exists, or
2. the program is recurrent, or
3. the program is acceptable (w.r.t. a specification S 0 possibly distinct from S).
Proving semi-completeness. We need the following notion.
Definition 9 A ground atom H is covered by a clause C w.r.t. a specification
S [17] if H is the head of a ground instance H ← B1 , . . . , Bn (n ≥ 0) of C, such
that all the atoms B1 , . . . , Bn are in S. A ground atom H is covered by a
program P w.r.t. S if it is covered w.r.t. S by some clause C ∈ P .
For instance, given a specification S = {p(si (0)) | i ≥ 0}, atom p(s(0)) is
covered both by p(s(X)) ← p(X) and by p(X) ← p(s(X)).
Now we present a sufficient condition for semi-completeness. Together with
Prop. 8 it provides a sufficient condition for completeness.
Theorem 10 (Semi-completeness). If all the atoms from a specification S
are covered w.r.t. S by a program P then P is semi-complete w.r.t. S.
Example 11. We show that program SPLIT from Ex. 5 is complete w.r.t.


s([t1 , . . . , t2n ], [t1 , · · · , t2n−1 ], [t2 , · · · , t2n ]),
n ≥ 0,
SSPLIT =
,
s([t1 , . . . , t2n+1 ], [t1 , · · · , t2n+1 ], [t2 , · · · , t2n ]) t1 , . . . , t2n+1 ∈ HU
where [tk , · · · , tl ] denotes the list [tk , tk+2 , . . . , tl ], for k, l both odd or both even.
Atom s([ ], [ ], [ ]) ∈ SSPLIT is covered by clause (1). For n > 0, any atom A =
s([t1 , . . . , t2n ], [t1 , · · · , t2n−1 ], [t2 , · · · , t2n ]) is covered by an instance of (2) with a
body B = s([t2 , . . . , t2n ], [t2 , · · · , t2n ], [t3 , · · · , t2n−1 ]). Similarly, for n ≥ 0 and any
atom A = s([t1 , . . . , t2n+1 ], [t1 , · · · , t2n+1 ], [t2 , · · · , t2n ]), the corresponding body
is B = s([t2 , . . . , t2n+1 ], [t2 , · · · , t2n ], [t3 , · · · , t2n+1 ]). In both cases, B ∈ SSPLIT .
(To see this, rename each ti as t0i−1 .) So SSPLIT is covered by SPLIT. Thus
SPLIT is semi-complete w.r.t. SSPLIT , by Th. 10.
6

Now by Prop. 8 the program is complete, as it is recurrent under the level
mapping |s(t, t1 , t2 )| = |t|, where | [h|t] | = 1 + |t| and |f (t1 , . . . , tn )| = 0 (for any
ground terms h, t, t1 , . . . , tn , and any function symbol f distinct from [ | ] ).
By Th. 4 the program is also correct w.r.t. SSPLIT , as SSPLIT |= SPLIT. (The
details are left to the reader.) Hence SSPLIT = MSPLIT .
Note that the sufficient condition of Th. 10 is equivalent to S ⊆ TP (S), which
implies S ⊆ gfp(TP ). It is also equivalent to S being a model of ONLY-IF(P )
(see e.g. [6] or [10] for a definition).
The notion of semi-completeness is tailored for finite programs. An SLD-tree
for a query Q and an infinite program P may be infinite, but with all branches
finite. In such case, if the condition of Th. 10 holds then P is complete for Q [9].
Proving completeness directly. Here we present another declarative way of
proving completeness; a condition is added to Th. 10 so that completeness is
implied directly. This also works for non-terminating programs. However when
termination has to be shown anyway, applying Th. 10 seems simpler.
In this section we allow that a level mapping is a partial function | |: HB ,→ N
assigning natural numbers to some atoms.
Definition 12 A ground atom H is recurrently covered by a program P
w.r.t. a specification S and a level mapping | |: HB ,→ N if H is the head of a
ground instance H ← B1 , . . . , Bn (n ≥ 0) of a clause of the program, such that
|H|, |B1 |, . . . |Bn | are defined, B1 , . . . , Bn ∈ S, and |H| > |Bi | for all i = 1, . . . , n.
For instance, given a specification S = { p(si (0)) | i ≥ 0 }, atom p(s(0)) is
recurrently covered by a program { p(s(X)) ← p(X).} under a level mapping
for which |p(si (0))| = i. No atom is recurrently covered by { p(X) ← p(X).}.
Obviously, if H is recurrently covered by P then it is covered by P . If H is
covered by P w.r.t. S and P is recurrent w.r.t. | | then H is recurrently covered
w.r.t. S, | |. The same holds for P acceptable w.r.t. an S 0 ⊇ S.
Theorem 13 (Completeness 2). (A reformulation of Th. 6.1 of [3]). If, under some level mapping | |: HB ,→ N, all the atoms from a specification S are
recurrently covered by a program P w.r.t. S then P is complete w.r.t. S.
Example 14. Consider a directed graph E. As a specification for a program describing reachability in E, take S = Sp ∪ Se , where
Sp = { p(t, u) | there is a path from t to u in E },
Se = { e(t, u) | (t, u) is an edge in E }.
Let P consist of a procedure p: { p(X, X). p(X, Z) ← e(X, Y ), p(Y, Z).} and a
procedure e which is a set of unary clauses describing the edges of the graph.
Assume the latter is complete w.r.t. Se . Notice that when E has cycles then
infinite SLD-trees cannot be avoided, and completeness of P cannot be shown
by Prop. 8.
7

To apply Th. 13, let us define a level mapping for the elements of S such that
|e(t, u)| = 0 and |p(t, u)| is the length of a shortest path in E from t to u (so
|p(t, t)| = 0). Consider a p(t, u) ∈ S where t 6= u. Let t = t0 , t1 , . . . , tn = u be a
shortest path from t to u. Then e(t, t1 ), p(t1 , u) ∈ S, |p(t, u)| = n, |e(t, t1 )| = 0,
and |p(t1 , u)| = n − 1. Thus p(t, u) is recurrently covered by P w.r.t. S and | |.
The same trivially holds for the remaining atoms of S. So P is complete w.r.t. S.

4

Pruning SLD-trees and completeness

Pruning some parts of SLD-trees is often used to improve efficiency of programs.
It is implemented by using the cut, the if-then-else construct of Prolog, or builtins, like once/1. Pruning preserves the correctness of a logic program, it also
preserves termination under a given selection rule, but may violate the program’s
completeness. We now discuss proving that completeness is preserved.
By a pruned SLD-tree for a program P and a query Q we mean a tree
with the root Q which is a connected subgraph of an SLD-tree for P and Q. By
an answer of a pruned SLD-tree we mean the computed answer of a successful
SLD-derivation which is a branch of the tree. We will say that a pruned SLDtree T with root Q is complete w.r.t. a specification S if, for any ground Qθ,
S |= Qθ implies that Qθ is an instance of an answer of T . Informally, such a tree
produces all the answers for Q required by S.
We present two approaches for proving completeness of pruned SLD-trees.
The first one is based on viewing pruning as skipping certain clauses while building the children of a node. The other deals with a restricted usage of the cut.
4.1

Pruning as clause selection.

To facilitate reasoning about the answers of pruned SLD-trees, we will now view
pruning as applying only certain clauses while constructing the children of a
node. So we introduce subsets Π1 , . . . , Πn of P .
. . . ,A,. . .
The intention is that for each node the clauses of
P
···
exactly one Πi are used. Programs Π1 , . . . , Πn
Πi
···
may be not disjoint.
not pruned
pruned
Definition 15 Given programs Π1 , . . . , Πn (n > 0), a c-selection rule is a
function assigning to a query Q0 an atom A in Q0 and one of the programs
∅, Π1 , . . . , Πn .
A csSLD-tree (cs for clause selection) for a query Q and programs
Π1 , . . . , Πn , via a c-selection rule R, is constructed as an SLD-tree, but for each
node its children are constructed using the program selected by the c-selection
rule. An answer of a csSLD-tree is defined in the expected way.
A c-selection rule may choose the empty program, thus making a given node
a leaf. Notice
S that a csSLD-tree for Q and Π1 , . . . , Πn is a pruned SLD-tree
for Q and i Πi . Conversely, for each pruned SLD-tree T for Q and a (finite)
program P there exist n > 0, and Π1 , . . . , Πn ⊆ P such that T is a csSLD-tree
for Q and Π1 , . . . , Πn .
8

Example 16. We show that completeness of each of Π1 , . . . , Πn is not sufficient
for completeness of a csSLD-tree for Π1 , . . . , Πn . Consider a program P :
q(X) ← p(Y, X). (3)

p(a, s(X)) ← p(a, X). (5)

p(Y, 0).

p(b, s(X)) ← p(b, X). (6)

(4)

and programs Π1 = {(3), (4), (6)}, Π2 = {(3), (4), (5)}, As a specification for
completeness consider S0 = { q(sj (0)) | j ≥ 0 }. Each of the programs Π1 , Π2 , P
is complete w.r.t. S0 . Assume a c-selection rule R choosing alternatively Π1 , Π2
along each branch of a tree. Then the csSLD-tree for q(sj (0)) ∈ S0 via R (where
j > 2) has no answers, thus the tree is not complete w.r.t. S0 .
Consider
programs P,
1 , . . . , Πn and specifications S, S1 , . . . , Sn , such that
Sn
SΠ
n
P ⊇ i=1 Πi and S = i=1 Si . The intention is that each Si describes which
answers are to be produced by using Πi in the first resolution step. We will call
Π1 , . . . , Πn , S1 , . . . , Sn a split (of P and S). Note that Π1 , . . . , Πn or S1 , . . . , Sn
may be not disjoint.
S
Definition 17 Let S = Π1 , . . . , Πn , S1 , . . . , Sn be a split, and S = Si .
Specification Si is suitable for an atom A w.r.t. S when no instance of A
is in S \ Si . (In other words, when ground(A) ∩ S ⊆ Si .) We also say that a
program Πi is suitable for A w.r.t. S when Si is.
A c-selection rule is compatible with S if for each non-empty query Q it
selects an atom A and a program Π, such that
– Π ∈ {Π1 , . . . , Πn } is suitable for A w.r.t. S, or
– none of Π1 , . . . , Πn is suitable for A w.r.t. S and Π = ∅ (so Q is a leaf ).
A csSLD-tree for Π1 , . . . , Πn via a c-selection rule compatible with S is said
to be weakly compatible with S. The tree is compatible with S iff for each
its nonempty node some Πi is selected.
The intuition is that when Πi is suitable for A then Si is a fragment of S
sufficient to deal with A. It describes all the answers for query A required by S.
The reason of incompleteness of the trees in Ex. 16 may be understood as
selecting a Πi not suitable for the selected atom. Take S = Π1 , Π2 , S0 ∪ S10 , S0 ∪
S20 , where S10 = { p(b, si (0)) | i ≥ 0 } and S20 = { p(a, si (0)) | i ≥ 0 }. In the
incomplete trees, Π1 is selected for an atom A = p(a, u), or Π2 is selected for an
atom B = p(b, u) (where u ∈ T U). However Π1 is not suitable for A whenever A
has an instance in S (as then ground(A) ∩ S 6⊆ S0 ∪ S10 ); similarly for Π2 and B.
When Πi is suitable for A then if each atom of Si is covered by Πi (w.r.t. S)
then using for A only the clauses of Πi does not impair completeness w.r.t. S:
Sn
Sn
Theorem 18. Let P ⊇ i=1 Πi (where n > 0) be a program, S = i=1 Si a
specification, and T a csSLD-tree for Π1 , . . . , Πn . If
1. for each i = 1, . . . , n, all the atoms from Si are covered by Πi w.r.t. S, and
2. T is compatible with Π1 , . . . , Πn , S1 , . . . , Sn ,
3. (a) T is finite, or
9

(b) program P is recurrent, or
(c) P is acceptable (possibly w.r.t. a specification distinct from S), and T is
built under the Prolog selection rule
then T is complete w.r.t. S.
Example 19. The following program SAT0 is a simplification of a fragment of
the SAT solver of [13] discussed in [7]. Pruning is crucial for the efficiency and
usability of the original program.
p(P -P, [ ]).

(7)

q(V -P,

) ← V = P.

(10)

p(V -P, [B|T ]) ← q(V -P, [B|T ]). (8)

q( , [A|T ]) ← p(A, T ). (11)

p(V -P, [B|T ]) ← q(B, [V -P |T ]). (9)

P = P.

(12)

The program is complete w.r.t. a specification


p(t0 -u0 , [t1 -u1 , . . . , tn -un ]), n ≥ 0, t0 , . . . , tn , u0 , . . . , un ∈ T,
S=
∪ S=
q(t0 -u0 , [t1 -u1 , . . . , tn -un ]) ti = ui for some i ∈ {0, . . . , n}
where T = {false, true} ⊆ HU, and S= = { t=t | t ∈ HU }. We omit a completeness proof, mentioning only that SAT0 is recurrent w.r.t. a level mapping
|p(t, u)| = 2|u| + 2, |q(t, u)| = 2|u| + 1, |=(t, u)| = 0, where |u| is as in Ex. 11.
The first case of pruning is due to redundancy within (8), (9); both Π1 =
SAT0\{(9)} and Π2 = SAT0\{(8)} are complete w.r.t. S. For any selected atom
at most one of (8), (9) is to be used, and the choice is dynamic. As the following
reasoning is independent from this choice, we omit further explanations.
So in such pruned SLD-trees the children of each node are constructed using
one of programs Π1 , Π2 . Thus they are csSLD-trees for Π1 , Π2 . They are compatible with S = Π1 , Π2 , S, S (as Π1 , Π2 are trivially suitable for any A, due to
Si = S and S \ Si = ∅ in Df. 17). Each atom of S is covered w.r.t. S both by Π1
and Π2 . As SAT0 is recurrent, by Th. 18, each such tree is complete w.r.t. S.
Example 20. We continue with program SAT0 and specification S from the previous example, and add a second case of pruning. When the selected atom is of
the form A = q(s1 , s2 ) with a ground s1 then only one of clauses (10), (11) is
needed – (10) when s1 is of the form t-t, and (11) otherwise. The other clause
can be abandoned without losing the completeness w.r.t. S.1
Actually, SAT0 is included in a bigger program, say P = SAT0 ∪Π0 . We skip
the details of Π0 , let us only state that P is recurrent, Π0 does not contain any
clause for p or for q, and that P is complete w.r.t. a specification S 0 = S ∪ S0
where S0 does not contain any p- or q-atom. (Hence each atom of S0 is covered
by Π0 w.r.t. S 0 .)
1

The same holds for A of the form q(s11 -s11 , s2 ), or q(s11 -s12 , s2 ) with nonunifiable s11 , s12 . The pruning is implemented using the if-then-else construct in
Prolog: q(V-P,[A|T]) :- V=P -> true ; p(A,T). (And the first case of pruning
by p(V-P,[B|T]) :- nonvar(V) -> q(V-P,[B|T]) ; q(B,[V-P|T]).)

10

To formally describe the trees for P resulting from both cases of pruning,
consider S = Π0 , . . . , Π5 , S0 , . . . , S5 , where
Π1
Π3
Π4
Π5

= {(7), (8)}, Π2 = {(7), (9)},
= {(10)},
= {(11)},
= {(12)},

S1
S3
S4
S5

= S2 = S ∩ { p(s, u) | s, u ∈ HU },
= S ∩ { q(t-t, s) | t, s ∈ HU },
= S ∩ { q(t-u, s) | t, u, s ∈ HU, t 6= u },
= S= .

Each atom from Si is covered by Πi w.r.t. S (for i = 0, . . . , 5). For each qatom with its first argument ground, Π3 or Π4 (or both) is suitable. For each
remaining atom from T B, a program from Π0 , Π1 , Π2 , Π5 is suitable.
Consider a pruned SLD-tree T for P (employing the two cases of pruning
described above). Assume that each q-atom selected in T has its first argument
ground. Then T is a csSLD-tree compatible with S. From Th. 18 it follows that
T is complete w.r.t. S.
The restriction on the selected q-atoms can be implemented by means of
Prolog delays. This can be done in such a way that floundering is avoided for
the intended initial queries [13]. So the obtained pruned trees are as T above,
and the pruning preserves completeness of the program.
Example 21. A Prolog program {nop(adam, 0) ← !. nop(eve, 0) ← !. nop(X, 2).}
is an example of difficulties and dangers of using the cut in Prolog. Due to the cut,
for an atomic query A only the first clause with the head unifiable with A will be
used. The program can be seen as logic program P = Π1 ∪Π2 ∪Π3 executed with
pruning, where (for i = 1, 2, 3) Πi is the i-th clause of the program with the cut
removed. The intended meaning
 is S = S1 ∪S2 ∪S3 , where S1 = {nop(adam, 0)},
S2 = {nop(eve, 0)}, and S3 = nop(t, 2) ∈ HB | t 6∈ {adam, eve} . Note that all
the atoms from Si are covered by Πi (for i = 1, 2, 3). (We do not discuss here
the (in)correctness of the program.)
Let S be Π1 , Π2 , Π3 , S1 , S2 , S3 . Consider a query A = nop(t, Y ) with a ground
t. If t = adam then only Π1 is suitable for A w.r.t. S, if t = eve then only Π2 is.
For t 6∈ {adam, eve} the suitable program is Π3 . So for a query A the pruning
due to the cuts in the program results in selecting a suitable Πi , and the obtained
csSLD-tree compatible with S. By Th. 18 the tree is complete w.r.t. S.
For a query nop(X, Y ) or nop(X, 0) only the first clause, i.e. Π1 , is used.
However Π1 is not suitable for the query (w.r.t. S), and the csSLD-tree is not
compatible with S. The tree is not complete (w.r.t. S).
4.2

The cut in the last clause.

The previous approach is based on a somehow abstract semantics in which pruning is viewed as clause selection. Now we present an approach referring directly to
Prolog with the cut. However the usage of the cut is restricted to the last clause
of a procedure. The author expects that the general case could be conveniently
studied in the context of programs with negation (because if H ← A1 , !, A2 is
11

followed by H ← A3 then the latter clause is used only if A1 fails). We consider LD-resolution, as interaction of the cut with delays introduces additional
complications.
We need to reason about the atoms selected in the derivations. So we employ
a (non-declarative) approach to reason about LD-derivations, presented in [1]. A
specification in this approach, let us call it call-success specification, is a pair
pre, post ∈ T B of sets of atoms, closed under substitution. A program is correct
w.r.t. such specification, let us say c-s-correct, when in each LD-derivation
every selected atom is from pre and each corresponding computed answer is in
post, provided that the derivation begins with an atomic query from pre. See [1]
or [10] for further explanations, and for a sufficient criterion for c-s-correctness.
By vars(E) we denote the set of variables occurring in an expression E.
For a substitution θ = {X1 /t1 , . . . , Xn /tn }, let dom(θ) = {X1 , . . . , Xn }, and
rng(θ) = vars({t1 , . . . , tn }).
Definition 22 Let S be a specification, and pre, post a call-success specification.
A ground atom A is adjustably covered by a clause C w.r.t. S and pre, post
if A is covered by C and the cut does not occur in C, or the following three
conditions hold:
1. C is H ← A1 , . . . , Ak−1 , !, Ak , . . . , An ,
2. A is covered by H ← A1 , . . . , Ak−1 w.r.t. S,
3. – for any instance Hρ ∈ pre such that A is an instance of Hρ,
– for any ground instance (A1 , . . . , Ak−1 )ρη such that A1 ρη, . . . , Ak−1 ρη ∈
post,
– A is covered by (H ← Ak , . . . , An )ρη w.r.t. S,
where dom(ρ) ⊆ vars(H), rng(ρ)∩vars(C) ⊆ vars(H), dom(ρ)∩rng(ρ) = ∅,
and dom(η) = vars((A1 , . . . , Ak−1 )ρ).
Informally, condition 3 says that A could be produced out of each “related”
answer for A1 , . . . , Ak−1 , and some answer for Ak , . . . , An specified by S. Note
that if A is adjustably covered by C w.r.t. S, pre, post, where S ⊆ post, then A
is covered by C w.r.t. S. If condition 3 holds for an Hρ then it holds for any its
instance Hρδ of which A is an instance. For a proof of this property and of the
theorem below, see Appendix.
Theorem 23. Let S be a specification, pre, post a call-success specification,
where S ⊆ post. Let T be a pruned LD-tree for a program P and an atomic
query Q, where pruning is due to the cut occurring in the last clause(s) of some
procedure(s) of P . If
– T is finite, Q ∈ pre, P is c-s-correct w.r.t. pre, post, and
– each A ∈ S is adjustably covered by a clause of P w.r.t. S and pre, post
then T is complete w.r.t. S.
Example 24. Consider a program IN and specifications:
in([ ], L).
in([H|T ], L) ← m(H, L), !, in(T, L).
12

m(E, [E|L]).
m(E, [H|L]) ← m(E, L).

S = Sm ∪ Sin , pre = prem ∪ prein , post = postm ∪ postin , where
prem = { m(u, t) ∈ T B | t is a list },
prein = { in(u, t) ∈ HB | u, t are ground lists },
postm = { m(ti , [t1 , . . . , tn ]) ∈ T B | 1 ≤ i ≤ n },
postin = { in([u1 , . . . , um ], [t1 , . . . , tn ]) ∈ HB | {u1 , . . . , um } ⊆ {t1 , . . . , tn } },
Sm = postm ∩ HB, Sin = postin .
The program is c-s-correct w.r.t. pre, post (we skip a proof). We show that each
atom A = in(u, t) ∈ Sin , where u = [u1 , . . . , um ], m > 0, is adjustably covered
by the second clause C of IN. Let C0 be in([H|T ], L) ← m(H, L). Now A is
covered by C0 w.r.t. S (A ← m(u1 , t) is a relevant ground instance of C0 ).
Take an instance in([H|T ], L)ρ ∈ pre of the head of C. The instance is
ground, and the whole Cρ is ground. So in Df. 22, ρη = ρ. If A is an instance
of (thus equal to) in([H|T ], L)ρ then in(T, L)ρ = in([u2 , . . . , um ], t) ∈ S (as
A ∈ S). Thus A is covered by (in([H|T ], L) ← in(T, L))ρ.
Thus A is adjustably covered by C. It is easy to check that all the remaining
atoms of S are covered by IN w.r.t. S, and that IN is recurrent (for |m(s, t)| = |t|,
|in(s, t)| = |s|+|t|, |t| as in Ex. 11). Thus each LD-tree for IN and a query Q ∈ pre
is finite. By Th. 23, each such tree pruned due to the cut is complete w.r.t. S.
Notice that condition 3 does not hold when non ground arguments of in are
allowed in prein , and that for such queries some answers may be pruned.

5

Discussion

Declarativeness. Without declarative ways of reasoning about correctness and
completeness of programs, logic programming would not deserve to be called a
declarative programming paradigm. The sufficient condition for proving correctness (Th. 4), that for semi-completeness of Th. 10, and those for completeness of
Prop. 8.2 and Th. 13 are declarative. However the sufficient conditions for completeness of Prop. 8.1 and 8.3 are not, as they refer to program termination, or
depend on the order of atoms in clause bodies.
Declarative completeness proofs employing Prop. 8.2 or Th. 13 imply termination, or require reasoning similar to that in termination proofs. So proving
completeness by means of semi-completeness and termination may be a reasonable compromise between declarative and non-declarative reasoning, as termination has to be shown anyway in most of practical cases.
Granularity of proofs. Note that the sufficient condition for correctness deals
with single clauses, that for semi-completeness – with procedures, and those for
completeness take into account a whole program.
Incompleteness diagnosis. There is a close relation between completeness proving
and incompleteness diagnosis [17]. As the reason of incompleteness, a diagnosis
algorithm finds an atom from S that is not covered by the program. Thus it
finds a reason for violating the sufficient conditions for semi-completeness and
completeness of Th. 10, 13.
13

Approximate specifications. We found that approximate specifications are crucial in avoiding unnecessary complications in dealing with correctness and completeness of programs (cf. Sect. 2, [10,7,9]). For instance, in the main example
of [7] (and in its simpler version in Ex. 19, 20) finding an exact specification is
not easy, and is unnecessary. The required property of the program is described
more conveniently by an approximate specification. Moreover, as this example
shows, in program development the semantics of (common predicates in) the
consecutive versions of a program may differ. What is unchanged is correctness
and completeness w.r.t. an approximate specification.
Approximate specifications in program development. This suggests a generalization of the paradigm of program development by semantics preserving program transformations [16]: it is useful and natural to use transformations which
only preserve correctness and completeness w.r.t. an approximate specification.
Approximate specifications in debugging. In declarative diagnosis [17] the programmer is required to know the exact intended semantics of the program. This
is a substantial obstacle to using declarative diagnosis in practice. Instead, an
approximate specification can be used, with the specification for correctness (respectively completeness) applied in incorrectness (incompleteness) diagnosis. See
[9] for discussion and references.
Interpretations as specifications. This work uses specifications which are interpretations. (The same kind of specifications is used, among others, in [1], and in
declarative diagnosis.) There are however properties which cannot be expressed
by such specifications [10]. For instance one cannot express that some instance of
an atomic query A should be an answer; one has to specify the actual instance(s).
Other approach is needed for such properties, possibly with specifications which
are logical theories (where axioms like ∃X. A can be used).
Applications. We want to stress the simplicity and naturalness of the sufficient
conditions for correctness (Th. 4) and semi-completeness (Th. 10, the condition
is a part of each discussed sufficient condition for completeness). Informally,
the first one says that the clauses of a program should produce only correct
conclusions, given correct premises. The other says that each ground atom that
should be produced by P can be produced by a clause of P out of atoms produced
by P . The author believes that this is a way a competent programmer reasons
about (the declarative semantics of) a logic program.
Paper [7] illustrates practical applicability of the methods presented here. It
shows a systematic construction of a non-trivial Prolog program (the SAT solver
of [13]). Starting from a formal specification, a definite clause logic program
is constructed hand in hand with proofs of its correctness, completeness, and
termination under any selection rule. The final Prolog program is obtained by
adding control to the logic program (delays and pruning SLD-trees). Adding
control preserves correctness and termination. However completeness may be
violated by pruning, and by floundering related to delays. By Th. 18, the program
14

with pruning remains complete.2 Proving non-floundering is outside of the scope
of this work. See [11] for a related analysis algorithm, applicable in this case [14].
The example shows how well “logic” could be separated from “control.” The
whole reasoning related to correctness and completeness can be done declaratively, abstracting from any operational semantics.
Future work. A natural continuation is developing completeness proof methods
for programs with negation (a first step was made in [10]), maybe also for constraint logic programming and CHR (constraint handling rules). Further examples of proofs are necessary. An interesting task is formalizing and automatizing
the proofs, a first step is formalization of specifications.
Conclusion. Reasoning about completeness of logic program has been, surprisingly, almost neglected. This paper presents a few sufficient conditions for completeness. As an intermediate step we introduced a notion of semi-completeness.
The presented methods are, to a large extent, declarative. Examples suggest that
the approach is applicable – maybe at informal level – in practice of Prolog programming. The approach is augmented by two methods of proving completeness
in presence of pruning.

Appendix
The appendix contains a proof of Th. 23 and of a property stated on p. 12. We
begin with an additional example of applying Th. 23.
Example 25. Consider a program P :
p(X, Z) ← q(X, Y ), !, r(Y, Z).

q(a, a)
q(a, a0 )
q(b, b)

r(a, c)
r(a0 , c)

and specifications
S = { p(a, c), q(a, a0 ), q(b, b), r(a, c), r(a0 , c) },
post = S ∪ {q(a, a)},
pre = { p(a, t) | t ∈ T U } ∪ { q(a, t) | t ∈ T U } ∪ { r(t, u) | t, u ∈ T U }
The program is c-s-correct w.r.t. pre, post (we skip a proof). To check that atom
p(a, c) ∈ S is adjustably covered by the first clause of P , note first that it is
covered w.r.t. S by p(a, c) ← q(a, a0 ). It is sufficient to check condition 3 of
Df. 22 for ρ = {X/a}, as p(X, Z)ρ = p(a, Z) is a most general p-atom in pre (cf.
Lemma 27 below). If q(X, Y )ρη ∈ post then η = {Y /a} or η = {Y /a0 }. Hence
r(Y, Z)ρη is r(a, Z) or r(a0 , Z). In both cases, p(a, c) ← r(Y η, c) is a ground
instance of (p(X, Z) ← r(Y, Z))ρη covering p(a, c) w.r.t. S.
2

In [7] a weaker version of Th. 18 was used, and one case of pruning was discussed
informally. A proof covering both cases of pruning is illustrated here in Ex. 20.

15

The remaining atoms of S are trivially covered by the unary clauses of P .
The LD-tree for P and Q = p(a, Z) is finite, hence the LD-tree pruned due to
the cut is complete w.r.t. S by Th. 23.
Before the proof of Th. 23. let us discuss how the cut works. We treat Prolog
programs as definite programs, the same for queries. The cut is considered as
additional control information. We however often write symbol ! in queries, to
remind the original position of the cut in a program clause.
Assume a Prolog program P , which is a logic program in which, additionally,
the cut may occur in the last clause of a procedure. Consider a pruned LD-tree
T resulting from pruning an LD-tree T0 due to the cut. The cut is involved
whenever a query Qi−1 has a child Qi :
Qi−1 = A, Q0 ,
Qi = (A1 , . . . , Ak−1 , !, Ak , . . . , An , Q0 )θi ,
where H ← A1 , . . . , Ak−1 , !, Ak , . . . , An is the clause variant used and θi is an
mgu of A and H. Note first that the cut introduced in Qi may affect only the
subtree of T0 rooted in Qi (as the clause with the cut is the last in its procedure).
The top part of the subtree of T0 rooted in Qi can be seen as the LD-tree T 0
for (A1 , . . . , Ak−1 )θi (with an instance of Ak , . . . , An , Q0 added to each query of
T 0 ). If T 0 contains no success then no pruning is performed due to the cut in
Qi . Also, no pruning happens when there is an infinite branch in T 0 preceding
all the success branches. Otherwise, pruning is performed and all the successes,
but one, are pruned away. More precisely, exactly one path remains not pruned,
out of all the paths in T0 beginning in Qi of the form
Qi = (A1 , . . . , Ak−1 , !, Ak , . . . , An , Q0 )θi ,
Qi+1 = (. . . , A2 , . . . , Ak−1 , !, Ak , . . . , An , Q0 )θi θi+1 ,
···
Qj−1 = (A0 , !, Ak , . . . , An , Q0 )θi · · · θj−1 ,
Qj = (Ak , . . . , An , Q0 )θi · · · θj ,
(where each query Qi , . . . , Qj−1 contains more atoms than Qj does).
Strictly speaking, it was assumed here that no cut is introduced in any query
Ql (i < l < j). To deal with such extra cuts, notice that the same reasoning
applies recursively (i.e. by induction on the number of cuts introduced within
Qi , . . . , Qj ). So we showed that:
If the LD-tree T 0 for (A1 , . . . , Ak−1 )θi contains a successful branch,
not preceded by an infinite branch, then the pruned tree T contains
a path Qi−1 , Qi , . . . , (Ak , . . . , An , Q0 )θi · · · θj .
Otherwise no pruning occurs due to the cut introduced in Qi . (The
cut is not executed. No success leaf is a descendant of Qi in T .)

(13)

Proof (of Th. 23). As each atom of S is covered by P w.r.t. S, P is semi-complete
w.r.t. S by Th. 10. Consider the LD-tree T0 for P and Q, and the finite pruned
16

LD-tree T . Without loss of generality we can assume that the employed mgu’s
are idempotent and relevant [1, p. 37–38].
Consider a ground instance Qθ of Q such that S |= Qθ. In the proof of Th. 10
(cf. [8, Th. 4]), out of a ground successful derivation D for Qθ a lift [6, Df. 5.35]
was constructed, which was a branch of the tree for Q. Each atom occurring in D
was from S. Here such a ground derivation may not exist. Instead we construct
a lift (for a superset of P ) which consists of some nodes of a successful branch
of T . Roughly speaking, a fragment of computation involving the cut will be
represented by three nodes in the lift.
We first prove the following property, which is the inductive step of the main
proof.
If Qi−1 = A, Q0 is a node in the pruned tree T , with a ground instance
Qi−1 σi−1 such that S |= Qi−1 σi−1 then there exists in T a descendant
Qj of Qi−1 with a ground instance Qj σj , such that S |= Qj σj .
Moreover, Qi−1 , Qj are the first and the last query of an LD-derivation
Di,j (for a P 0 ⊇ P ) which is a lift of an unrestricted derivation [6,
Df. 5.35] beginning with Qi−1 σi−1 and ending with Qj σj . Also, the resultant of Di,j is the same as the resultant of the derivation Qi−1 , Qi , . . . , Qj
for P , which is a path in T between Qi−1 and Qj .
If the selected atom Aσi−1 of Qi−1 σi−1 is covered by a clause without the cut
then the proof follows that of Th. 10 [8, Th. 4]; Qj is a child of Qi−1 in T .
The main part of this proof deals with the case when a ground instance
Aσi−1 of the selected atom is adjustably covered by a clause C = H ←
A1 , . . . , Ak−1 , !, Ak , . . . , An (and thus covered by C). Without loss of generality we may assume that C is a clause variant used in the resolution step. Let
Qi−1 = A, Q0 . Then A ∈ pre, A is unifiable with H with an mgu θi , Hθi ∈ pre,
atom Aσi−1 is an instance of Hθi , and Qi = (A1 , . . . , Ak−1 , !, Ak , . . . , An , Q0 )θi
is a child of Qi−1 (in T0 and in T ).
Some ground instance of Qi consists of atoms from S; hence S |=
∃(A1 , . . . , Ak−1 )θi . As P is semi-complete w.r.t. S, the LD-tree T 0 for
(A1 , . . . , Ak−1 )θi has an infinite, or a successful branch. Assume that each successful branch of T 0 is preceded by an infinite one. Then, by (13), the cut introduced in Qi is not executed, and T contains an infinite branch, contradiction.
So T 0 has a successful branch not preceded by an infinite one. Hence, by (13), T
contains a path, starting in Qi , of the form
Qi = (A1 , . . . , Ak−1 , !, Ak , . . . , An , Q0 )θi ,
Qi+1 = (. . . , A2 , . . . , Ak−1 , !, Ak , . . . , An , Q0 )θi θi+1 ,
···
Qj = (Ak , . . . , An , Q0 )θi · · · θj ,
where θi+1 , . . . , θj are the used mgu’s, and each query Qi , . . . , Qj−1 contains
more atoms than Qj does.
Let φ = θi+1 · · · θj . We have A1 θi φ, . . . , Ak−1 θi φ ∈ post (hence all ground
instances of A1 θi φ, . . . , Ak−1 θi φ are in post). To apply condition 3 of Df. 22,
17

take ρ = θi C (the restriction of θi to the variables of C). Then dom(ρ) ⊆
vars(H), rng(ρ) ∩ vars(C) ⊆ vars(H) (as θi is a relevant unifier of A and H),
dom(ρ)∩rng(ρ) = ∅ (as θi is idempotent) and, obviously, Cθi = Cρ. By condition
3 of Df. 22 (with η = φ (A1 ,...,Ak−1 )ρ ), Aσi−1 is covered by (H ← Ak , . . . , An )ρη,
which is (H ← Ak , . . . , An )θi φ. So Aσi−1 = Hθi φσ 0 and Ak θi φσ 0 , . . . , An θi φσ 0 ∈
S, for some σ 0 . Let ψ = θi φσ 0 .
Let us now have a different look at the derivation Qi−1 , . . . , Qj . Let us introduce a new predicate symbol p and and treat A1 , . . . , Ak−1 as terms. Consider
Qi−1 = A, Q0
Q0i = (p(A1 , . . . , Ak−1 ), !, Ak , . . . , An , Q0 )θi ,
Qj = (Ak , . . . , An , Q0 )θi φ.
It is a derivation for a program {C 0 , C 00 }, where
C 0 = H ← p(A1 , . . . , Ak−1 ), !, Ak , . . . , An ,
C 00 = p(A1 , . . . , Ak−1 )θi φ.
The mgu’s used are θi and φ. We construct an unrestricted derivation Γ for
{C 0 , C 00 } [6, Df. 5.9], so that derivation ∆ = Qi−1 , Qi , Qj is a lift [6, Df. 5.35]
of Γ . Γ consists of ground queries R1 , R2 , R3 , where
R1 = Qi−1 σi−1 = (A, Q0 )σi−1 ,
R2 = (p(A1 , . . . , Ak−1 ), !, Ak , . . . , An )ψ, Q0 σi−1 ,
R3 = (Ak , . . . , An )ψ, Q0 σi−1 .
So Γ is an unrestricted derivation, where C 0 , C 00 are the applied clauses.
Hence ∆ is a lift of Γ . By the lifting theorem [6, Th. 5.37], the resultant R3 → R1
of Γ is an instance of the resultant Qj → Qi−1 θi φ of ∆. The latter is also
the resultant of the original derivation Qi−1 , Qi , Qi+1 . . . , Qj for P . Note that
S |= R3 . So R3 is the required ground instance of Qj . This completes the proof
of the inductive step.
By induction we obtain that in T there exists a successful (as T is finite)
branch Q, . . . , 2 with a subsequence of nodes ∆0 = Q, Qj1 . . . , Qjl , 2 (where
0 < j1 < · · · < jl ) which is a lift of a ground successful unrestricted derivation
starting with Qθ (for some superset of the program P ). The resultants (i.e.
the answers) for both successful derivations are the same. Hence, by the lifting
theorem [6, Th. 5.37] Qθ is an instance of the answer of ∆0 , hence of an answer
of T .
2
It remains to show that if condition 3 of Df. 22 holds for an Hρ then it holds
for all its instances (for which A is an instance)
Lemma 26. Let C be a clause H ← A1 , . . . , Ak−1 , !, Ak , . . . , An (0 ≤ k ≤ n).
→
−
→
−
Let A be A1 , . . . , Ak−1 . Let A, ρ, η, Hρ i A ρη be as in condition 3 of Df. 22.
The following conditions (1) and (2) are equivalent.
(1) A is covered by (H ← Ak , . . . , An )ρη w.r.t. S.
18

(2) There exists a successful LD-derivation for A using in its consecutive steps
the clauses C, A1 ρη, . . . , Ak−1 ρη, and then some atoms from S.
Note that in (2) all the clauses used in the derivation, except C, are ground.
Proof. (1) ⇒ (2): (1) implies that A is covered by a ground clause (H ←
Ak , . . . , An )ρησ. Construct an LD-derivation D for A, using first clause Cρησ
and then the clauses as in (2). Its lift is a required derivation.
(2) ⇒ (1): Take a derivation as in (2):
A
(A1 , . . . , An )θ1
...
(Ak , . . . , An )θ1 · · · θk
...
An θ 1 · · · θ n
2
with mgu’s θ1 , . . . , θn+1 , which are ground substitutions. We have A = Hθ1 =
Hθ1 · · · θn+1 , and the ground clauses used in the derivation are Ai θ1 · · · θi+1 =
→
−
→
−
Ai θ1 · · · θn+1 (i = 1, . . . , n). Then A ρη = A θ1 · · · θn+1 and Ai θ1 · · · θn+1 ∈ S for
i = k, . . . , n.
Now A = Hρδ for some ground substitution δ with dom(δ) = vars(Hρ).
So θ1 = (ρδ) vars(H) , as dom(θ1 ) = vars(H). Note that dom(δ) ∩ vars(C) ⊆
vars(H) (as rng(ρ)∩vars(C) ⊆ vars(H)). Hence θ1 = (ρδ) vars(H) = (ρδ) vars(C) ,
→
−
→
−
→
−
→
−
and thus Cθ1 = Cρδ. In particular, A θ1 = A ρδ. So A ρη = A θ1 · · · θn+1 =
→
−
→
−
A ρδθ2 · · · θn+1 . Thus η = (δθ2 · · · θn+1 ) →
− (as dom(η) = vars( A ρ)).
Aρ
Let σ = (δθ2 · · · θn+1 ) \ η. As δ and σ are ground and with disjoint domains,
δθ2 · · · θn+1 = η ∪ σ = ησ. Hence Cθ1 · · · θn+1 = Cρδθ2 · · · θn+1 = Cρησ (as
Cθ1 = Cρδ). So Hρησ = Hθ1 · · · θn+1 = A and Ai ρησ = Ai θ1 · · · θn+1 ∈ S, for
i = k, . . . , n. Hence A is covered by (H ← Ak , . . . , An )ρη w.r.t. S.
2
Lemma 27. If condition 3 of Df. 22 holds for an atom Hρ ∈ pre then it holds
for any its instance Hρ0 such that A is an instance of Hρ0 , and ρ0 satisfies
the requirements of condition 3 (i.e. dom(ρ0 ) ⊆ vars(H), rng(ρ0 ) ∩ vars(C) ⊆
vars(H), dom(ρ0 ) ∩ rng(ρ0 ) = ∅).
→
−
→
−
→
−
Proof. Let A be A1 , . . . , Ak−1 . We first show that A ρ0 is an instance of A ρ. For
0
0
some δ with dom(δ) ⊆ vars(Hρ), we have Hρ = Hρδ, so ρ = (ρδ) H . Consider
a variable X from C. There are two cases:
1. X ∈ vars(H), thus Xρ0 = Xρδ.
2. X 6∈ vars(H). So X 6∈ dom(ρ), as dom(ρ) ⊆ vars(H). From dom(δ) ⊆
vars(H) ∪ rng(ρ) it follows that dom(δ) ∩ vars(C) ⊆ vars(H) (as rng(ρ) ∩
vars(C) ⊆ vars(H)). So X 6∈ dom(δ). Hence Xρδ = X and Xρ0 = Xρδ.
→
−
→
−
We showed that ρ0 = (ρδ) C . So A ρ0 = A ρδ. Then each ground instance
→
− 0 0 →
−
→
− →
−
A ρ η of A ρ0 such that A1 ρ0 η 0 , . . . , Ak−1 ρ0 η 0 ∈ post is an instance of A ρ ( A ρ0 η 0 =
→
−
→
−
− )η 0 ).
A ρδη 0 = A ρη where η = (δ →
Aρ
19

Assume that condition 3 holds for Hρ. Then for each ground instance as
→
−
above where each atom of A ρη is in post, atom A is covered w.r.t. S by (H ←
Ak , . . . , An )ρη. By Lemma 26 there exists a successful LD-derivation for A using
in its consecutive steps the clauses C, A1 ρη, . . . , Ak−1 ρη, and then some atoms
from S. As Ai ρη = Ai ρ0 η 0 for i = 1, . . . , k − 1, by Lemma 26 used in the opposite
direction, A is covered by (H ← Ak , . . . , An )ρ0 η 0 .
2

References
1. K. R. Apt. From Logic Programming to Prolog. International Series in Computer
Science. Prentice-Hall, 1997.
2. K. L. Clark. Predicate logic as computational formalism. Technical Report 79/59,
Imperial College, London, December 1979.
3. P. Deransart and J. Maluszyński. A grammatical view of logic programming. The
MIT Press, 1993.
4. Y. Deville. Logic Programming: Systematic Program Development. AddisonWesley, 1990.
5. Y. Deville and K.-K. Lau. Logic program synthesis. J. Log. Program., 19/20:321–
350, 1994.
6. K. Doets. From Logic to Logic Programming. The MIT Press, Cambridge, MA,
1994.
7. W. Drabent. Logic + control: An example. In Agostino Dovier and Vı́tor Santos
Costa, editors, Technical Communications of ICLP’12, volume 17 of LIPIcs, pages
301–311, 2012. http://drops.dagstuhl.de/opus/volltexte/2012/3631.
8. W. Drabent. Logic + control: An example of program construction. CoRR, arXiv:
1110.4978 [cs.LO], 2012. http://arxiv.org/abs/1110.4978.
9. W. Drabent. Correctness and completeness of logic programs. Technical report,
IPI PAN, 2014. Forthcoming.
10. W. Drabent and M. Milkowska. Proving correctness and completeness of normal
programs – a declarative approach. TPLP, 5(6):669–711, 2005.
11. S. Genaim and A. King. Inferring non-suspension conditions for logic programs
with dynamic scheduling. ACM Trans. Comput. Log., 9(3), 2008.
12. C. J. Hogger. Introduction to Logic Programming. Academic Press, London, 1984.
13. Jacob M. Howe and Andy King. A pearl on SAT and SMT solving in Prolog.
Theor. Comput. Sci., 435:43–55, 2012.
14. A. King. Personal communication. March 2012.
15. Robert A. Kowalski. The relation between logic programming and logic specification. Phil. Trans. R. Soc. Lond. A, 312:345–361, 1984.
16. Alberto Pettorossi and Maurizio Proietti. Transformation of logic programs: Foundations and techniques. J. Log. Program., 19/20:261–320, 1994.
17. E. Shapiro. Algorithmic Program Debugging. The MIT Press, 1983.
18. Robert F. Stärk. The theoretical foundations of LPTP (a logic program theorem
prover). J. Log. Program., 36(3):241–269, 1998.
19. L. Sterling and E. Shapiro. The Art of Prolog. The MIT Press, 2 edition, 1994.

20

