6.4 A normal rulebase goal interpreter

The purpose of this section is to develop a program (an interpreter) to compute goals for normal rulebases. Normal rules, or clauses, were introduced in the previous section, and will be reviewed presently. The program will be based upon the style of interpreter discussed in Section 6.2, so it might be a good idea to review that section before wading into the current one.

Normal rulebases

We repeat here the definition of a normal rule, or clause, from the previous section. A normal rule has one of the following forms ...
A1 | A2 | ... | Am :- B1, B2, ... Bn .
where each Ai and each Bj are positive predicate terms and where m,n >= 0, but not both m = 0 and n = 0. A positive predicate term is one like p(X,Y), whereas the predicate expression ~p(X,Y) is considered as negative.

In a manner consistent with the translation from wffs to normal clauses of the previous section, such a normal clause is intended to say that either A1 or A2or ... Am is the case provided that each of B1 and B2 and ... and Bn is the case.

When m = 0 (and consequently n >= 1) the convention will be to write the normal clause in the "denial" form

false :- B1, B2, ... Bn .
where false is a special reserved term that can only be used in this context. When n = 0 (and consequently m >= 1) the convention will be to write the normal rule in the "state" form
A1 | A2 | ... | Am .
The "denial" form is intended to say that B1, B2, ..., Bn cannot all be true together. The "state" form is intended to say that at least one of A1, A2, ..., Am is true.

As with Prolog clauses, a normal clause has a head (to left of ':-') and a body (to the right of ':-'). The special false head is equivalent to an empty clause head.

A normal rulebase is a finite collection of normal rules.  It is common to also refer to a rulebase as a (logic) program.

A Prolog program is a special case of a normal rulebase: For Prolog, the head of each clause must have only one disjunct, and Prolog programs cannot have denial clauses.

Example R1. Consider the following normal rulebase.

p(f(X)) | q(Y) :- r(X,Y).
r(X,Y) :- s(X), t(Y).
false :- q(b), s(a).
Example R2. Another normal rulebase ...
a(X) | b(X) :- c(X).
d(X) :- a(X).
d(X) :- b(X).
c(1) | c(2).

Goals for normal rulebases

Suppose that R is a normal rulebase. A state goal for R has a disjunctive form

    Q1 | Q2 | ...| Qn.

where n >= 1 and each Qi is either a positive or negative predicate term. Each Qi must be expressed in the same language as R. That is, only predicate symbols, constant symbols and function symbols from R, and arbitrary variables, may be used to form each Qi. A normal goal has the form

    G1, G2, ..., Gk.

where k >= 1 and each Gj is a state goal. A normal goal is suppose to represent a conjunction of state goals.

As an example, for the rulebase R1, the following are state goals:

