Logic Programming with General Clauses and Defaults Based on Model Elimination

1. INTRODUCTION

This paper addresses the foundations of a class of logic programming systems with the expressive power of full first-order logic and a non-monotonic component. Systems in this class provide a direct generalization of pure Prolog and they can be implemented using the · same technology as Prolog processors. The discussion centers on the underlying refutation method, which is an extended version of weak model elimination (Loveland [1978]) enhanced with defaults (Reiter [ 1980]).

The first contribution of this paper consists in defining an adaptation of weak model elimination ( WME) that is sound and complete with respect to computing answers when the logic programs and queries are expressed by sets of generic clauses. The proofs of these two results are far more complex than the corre­ sponding results for SLD-resolution (see Lloyd [ 1984]), the basis of Prolog systems. The question of computing just definite answers is also settled, using a new result about refutations in WME.

Negation within the scope of WME has the classical meaning. The second contribution of this paper then refers to extending WME with defaults to capture answer A to Q over P is more general than an answer B to Q over P iff A logically implies B. We let False be an answer simply because it will be the most general answer to any query over an inconsistent program.

For example, the following set of clauses is a program, that we call DIC:

1. program(a,fortran)
2. program(b,pascal)
3. program(c,fortran) program(c,pascal)
4. calls(a,b)
5. calls(b,c)
6. -. calls(x,y) depends(x,y)
7. -. calls(x,z) -. depends(z,y) depends(x,y)

Thus, clause (3) indicates that c is an ordinary program written in fortran or pascal and clauses (6) and (7) indicate that x depends on y if x calls y direct or transitively. The formula below is a query, that we call DEP[a]:

(depends(a,x) 11. program(x,pascal)) v (depends(a,x) 11. program(x,fortran))

It asks for a program written in fortran or pascal that the program a depends on. An answer A to DEP[a] over DIC would be:

depends(a,b) 11. program(b,pascal)

Indeed, the conjunction in A is an instance of the first conjunction in DEP[a]. It is in fact a correct answer since DIC logically implies VA. A second correct answer to DEP[a] over DIC would be:

(depends(a,c) 11. program(c,fortran)) v (depends(a,c) 11. program(c,pascal))

3. COMPUTING ANSWERS WITH WME

3.1 Weak Model Elimination

To achieve completeness, the inference rules of WME sometimes maintain the resolved literals within the derived clauses and keep the literals (resolved or not) ordered within a clause. To distinguish these extended clauses from the ordinary clauses, they will be called chains. Moreover, resolved literals in a chain will be enclosed within brackets.

More precisely, a resolved literal (or a R-literal) is an expression of the form [L], where L is a literal. An element is a literal or a R-literal. An elementary chain is any sequence of literals and a chain is any sequence of elements. The symbol D will denote the empty chain, which is elementary by definition. Each chain C represents, by convention, the universal closure of the disjunction of its literals, in the sense that any structure for the first-order alphabet in question satis­ fies C if and only if it satisfies the formula that C represents. Hence, the R-literals of a chain do not influence its semantics. From these definitions, it should be clear that elementary chains and clauses are one and the same concept and will be used inter­ changeably in this text.

The next definitions are basic for the inference rules of the method and assume familiarity with the notion of unification. In what follows, B'B" denotes the concat­ enation of two chains B' and B" and Ill indicates the atom of a literal L. Two literals L' and L" can be can­ celled by a substitution 8 if and only if 8 is a most general unifier (m.g.u.) of {IL'I,IL"I} and L'8 and L"8 are complementary. ·

Let A' be a chain and let A" be an elementary chain. Let P be a renaming of the variables of A" such that A"P has variables distinct from those of A'. Let L' be the leftmost element of A' and suppose that L' is a literal. A chain A is an extension of A' by A" if and only if there exists a literal L" of A" and a substitution 8 such that L' and L"P can be cancelled by 8 and A= B"B', where B" is the chain A"P8 with the literal L"P8 removed and B' is a chain A'8 with the literal L'8 replaced by [L'8].

Let A' be a chain. Let L' be the leftmost element of A' and suppose that L' is a literal. A chain A is a reduction of A' if and only if there exists a R-literal [M'] of A' and a substitution 8 such that L' and M' can be cancelled by 8 and A is A'8 with the literal L'8 removed.

A chain A is a contraction of a chain A' if and only if A is the chain obtained by removing from A' all R-literals that are to the left of the leftmost literal. If A has only R-literals, the result becomes the empty chain.

A chain A is a full extension of A' by A" if and only if A is the contraction of an extension of A' by A". A chain A is a full reduction of a chain A' if and only if A is the contraction of a reduction of A'.

The weak model elimination method, WME, works with the class of all sets of first-order chains, it has no axioms and two inference rules, full extension and full contraction, defmed as follows:

Full Extension:

if A' and A" are chains and A is a full extension of A' by A" then derive A from A' and A".

Full Reduction:

if A' is chain and A is a full reduction of A' then derive A from A'.

A WM £-deduction of a chain C from a set S of ele­ mentary chains is any fmite sequence of chains E = (E 1 , ... ,En) such that C is the last chain of E, there is i ~ n such that E 1 , ... ,E;, the prefix of E, consists of chains in S and, for each jE[i + l,n], Ej is derived from Ej_ 1 , the parent chain of Ej, by full reduction or full extension, in the latter case using an auxiliary chain from the prefix of E. The chain E; is called the initial chain of E. A WM £-refutation from a set of elemen­ tary chains S is a WME-deduction of the empty chain from S .

The W ME method defmed above is slightly different from the original version of Loveland [ 1978] but the results therein can be easily adapted to establish that W ME is refutationally sound and complete.

3.2 Computing Answers with WME

Given a WME-refutation R from the elementary chains in a program P and in the clausal representation of the negation of the existential closure of a query Q, denoted by CL(-... 3Q), it is possible to show that the substitutions applied to the free variables of chains in CL(-... 3Q) during the construction of R induce a correct answer to Q over P. However, to recover such substitutions is not exactly simple since CL(-... 3Q) may possibly contain more than one chain, that may also be reused in R. This section then redefmes the notion of chain and the inference rules of W ME to register such substitutions, using answer literals (Green [ 1969]).

An activated chain is a pair of the form (C,L), where C is a chain and L is a set of literals. The activation of P is the set activate(P) consisting of the activated chains (C,0) , where CEP. The activation of a query Q of the form Q 1 v .. . vOn is the set activate( Q) of activated chains ( -O; ,{r;(X;)} ), i = l, ... ,n, where -0;, by con­ vention, is the chain consisting of the complement of the literals of 0; , · x i is a list of the variables of 0; and r; is a predicate symbol, not in the original alphabet, whose arity is equal to the length of X;. The literal r;(X;) is the answer literal for 0; in the activation of Q.

The activation of a query Q therefore produces a clausal representation of the negation of the existential closure of Q, with each elementary chain armotated with an answer literal whose function will be to record the substitutions applied to the variables of the chain. But, to effect this recording, the inference rules of WME had to be modified as follows.

An activated chain (A,L) is a full activated reduction of an activated chain (A',L') if and only if A is a full reduction of A' with m.g.u. 9 and L = L'9 . An acti­ vated chain (A,L) is a full activated extension of (A',L') by an elementary activated chain (A",L") if and only if A is a full extension of A' by A", with m.g.u. 9 and renaming P of A", and L = L'8 U L"P8 .

An answer A to Q over P is WM £-computed if and only if there is an activated WME-refutation R from activate(P) U activate(Q) such that either R terminates in ( 0 ,0), in which case A must be equal to False, or R terminates in ( 0 ,L), with L * 0, and A is a disjunc­ tion of all conjuncts B such that there IS ( -O;,{r;(x;)} )Eactivate(Q) and r;(t)EL such that B is equal to 0;9, where e = {x;/t} .

The following example illustrates how the method computes a defmite answer to an indefmite query. Consider again the program DIC and the query DEP[a] introduced in section 2. An activated WME-refutation from the set of chains in the acti­ vation of DIC (chains 1 to 7) and the activation of DEP[a] (chains 8 and 9) is:

1. (program(a,fortran), 0)
2. (program(b,pascal), 0)
3. (program(c,fortran) program(c,pascal), 0)
4. (calls(a,b), 0)
5. (calls(b,c), 0)
6. (-... calls(xJI) depends(xJI), 0)
7. (-... calls(x,z) -... depends(zJI) depends(xJI), 0)
8. (-... depends(a,u) -... program(u,fortran), {r 1 (u)})
9. (-... depends(a,v) -... program(v,pascal), {r 2 (v)})
10. (-... calls(aJ') [-... depends(aJ!)] -... program(y,pascal), {r 2 (y)}) (from 9 and 6)
11. (-... program(b,pascal), {r 2 (b)}) (from 10 and 4)
12. (0, {r 2 (b)}) (from 11 and 2)

Hence, A= depends(a,b) 1\ program(b,pascal) is a WME-computed answer to DEP[a] over DIC since r2(b) in (12) indicates that the variable v of the chain in (9) was substituted by b.

The WME method, modified as described above, is sound and complete for computing answers in the fol­ lowing sense:

Theorem 1: (Soundness and Completeness Theorem)

Let P be a program and Q be a query.

• (a) Every WME-computed answer to Q over P is correct.
• (b) Given any correct answer to Q over P, there is a WME-computed answer which is more general.

We conclude this section with another variation of weak model elimination that computes only defmite answers.

Let S be a set of activated elementary chains and T be a subset of S. We say that an activated WME-refutation R from S has initial support from T iff the initial activated chain of R is in T and no acti­ vated chain in T is ever used as an auxiliary chain in derivations in R.

Let Q be a query to a program P. An answer A to Q over P is WM £-computed with initial support from Q iff there is an activated WME-refutation R from acti­ vate(P) U activate(Q), with initial support from activate(Q), that computes A. Note that, since just one chain from activate(Q) is used in R, A is a defmite answer. In fact, we can prove that:

• Theorem 2: (Soundness and Completeness Theorem for Defmite Answers)

Let P be a program and Q be a query.

• (a) Let A be an answer to Q over P that is WME-computed with initial support from Q. Then, A is defmite and correct.
• (b) Given any defmite correct answer A to Q over P, there is a defmite answer B to Q over P such that B is WME-computed with initial support from Q and B is more general than A.

4. EXTENDING WME WITH DEFAULTS

4.1 Clausal Defaults

A clausal default is any expression of the form "A:C", where the prerequisite A of the default is a conjunc­ tion of literals and the consequent C of the default is an elementary chain. A clausal default theory is a pair

~ = (P,D), where P is a fmite set of elementary chains and D is a fmite set of clausal defaults. We will denote by consequent(D) the set of the consequents of all defaults in D. We also accept ":C" as a clausal default .

The clausal default "A:C" should be understood as a convenient way of expressing the open normal default

A:~F , in the notation of Reiter [ 1980], where F is a disJunction of the literals in the clause C. Therefore, since we will limit ourselves to clausal defaults, we will be concerned with a particular case of open normal defaults.

The semantics for clausal default theories follows from the concept of extensions for open default theories. Then, given a clausal default theory ~ = (P,D), a clausal default "A:C" in D should be interpreted as a generator of the set of def~ults "A9:C9", for all substi­ tutions 9 of the variables in A and C by terms of the Herbrand universe for the current alphabet. The clausal default "A8:C8" therefore reads: C8 can be assumed 'by default" if the prerequisite A8 is believed and ce is consistent with the beliefs.

Let~= (P,D) be a clausal default theory and let Q be a disjunction of conjunctions of literals. Let CL(....., 3Q) again denote a clausal representation of the negation of the existential closure of Q. Intuitively, a refutation with defaults from ~ and Q is a sequence of WME-refutations . such that the first ts a WME-refutation from the chains m P U CL(....., 3Q) U consequent(D) with initial chain m CL(....., 3Q) and, after the first, each WME-refutation intends to refute the negation of the conjunction of the prerequisites of the defaults used on the preceding WME-refutation, with the appropriate substitutions, from the chains in P U consequent(D) (but not in CL(....., 3Q)). The sequence should also satisfy a global consistency test, verifying if the use of the defaults is acceptable.

To record the substitutions affecting each use of each default in each WME-refutation in the sequence, we will use default literals in the same way we used answer literals for computing answers. Hence, the indexing of~= (P,D) is the set of pairs of the form (Cj,0), where CiEP, or the form (Ci,{oj(xi)}), for each default "Ai :C( in D, where xi is a list of the variables occurring in Ai and Ci and oi is a new predicative symbol whose arity is the length of Xj · The indexing of Q consists of the set of pairs (Cj,0), where CiECL(....., 3Q). Similarly to the answer literals, Oj(Xj) will record the substitutions applied to the variables of the default "Ai:C( For that purpose, the inference rules of WME and the notions of WME-deduction and WME-refutation are also modified to account for default literals similarly to what was described in section 3 for answer literals.

Let R be an indexed WME-refutation from the chains in the indexing of ~ and Q. Suppose that R termi­ nates in ( D ,S) . A default 'Jf is returned by R iff there is a pair (Cj ,{Oj(Xj)}) in the indexing of ~. corre­ sponding to some default "Ai:Ci" in D, and there exists a literal of the form Oj(t) in S such that 'Jf can be written as "Ai8:Ci8", where 8 = {xi;t}.

Let "Ai :Ct be a default in D and (Cj,{Oj(Xj)}) be the corresponding pair in the indexing of~- This default is fired in R iff exists an indexed chain in R derived by indexed full extension with (Cj,{Oj(Xj)}) as auxiliary chain. Then, each default "Ai :C( ftred in R, as well as each default corresponding to a default literal in the initial chain of R, if any, generates a descendent default in the set of defaults returned by R.

A WM £-refutation sequence with defaults from ~=(P , D) and Q is a ftnite sequence R=(R 0 , ... ,Rk) of indexed WME-refutations such that:

1. R 0 is an indexed WME-refutation from the indexing of ~ and the indexing of Q, with initial chain in indexing of Q;
2. for 0 ,:5; i ,:5; k, let Di be the set of defaults returned by Ri , Mi be the set of default. literals corre­ sponding to the defaults in Di, 0( 1 ) be the set of defaults in Di which are the descendents of the defaults ftred in Ri and Bi be the chain repres­ enting the negation of the conjunction of the pre­ requisites of all defaults in o(i). Then:
3. For 1 ,:5; i ,:5; k, Ri must be an indexed WME-refutation, with initial support {(Bi-1 ·Mi-1)}, from the indexed chains in the indexing of~ U {(Bi-1·Mi-1)};
4. o(k) = 0;
5. (Consistency Te.rt). Let C be the set of the consequents of all defaults occurring in Dk. Then, there is a substitution 8 of the variables occurring in C by ground terms of Herbrand universe over the current alphabet such that p u ce is satisftable.

It follows from the results in Reiter [ 1980) and from the soundeness and completeness theorem for computing deftnite answers that the WME method, adapted to account for clausal defaults as described above, is refutationally correct and complete.

4.2. Computing Answers with Defaults

A program with defaults is a pair~= (P,D), where Pis a ftnite set of elementary chains and D is a ftnite set of clausal defaults. The notions of query and answer are not modifted. The notion of correct answer is now based on the notion of extensions of default theories.

The computation of answers now combines the two notions described in sections 3.2 and 4.1: activation and indexing. Then, the inference rules now work with triples of the form (C,L,M), where C is a chain, L is a set of answer literals for computing answers of a query, following the description in the section 3.2, and M is a set of default literals for monitoring the defaults used in a refutation, as described in section 4.2.

The defmition of the WME-refutation with defaults immediately induces the following notion of computed answer. Let ~ = ( P ,D) be a program with defaults and Q be a query to ~- An answer A to Q over ~ is WM £-computed by defaults iff there exists a WME-refutation with defaults R from the activation and indexing of ~ and Q such that the last refutation in R terminates with ( D ,S,E), the consistency test for R uses the substitution 8 and either S = 0, in which case A must be equal to False, or S * 0 and A is a disjunction of all conjuncts B such that there is ( -Qi,{ri(xi)},0) in the activation and indexing of Q and there is ri(t)ES such that B is equal to Qiy8, where y = {xj/1}.

This defmition is not reasonable, though, because it admits answers with arbitrary instanciations, coming from the substitution e generated for the consistency test. On the other hand, by the semantics itself of open defaults, it is not possible to abandon such sub­ stitution under the risk of invalidating the correctness of WME-refutation sequences with defaults. For example, let ~ = (P,D) be a program, where P = {bird(z), --. fly(pengu in), --.fly( ostrich), yellow(canary)} and D = {bird(y):fly(y)}. Consider the query Q = fly(x). Consider the WME-refutation sequence with defaults R = (R 0 ,R1 ), from ~ and Q, constructed as follows. First, R 0 is an indexed and activated WME-refutation from the activation and indexing of L\ and Q:

1. (fly(y),0,{8(y)}) (from ~)
2. ( -.fly(x),{r(x)},0) (from Q)

0.3 (D,{r(x)},{o(x)}) (from 0.2 by 0.1)

Note that R 0 returns the default "bird(x) :fly(x)". Hence, R 1 must be an indexed and activated WME-refutation from the chains in the indexing and activation of ~ and the chain representing the negation of the prerequisite of "bird(x) : fly(x)" (the chain (1.2) below):

1. (bird(z),0,0) (from ~)
2. (D,{r(x)},{o(x)}) (from 1.2 by 1.1)

1.2 (--. bird(x),{r(x)},{o(x)}) (from the negation of the prerequisite)

Note that the chain in 1.2 carries on the set of answer literals and the set of default literals from the chain 0.3. This is necessary to correctly compute answers.-

By the definition of WME-refutation sequence with defaults, we must also test the consistency of the set E {bird(z), -.fly(penguin), -.fly(ostrich), yellow(canary)} U {fly(x)9}, for some substitution e of X by a term of the Herbrand universe of the alphabet in question. Indeed, by taking 9 = {x/canary}, the set E becomes consistent. Hence, fly(canary) is the answer WME-computed by the ref­ utation R, for this choice of 9.

Note that the choice of 9 is entirely arbitrary. On the other hand, it is not possible to ignore e' since the set {bird(z), -.fly(penguin), -.fly(ostrich), yellow(canary)} U {fly(x)}, is not satisfiable. Intu­ itively, the default in D cannot be fired for a substi­ tution of x by, for example, penguin.

To solve the above dilemma, we propose to always base the consistency test on a class of substitutions that change each variable by a new constant not in the original language, whose semantics would be "the typical individual such that ... ". In the current example, we introduce the new constant Po, under­ stood as "the typical bird". Consider again the WME-refutation with defaults R, except that the sub­ stitution of the consistency test is now, by definition, 9 = {x/po}· Since, for this choice of 9, the set {bird(z), --. fly(pengu in), --.fly( ostrich), yellow(canary)} U {fly(x)9}, is consistent, we have that fly(po) is the new computed answer by the WME-refutation R. Intuitively, this answer indicates that "the typical bird" flies. Note that the introduction of Po is similar to the Skolemization of the formula 3x(fly(x)), except for the intuitive interpretation of the Skolem constant introduced.

Using the idea of "typical individuals" we can extend our concepts to consider answers that, in addition to indicating the appropriate substitutions as before, pos­ sibly including "typical individuals", point out some "atypical individuals" or even all "atypical individuals".

5. CONCLUSIONS

Weak model elimination offers an interesting alterna­ tive for the development of logic programming systems since it works with classes of programs and queries which are more general than those commonly consid­ ered. Section 3 established soundness and complete­ ness results for computing answers. Section 4 extended these results to a special class of defaults. In this case, the notion of answer must be appropriately revised to include the concept of "typical individual" thus avoiding arbitrary components.