p(X) | ~q(f(Y).
The first state goal corresponds to asking the question whether p(f(a)) is true. The second corresponds to asking the question whether either p(X) or ~q(f(Y)), for some Y, is true. The following are normal goals
p(a), q(X), (r(a)|s(b)).
The first of these corresponds to asking the question of whether all three of p(a), q(X), for some X, and either r(a) or s(b), is true. The second corresponds to asking whether r(X,Y), for some X and Y, is true.

Prolog goals are a special case of normal goals: For Prolog, no disjunctions are allowed in goals and no negation (~) is allowed.

Interpretation of normal rulebases

The theoretical semantics of normal rulebases should give a precise definition of which normal programs have models, and are therefore consistent, and which goals are a consequence of a normal rulebase. For the interpretation of normal rulebases, and normal goals, we will follow an approach similar to that from mathematical (or symbolic) logic.

Roughly speaking, an interpretation of a normal rulebase assigns certain meanings or values to the arguments in the program clauses and gives truth values {true, false} to all normal clauses of the program and all normal goal expressions for the normal program. A normal rulebase is consistent provided that it has a model, that is, if there is an interpretation of the rulebase which makes all of the clauses in the program true. A normal goal is a consequence of a normal rulebase provided that every interpretation that assigns true to every normal rulebase clause must also assign true to the normal goal. More precise definitions follow.

Suppose that R is a normal rulebase. The universe of R, universe(R), is formed using all possible combinations of the individual constants and function symbols of the rulebase.  The definition of the universe is the same as in Section 2 for positive rulebases.

For example, in normal rulebase R1 the individual constants are a and d and the only function symbol is f. The universe of R1 is then the set indicated as follows:

    universe(R1) = {a,b,f(a),f(b),f(f(a)),f(f(b),f(f(f(a))),f(f(f(b),...}

All of the interpretations that we will define will use universe(R) to assign meanings to the variables of clauses of R. If R has no constants, then the convention is to supply a single "dummy constant" so as to provide a nonempty domain. For example, if R were the rulebase that has the single clause

p(X) | p(f(X)).
then universe(R) = {d, f(d), f(f(d), ...}, where d is the "dummy".

It is possible to define interpretations over other universes, or domains, but this will not be necessary for our present purposes.

The base of a normal rulebase R is the collection of all positive predicate terms of R grounded using universe(R).  This is essentially the same definition for the base as given in Section 2 for positve rulebases.

For example, for rulebase R1 again, the base would be

base(R1) = {p(U), q(U), r(U,V), s(U),t(U) | U,V in universe(R1)}
= {p(a), p(f(a)), ... p(b), p(f(b)), ..., q(a),q(f(a)), ... s(a), s(b), s(f(a)), ..., r(a,a), r(a,b),...,etc.}

An interpretation I of R is a mapping from base(R) into the set {true,false}. Such a mapping I assigns truth values to the positive grounded predicate terms of R.

For example, one interpretation of example R1 that is very easy to describe is I1(B) = true for every B in base(R1). Now it will turn out that this interpretation will not satisfy (make true) the third clause of R1. An interpretation I2 that would satisfy all of R1's clauses would be to assign all B in base(R1) true except q(a), and q(a) is assigned to be false. Thus interpretation I2 is a model for R1, showing that R1 is indeed consistent. It should be clear that R1 has infinitely many interpretations. We need to define precisely how an interpretation is used to determine truth values for normal clauses and normal goals for a rulebase.

Suppose that C is a clause of normal rulebase R. A grounding of C is the result of uniformly substituting values from universe(R) for the variables that occur in C.

For example, consider the first clause of example R1. The are infinitely many groundings, including the following:

p(f(a)) | q(b) :- r(a,b).
p(f(b)) | q(b) :- r(b,b).
p(f(f(b))) | q(f(b)) :- r(f(b),f(b)).
etc. ...
Suppose that I is an interpretation of normal rulebase R. The following definitions show how I determines a truth value for each normal clause of R, as follows. If C is a clause of R having the following form
A1 | A2 | ... | Am :- B1, B2, ... Bn .
then I(C) = true provided that, for every grounding
A1' | A2' | ... | Am' :- B1', B2', ... Bn' .
of C, I assigns true to at least one of the Ai' if it assigns true to all of the Bj'. Otherwise, I(C) = false. Informally, an interpretation assigns true to a clause provided it assigns true to each of its possible ground instances over the domain of the program. Furthermore, an interpretation interprets the symbol '|' as 'or', the symbol ',' as 'and' and the symbol ':-' as 'if'.

If clause C has the denial form

false :- B1, B2, ... Bn .
then I(C) = true provided that for every grounding
false :- B1', B2', ... Bn' .
of C, I assigns false to at least one of the Bj'. Otherwise, I(C) = false. Informally, an interpretation assigns true to a denial form clause provided it denies at least one conjunct of each grounding of the clause.

An interpretation satisfies R provided that it assigns true to each clause of R. In this case, the interpretation is a model for the rulebase, and the program is consistent. If no interpretation satisfies R then R is inconsistent, or unsatisfiable. It is easy to construct unsatisfiable normal rulebases, such as the following little program ...

false :- p.
Clearly, this normal program cannot be satisfied by any interpretation, since the first clause would require that p be assigned true, and the second clause would require that p be assigned false.

Now, we also want to define the truth value that an interpretation I of a normal program determines for a normal goal. First assume that goal G has the form

where A is positive atomic (e.g., A = ~q(a)) for R1). Then I(G) = true provided that for every grounding
of G we have I(A') = false; otherwise I(G) = false. Next assume that goal G is a state goal
Q1 | Q2 | ...| Qn.
Then I(G) = true provided that for every grounding
Q1' | Q2' | ...| Qn'.
of G, I assigns true to at least one of the Qi'. Otherwise I(G) = false. Finally, assume that normal goal G has the form
G1, G2, ..., Gk.
Then I(G) = true provided that for every grounding
G1, G2, ..., Gk.
of G, I assigns true to each of the Gj. Otherwise I(G) = false. We also say that I satisfies G provided I(G) = true.

A normal goal G is a consequence of normal rulebase R if, and only if, for every interpretation I, if I satifies R then I must also satisfy G. When this is the case, we will write

    R => G.

Note that an interpretation is completely determined by the values that it asssigns to the base of the rulebase. When we write I(C), C a clause, or I(G), G a normal goal, we are referring to a well-defined extension of the original mapping I.

Two grounded expressions of R (goals or rules) are said to be logically equivalent provided that they have the same truth value under all interpretations of R.  For example, the grounded rule expression d(2) :- a(2) and the disjunctive goal d(2) | ~a(2) are logically equivalent expressions or R.

Exercise 1. Suppose that R is a normal rulebase. Let R.k refer to the kth clause of R. Let (R.k)s refer to the result of substituting for the variables of R.k using a substitution s. Show that R => (R.k)s.

Using the notaion of Exercise 1, let us show that R2 => d(3). We have

R2 => R2.5() = c(3).
Substituting 3 for X in R.1 we have
R2 => R2.1(X/3) = a(3)|b(3) :- c(3)
Using the last two conclusions,
R2 => a(3)|b(3)
and so
R2 => a(3) or R2 => b(3)
if R2 => a(3) then R2 => d(3) using R2.2 and if R2 => b(3) then R2 => d(3) using R2.3 Thus
R2 => d(3)
as required.

Exercise 2. Show that R1 => p(f(a)).

Exercise 3. Show that R1 => ~q(b).

Exercise 4. Show that R2  is consistent and that  R2 => d(1)|d(2).

Exercise 5. Show that if R is is inconsistent then R => G for any normal goal G.

Exercise 6. Show that if R => G1 and R => G2 then R => G1,G2 (the conjunction of G1 and G2).

The yield of a normal rulebase

A (possible) state of a normal rulebase R is a disjunction of the form

    A1 | A2 | ... | An

where each Ai is either a positive or negative literal of R grounded over universe(R), and n >= 1.  For example, the following three expressions represent states for R2:

    d(1)|d(2)  ~c(3)     ~c(2)|d(1)|c(1)

The set of all possible states of R is denoted as

    states(R) = { S |  S is a state of R}.

The states(R) represents all possible grounded disjunctive goals of R. Notice that if

Two states can sometimes be combined using an operation called binary resolution.  If S1 = D1|A is a state containing disjuct literal A and S2 = D2|~A is a state containing disjunct literal ~A then the resolvent of S1 and S2 is the state D1|D2.  For example, using example R1:

r(a,b)|~s(a)|~t(b) and s(a) have resolvent r(a,b)|~t(b)

p(f(a))|q(b)|~r(a,b) and r(a,b)|~s(a)|~t(b) have resolvent p(f(a))|q(b)|~s(a)|~t(b)

We will assume that states are factored, which means that there are no repeated literals (factors) in the disjunction.  Thus d(1) | d(1)|~c(3) would be rewritten in the factored form: d(1)|~c(3).  Note that the factored form is logically equivalent to any unfactored form. Also note that any rearrangement of factors gives a logically equivalent expression.

One state S1 is said to be a substate of state S2 provided that the disjuncts appearing in S1 all appear also in S2. For example, for R2d(1)|d(2) is a substate of d(1)|c(3)|d(2).  We allow that any state is a substate of itself, otherwise we have a proper substate.  A proper substate represents more definite information.

Each grounded rule expression of R is logically equivalent to a state, in a natural way :

  A1|A2|...|Ak :- B1,B2,...,Bn <=>  A1|A2|...|An|~B1|~B2|...|~Bn

  false :- B1,B2,...,Bn        <=>  ~B1|~B2|...|~Bn

(We assume that factoring is done wherever  needed.)  Define set Y1 to be the set of all possible grounded factored rule expressions of R:

    Y1 = { all grounded factored rule expresions of R}

Note that Y1 is a subset of states(R). Y1 is the base for an inductive definition of the yield of rulebase R. The idea is to allow binary resolution to produce all possible resolvents (yields) over and over...

    Y2 = { all factored resolvents of Y1}  ∪ Y1
    Yn+1 = {all factor resolvents of Yn}  ∪ Yn

Note that every Yi is a subset of the next one.  Then, the yield of R is defined as

    yield(R) = UYi,  i = 1, 2,....

the union of all the partial yields.  Finally, define the umbrella of R as the following set:

    umbrella(R) = {S | S is a state of R and some substate of S belongs to yield(R) }

As an example of calculating the Yi, let us show that d(1)|d(2) belongs to yield(R2).  First let us write R2 in the state forms (with variables for awhile).
1  a(X) | b(X) | ~ c(X)
2  d(X) | ~a(X)
3  d(X) | ~b(X)
4  c(1) | c(2)
5  c(3)

Each of states 1-5 belongs to Y1.  Now resolve ground instances of these to get new states as follows ...

6    a(1) | b(1) | c(2)  resolve 1 & 4              in Y2
7    d(1) | b(1) | c(2)  resolve 2 & 6              in Y3
8    d(1) | c(2)         resolve 3 & 7 and factor   in Y4
9    a(2) | b(2) | d(1)  resolve 1 & 8              in Y5
10   d(2) | b(2) | d(1)  resolve 2 & 9              in Y6
11   d(2) | d(1)         resolve 3 & 10 and factor  in Y7

Thus d(1)|d(2) belongs to Y6.

Exercise 7.  (a)  For R1 show that p(f(a))  belongs to Y3.  (b) For R2 show that d(3) belongs to Y3.

The umbrella(R) is a very important set for R.  It represents all the states of R that are logical consequences of R.
Theorem 1.  R => umbrella(R).  (Everything in the umbrella is a logical consequence of R.)

proof.  Exercise 1 above shows that R => Y1.  Suppose that S1 and S2 are two states with resolvent S. Show that if R => S1 and R=> S2 then R => S.  Thus R => Y2.  By mathematical induction R => yield(R).  Notice that anything in umbrella(R) is a logical consequence of something in yield(R).  Thus, R => umbrella(R) also.
Theorem 2.  Suppose that R is a consistent rulebase and that S is a state of R such that R =>S.  Then S belongs to umbrella(R).

proof.  This is actually a restatement of a well-known theorem in resolution theorem proving (the most important one!).  That theorem says the following (using the current terminology of "states"):  If  R is a consistent set of states and state S = A1 | A2 | ... | An is a logical consequence of R, then there is a linear resolution refutation using R ∪ {~A1, ~A2,...,~An}.  A resolution refutation uses binary resolution to produce nil, the empty clause.  We do not reprove this here, but let us look at an example of how a resolution refutation can be recast as a generation of a state in some Yk.  Let us reuse the previous example.   To wit, d(1)|d(2) is a logical consequence of R2, and R2 is logically consistent (See Exercise 4 above.).  Here is a resolution refutation of R2 ∪ {~d(1), ~d(2)}, in the form of a diagram (a typical kind of diagram for linear resolution refutations).  The top center state must belong to R2 ∪ {~d(1), ~d(2)}.  Each resolution step involves the state in the center and the state at the side...  Each side state is either in R or in {~d(1), ~d(2)}.

   center       side

d(1) | ~a(1)

     \------------ ~d(1)


     \------------ a(1) | b(1) | ~c(1)

b(1) | ~c(1)

     \------------ c(1) | c(2)

b(1) | c(2)

     \------------ d(1) | ~b(1)

c(2) | d(1)

     \------------ ~d(1)


     \------------ a(2) | b(2) | ~c(2)

a(2) | b(2)

     \------------ d(2) | ~a(2)


     \------------ d(2)|~b(2)


     \------------ ~d(2)


Now, as an exercise, show how this very same diagram can be systematically modified to show that d(1)|d(2) can be produced using resolvents, that is, that d(1)|d(2) belongs to yield(R).  Argue that this conversion can be done in general, and thus prove Theorem 2. ///

Theorem 2 does not hold when R is inconsistent. The following simple rulebase R shows this.

false :- a.
b :- c.
Note that R => b, but  b  does not belong to umbrella(R).  Show this!!!


Suppose that R is a normal rulebase and that G is a normal goal. Let s be a substitution for the variables in G, and let Gsdenote the result of applying the substitution sto G. Then sis a answer substitution provided that R => Gs. That is, an answer substitution says what values of the variables would make the goal a consequence of the rulebase.

For example, for normal rulebase R1, s = {Z/f(a)} is an answer substitution for goal G = p(Z) because R1 => p(Z)s = p(f(a)). Notation like 'Z / f(a)' means "replace variable Z by f(a)".

The empty substitution is an answer substitution for a grounded goal that is a consequence of the rulebase. For example, for R1 again, s = {} is an answer substitution for the goal G = p(f(a)).

As another example, since R2 => d(1)|d(2), s = {X/1, Y/2} would be an answer substitution for the goal G = d(X)|d(Y).

The concept of answer substitution is cogent for consistent normal programs. For inconsistent rulebases, the concept of an answer substitution is nondiscriminating: Every possible substitution is an answer substitution, according to our definition above, R => Gs. See Exercise 5 above. Later in the section, we will define other kinds of "answers" which are discriminating; that is, even for inconsistent programs, not every substitution would be an "answer".


Every normal rule determines a set of contrapositives. A contrapositive is another kind of clause form, which can be characterized as having the form
H :- B1, B2, ..., Bh .
where H and each Bj is either positive or negative. Normal rules are translated to contrapositives. For example, the first clause of R1 determines the following contrapositive clauses:
p(f(X)) :- ~q(Y), r(X,Y).
q(Y) :- ~p(f(X), r(X,Y).
~r(X,Y) :- ~p(f(X), ~q(Y).
The second clause of R1 determines these contrapositives
r(X,Y) :- s(X), t(Y). %% the clause itself
~s(X) :- ~r(X,Y), t(Y).
~t(Y) :- ~r(X,Y), s(X).
The third clause of R1 determines these contrapositives
~q(b) :- s(a).
~s(a) :- q(b).
In general, a normal clause of the form
A1 | A2 | ... | Am :- B1, B2, ... Bn .
determines m+n contrapositives. (this is also the case if m = 0, the case where the head is false.)

If R is a normal rulebase, let contra(R) denote the set of contrapositive clauses determined by R. We will ignore the ordering of the literals in the body of a contrapositive clause. To simplify things, we can assume that some proscribed ordering rule is used. Later, we will present a Prolog program that expands a file of normal clauses into contrapositive forms.

Rule trees for normal rulebases

The contrapositive clauses are used to construct rule trees for a normal rulebase R. Before the precise definitions are given, it would be best to give several examples of rule trees for the programs R1 and R2. The sample trees will resemble the rule trees discussed in Section 2 of these Logic Topics  for positive rulebases, but there will be some very important additional features of these trees. In many ways these clause trees have much more visual content or suggestive visual information than do text-based reasoning. For example, here is a clause tree for R1 ...

Fig. 1

Fig. 1

The blue numbers next to arcs indicate clause numbers in the original program R1, but in the case of clause #1 and clause #3, contrapositive clauses from contra(R1) have been used to expand the tree. For emphasis, facts have been drawn with branches extending to "true". For example clause #4 has been used as if it were written 's(a) :- true.'. This is the convention used previously for clause trees in Section 3.3.

The tree in Fig. 1 shows, in effect, that R1 => p(f(a)).

Here is a clause tree for R2 ...

Fig. 2

Fig. 2

This tree is interesting because the leftmost leaf ~d(3) is the contrary of its ancestor in the tree, at the root, d(3). Stopping at the leaf ~d(3) is an example of ancestor resolution. This tree shows, in effect, that R2 => d(3).

It might help to explain ancestory resolution if one "argues backwards" from the top of the tree, using the following informal schematic argument (read "<=" as "if").

d(3) <=  a(3)
d(3) <=  ~b(3),c(3)
d(3) <=  ~d(3),c(3)
d(3) <= ~d(3),true
d(3) | d(3) <= true
d(3) <= true
or R2 => d(3). Can you find another clause tree rooted at d(3)? (Hint: note that clause #3, rather than clause #2, could have been used to make a tree.)

Here is another rule tree for R2, with a disjunctive goal at the root...

Fig. 3

Fig. 3

Here, the color boxes show which literals are involved in the ancestory resolution. The unlabelled link under the root does not correspond to a clause of R2, but rather to a rule for constructing clause trees, a so-called "drop-down" rule which says in effect, when trying to create a tree at a disjunctive node, try to construct a tree using either the first disjuct or the remaining disjuctions. There are other clause trees rooted at d(1)|d(2).

Rule trees are defined according to the following technical (but graphically motivated) definitions.

1. Suppose that A.   is a grounded rule in contra(R). Then

tree def 1

is a rule tree. The root of this tree is A, the leaf is 'true'. The tree reflects the fact that the rule says that A is true.

2. Suppose that A :- B1, B2, ..., Bnis a grounded rule in contra(R). Then

tree def 2

is a rule tree. The root of this tree is A, the leaves are B1, B2, ..., Bn.

3. Suppose that

tree def 3a

is a rule tree having root A and leaves L={Bj} ∪ L1. Suppose further that T is a rule tree rooted at Bj having leaves L2. Then

tre def 3b

is also a rule tree rooted at A, and having leaves L1 ∪ L2.

4.  Suppose that  D = A1|...|An is a nonempty (n >= 1) ground disjunctive state goal for R. Then the following is a rule tree rooted at D having descendant Aj, for each j=1,...,n.


The reader should check that the rule trees in Figures 1, 2, and 3 are in accordance with the definition. (This can be somewhat tedious, in general, even though the concepts are quite simple.) The kind of tree formed like in Figure 4 uses what we call a "drop-down" rule: In effect, this amounts to saying that in order to demonstrate D, one could demonstrate a "subdisjunct" of D.
Now for the formal mathematical definition of a rule tree. Rule trees have a mathematical representation as triples <r,D> where r is the root of the tree (which is either a positive or negative literal or a disjunction of same),  and D is a set of descendants of the root r.  The descendants are either leaves or are themselves rule trees. Then, the defintion of rule tree are formulated as follows (this time without the graphical representations).

1.  If  A.  is a rule, then <A,{true}> is a rule tree having leaf true.

2. If A :- B1, B2, ..., Bn  is a rule then <A,{B1, B2, ..., Bn}> is a rule tree having leaves B1, B2, ..., Bn.

3. Suppose that <A,D> is a rule tree having descendants D = {B}  ∪   D1 and leaves {B}  ∪ L1  and suppose that T is a rule tree rooted at B having leaves L2. Then <A,{T} ∪ D1> is a rule tree having leaves L1 ∪ L2.

4. Suppose that  D = A1|...|An is a nonempty (n >= 1) ground disjunctive state goal for R. Then <D, {Aj}> is a rule tree having leaf Aj, for each j.

The mathematical definition would require trees to be expressed in a very tedious way.  For example,  the tree in Fig. 2 would be expressed as

    <d(3), {<a(3),{<~b(3),{~d(3)}>, <c(3),{true}>}>}>

Exercise 8.  Find tree expressions using the mathematical definition for the rule trees drawn in Fig.1 and Fig. 3

Now, the rule trees in Figures 1, 2, and 3 are a special kind of clause tree. Each is a closed tree. A rule tree is closed if each leaf is either true or is the contrary of an ancestor.

Here is the theorem that explains why closed rule trees are important.  We will see how to compute these trees in a straightforward manner presently.
Theorem 3.  A state S belongs to Yh+1 if, and only if, S is the root of a closed rule tree of height <= h. 

Note that the closed rule tree in Fig. 3 has height 6, and that d(1)|d(2) belongs to Y7, as previously demonstrated.

Exercise 9.  (For the mathematically inclined.)  Prove Theorem 3.

Suppose that G is a disjunctive state goal for normal rulebase R. Suppose that s is a substitution for variables of G over universe(R) that grounds G. Then s is an evident answer substitution provided that there is a closed rule tree rooted at Gs

For example, Figure 1 shows that s = {X/f(a)} is an evident answer substitution for G = p(f(X)) for R1. Figure 2 shows that {Z/3} is an evident answer substitution for G = d(Z) for R2, and Figure 3 shows that {X/1,Y/3} is an evident answer substitution for goal G = d(X)|d(Y) for rulebase R2.
Now suppose that G is a general conjunctive normal goal, G=G1,...,Gn. Then a substitution s is an evident answer substitution for G provided that s is an evident answer substitution for all of the Gi jointly. That is, there would be a forest of closed rule trees for G1, G2, ..., Gn.

Thus, we have the following nice theorem, which follows from previous theorems ...
Theorem 4.  Suppose that R is a consistent normal rulebase. If s grounds normal goal G = G1,...,Gn(n >= 1) and if R => Gsthen there is a forest of closed rule trees rooted at the conjuncts Gis.

Of course, a forest of closed rule trees is simply a collection of closed rule trees, one for each Gi.  The only subtle point is that variables occuring in more than one subgoal may be bound via  s.

Thus, if Gs is a consequence of a consistent rulebase then there must be a forest of closed rule trees demonstrating this. Note that one tree (n=1) counts as a (sparse!) forest.

Computing rule trees and evident answers.

Finally, we present a Prolog program that implements what we "normal Prolog" or npl for short. This program provides definitions for ...
loading a file of normal clauses, converting them and asserting the contrapositive forms
listing the contrapositive forms of the normal program
forgetting or purging the normal program previously loaded
computing goals for evident answers
drawing the clause trees computed for evident answers

For example, let us first see how the program is supposed to behave before presenting its specification. Here is a transcript of the actual running program. The file p1.npl contains the normal program P1 from above, and p2.npl contain normal rulebase P2.

?- know('p1.npl').

?- show.

p(f(A)) :- 
        ~ q(B),
        r(A, B).
q(A) :- 
        ~ p(f(B)), 
          r(B, A).
r(A, B) :- 
~ r(A, B) :- 
        ~ p(f(A)), 
        ~ q(B). 
~ s(A) :- 
        ~ r(A, B), 
~ t(A) :- 
        ~ r(B, A), 
~ q(b) :-
~ s(a) :-

?- npl(p(X)).

X = p(f(a);

?- why(p(X)).

|-- p(f(a)) 
      |-- ~ q(b) 
          |-- s(a) 
               |-- true 
      |-- r(a, b) 
          |-- s(a) 
               |-- true 
          |-- t(b) 
               |-- true

X = f(a) ;


Note that npl handles goals with variables in a fashion similar to Prolog. A semicolon after an answer urges more answers, if any. Compare the clause tree drawn by the program with Figure 1.
?- forget.

?- know('p2.npl').

?- why(d(X)|d(Y)).

|-- d(1) | d(2) 
     |-- d(1) 
          |-- a(1) 
               |-- ~ b(1) 
                    |-- ~ d(1) 
                    |-- ancestor resolution 
               |-- c(1) 
                    |-- ~ c(2) 
                         |-- ~ a(2) 
                              |-- ~ d(2)
                                   |-- ancestor resolution 
                         |-- ~ b(2) 
                              |-- ~ d(2) 
                                   |-- ancestor resolution
X = 1
Y = 2 ; ....

|-- d(3) | d(G1096) 
     |-- d(3) 
          |-- b(3) 
               |-- ~ a(3) 
                    |-- ~ d(3) 
                         |-- ancestor resolution 
               |-- c(3) 
                    |-- true 
X = 2
Y = G1096 ; ...
Again, compare the tree that npl computes to the clause tree in Figure 3. Note also that npl can compute answers with variables, as in the second answer shown above. Y = G1906 really means d(3)|d(G1906) is an evident answer for any value of Y.

The loader (know) is fairly straightforward, and will not be explained in detail here. The student may examine the source code in the program file. Similarly for the lister (show) and the forgetter (forget). We will examine the source code for the clause tree inference engine, called ctie in the program specification...

%%%   Clause tree inference engine
%%%   ctie(+Goal,+AncestorList,-ClauseTree).

ctie(true,_,true):- !.                   %%% true
ctie((G,Gs),A,(TG,TGs)) :-               %%% sequence of goals
ctie(G,A,tree(G,T)) :-                   %%% disjunctive goals
   (G = (_|_) ; G = (_;_) ),
ctie(G,A,ancestor_resolution(G)) :-       %%% Ancestor Resolution
   ancestor_resolution(NG,A).             %%% no cut here
ctie(G,_,prolog(G)) :-                    %%% built-ins i.e., Prolog
   ( prolog(G) ;
     predicate_property(G,built_in) ;  
     predicate_property(G,compiled)  ), !,
   call(G).                               %%% Let Prolog do it. 
ctie(G,A,fail) :-                         %%% loop?
ctie(G,A,tree(G,TB)) :-                   %%% use clause

         %%% special treatment for disjunctive goals -- drop down
ctie1((F|R),A,T) :-
ctie1((F;R),A,T) :-
ctie1((F|R),A,T) :-
ctie1((F;R),A,T) :-


definite_negation(~G,G) :- !.

       %%% Ancestry Resolution -- CAN bind. 
ancestor_resolution(G,[F|_]) :- cancel(G,F),!. 
ancestor_resolution(G,[_|R]) :- ancestor_resolution(G,R).   

       %%% cancel if G matches a disjunct -- cancel = unify 
cancel(G,(_|R)) :- cancel(G,R).
cancel(G,(_;R)) :- cancel(G,R).

       %%% Loop checking -- does not bind. 
loop_check(G,[G1|_]) :-  
   G==G1,      %% ancestor with co-bindings    
loop_check(G,[_|R]) :- loop_check(G,R).

npl(G) :- ctie(G,[],_).
npl(G,T) :- ctie(G,[],T).

Notice how closely the code follows the pattern of the meta-interpreters presented in Section 3.3. In fact, the npl version simply adds cases for a drop-down rule for disjunctive goals and a case to detect the possiblity for ancestor resolution (and to force a binding for same if possible). As before, built-ins, such as arithmetic, are handed off to Prolog. As before, there is a simple loop-checker. The loop checker tries to detect whether an ancestor of a node in the clause tree (as currently expanded) has variables that are co-bound (share same current binding with descendant).

The explanation facility why works just like those in Section 3.3

   ctie(G,[],T), %% call the meta-interpreter
   draw_tree(T,0). %% draw the tree calculated
and draw_tree works just like the similarly-named version in section 3.3, except that ancestor resolution is noted, as appropriate.

Exercise 10. Translate the following to a normal program.

Everyone who entered the country and was not a VIP was searched by a customs official.
Bill was a drug pusher who entered the country and who was %% searched by drug pushers only.
No drug pusher was a VIP.
Formulate a normal goal that will answer
Who was both a drug pusher and a customs oficial?
and usp npl to compute the answer. This, and the next, problem appear in Chang and Lee (1972).

Exercise 11. Is the following set of premises consistent? Convert the premises to normal rules and use the npl goal ?- why((~X,X)) to expose the answer....

Exercise 12. Consider the following normal rulebase.
p(a) | p(b).
p(b) | p(c).
Use npl to observe the following queries
?- why(p(X)).
?- why(p(X)| p(Y)).
?- why(p(X)|p(Y)|p(Z)).
and explain the answers produced.

Exercise 13. Consider the following normal rulebase with evaluation.

a(X) | b(Y) :- X < Y.
false :- b(5).
Load this normal rulebase into npl and try the following goals
?- why(a(2)).
?- why(a(-33)).
?- why( b(4)|a(1) ).
?- why(p(X)).
The theory in this section did not really give an explicit meaning to clause trees whose leaves are evaluated using some external method (e.g., aritmetic). How might that be done?

This section is concerned with logic programs with disjunctions and traditional logical negation (so-called "classical negation"). Using trees in conjunction with disjunctive logic programs and well-founded semantics for "negation-as-failure" (the 'not' predicate) is discussed in the reference Fisher (1995). Project: implement a logic program interpreter for well-founded semantics using the approach covered in this reference.

XSB Prolog Code  for npl.P. Note: To use with SWI Prolog simply comment out the definition of 'member'.
Prolog Tutorial Contents

Valid HTML 4.01 Transitional