5.4. Forward chaining#
Search programs involving if-then rules, such as meta-interpreters and theorem provers, can use these rules in either of two directions: from body to head or forward, and from head to body or backward. The meta-interpreters we encountered up till now apply clauses backward, just like Prolog; they are said to perform backward chaining. For checking if a given formula follows logically from a given theory, this is usually the best strategy.
However, in some cases we must rather perform forward chaining, because we do not have a goal to start from. For instance, consider the problem of constructing a model of a given theory. It would not be feasible to generate all the ground atoms in the Herbrand base and follow the chains back to the theory. Rather, we would generate the model incrementally by forward chaining. The procedure is as follows:
search for a violated clause of which the body is true in the current model, but the head is not (such a clause is said to fire);
add a literal from the head to the model[1].
By step 2, the head (a disjunction) is made true in the model, so that this clause is no longer violated. The procedure iterates back to step 1; if no violated clauses remain, the model is complete.
The program for model generation by forward chaining is given below. It is a fairly simple forward chainer, in the sense that it simply chooses the first clause which fires. More sophisticated forward chainers use conflict resolution strategies in order to choose among the rules which fire at a certain stage.
% model(M) <- M is a model of the clauses defined by cl/1
model(M):-
model([],M).
model(M0,M):-
is_violated(Head,M0),!, % instance of violated clause
disj_element(L,Head), % L: ground literal from head
model([L|M0],M). % add L to the model
model(M,M). % no more violated clauses
is_violated(H,M):-
cl((H:-B)),
satisfied_body(B,M), % grounds the variables
\+ satisfied_head(H,M).
satisfied_body(true,_M). % body is a conjunction
satisfied_body(A,M):-
member(A,M).
satisfied_body((A,B),M):-
member(A,M),
satisfied_body(B,M).
satisfied_head(A,M):- % head is a disjunction
member(A,M).
satisfied_head((A;_B),M):-
member(A,M).
satisfied_head((_A;B),M):-
satisfied_head(B,M).
%%% from Section 10.2 (appendix)
disj_element(X,X):- % single-element disjunction
X\=false,
X\=(_;_).
disj_element(X,(X;_Ys)).
disj_element(X,(_Y;Ys)):-
disj_element(X,Ys).
%%% Example disjunctive clauses to compute model for
cl((married(X);bachelor(X):-man(X),adult(X))).
cl((has_wife(X):-married(X),man(X))).
cl((man(paul):-true)).
cl((adult(paul):-true)).
Given the following clauses:
cl((married(X);bachelor(X):-man(X),adult(X))).
cl((has_wife(X):-married(X),man(X))).
cl((man(paul):-true)).
cl((adult(paul):-true)).
and the query ?-model(M), the program constructs the following models (on backtracking):
M = [has_wife(paul),married(paul),adult(paul),man(paul)];
M = [bachelor(paul),adult(paul),man(paul)]
Notice that these are the two minimal models of the program.
Not every model generated by model/1 is minimal. Consider the following set of clauses:
cl((likes(peter,maria):-true)).
cl((student(maria):-true)).
cl((teacher(X);friendly(Y):-likes(X,Y),student(Y))).
cl((friendly(Y):-teacher(X),likes(X,Y))).
is_violated/2 will first succeed for the third clause, returning the instantiated head teacher(peter);friendly(maria). The first literal in this head will be added to the model. Next, the fourth clause is violated, and friendly(maria) is added to the model. This results in the following model:
[ friendly(maria),teacher(peter),
student(maria),likes(peter,maria) ]
However, this is not a minimal model since teacher(peter) can be removed from it, yielding the model
[ friendly(maria),student(maria),likes(peter,maria) ]
which will be returned as the second answer.
It should be noted that the program only works properly for a restricted class of clauses, namely those clauses for which grounding the body also grounds the head. Otherwise, a head literal from a violated clause might still contain variables. Adding a non-ground literal to the model could result in incorrect behaviour. Consider the following set of clauses:
cl((man(X);woman(X):-true)).
cl((false:-man(maria))).
cl((false:-woman(peter))).
Since the first clause is violated by the empty model, the program will attempt to add man(X) to the model. This leads to the second clause being violated, and since this clause has an empty head, it cannot be satisfied by adding a literal to the model. Upon backtracking woman(X) is tried instead, but this leads to a similar problem with the third clause. Consequently, model/1 will fail to construct a model, although there exists one, namely { man(peter), woman(maria) }.
The solution is to add a literal to the body of the first clause, which serves to enumerate the possible values for X:
cl((man(X);woman(X):-person(X))).
cl((person(maria):-true)).
cl((person(peter):-true)).
cl((false:-man(maria))).
cl((false:-woman(peter))).
In this way, the first clause is violated only under the substitutions { X → maria} and { X → peter }. Thus, all literals which are added to the model are ground, and the program constructs the correct model
[man(peter),person(peter),woman(maria),person(maria)]
Clauses of which all variables in the head occur also in the body are called range-restricted. Every set of clauses can be transformed into a set of range-restricted clauses by adding domain predicates enumerating the domains of variables, as above. The two sets of clauses are equivalent in the sense that there exists a one-to-one correspondence between their models:
any model of the original clauses provides an enumeration of all the domains;
any model of the range-restricted clauses can be transformed to a model of the original clauses by dropping the domain literals.
Obviously, model/1 loops if the model being constructed is infinite. This will happen, for instance, with the following set of clauses, representing a range-restricted version of the append predicate:
cl((append([],Y,Y):-list(Y))).
cl((append([X|Xs],Ys,[X|Zs]):-thing(X),append(Xs,Ys,Zs))).
cl((list([]):-true)).
cl((list([X|Y]):-thing(X),list(Y))).
cl((thing(a):-true)).
cl((thing(b):-true)).
cl((thing(c):-true)).
Instead of the complete, infinite model, we might be interested in a subset over a universe of lists up to a given length. Such a ‘submodel’ can be computed by a forward chaining procedure which stops after a prespecified number of steps. In this way, the procedure gets more of a ‘breadth-first’ flavour. The program is given below:
% model_d(D,M) <- M is a submodel of the clauses
% defined by cl/1
model_d(D,M):-
model_d(D,[],M).
model_d(0,M,M).
model_d(D,M0,M):-
D>0,D1 is D-1,
findall(H,is_violated(H,M0),Heads),
satisfy_clauses(Heads,M0,M1),
model_d(D1,M1,M).
satisfy_clauses([],M,M).
satisfy_clauses([H|Hs],M0,M):-
disj_element(L,H),
satisfy_clauses(Hs,[L|M0],M).
model/1 is replaced by model_d/2, which has an additional depth parameter. On each iteration, all the violated clauses are generated and satisfied.
Below, we illustrate the operation of the program on the above set of clauses, setting the depth to 4:
?-model_d(4,M).
M = [list([a,c,a]), list([a,c,b]), list([a,c,c]), % D=4 %
list([a,b,a]), list([a,b,b]), list([a,b,c]),
list([a,a,a]), list([a,a,b]), list([a,a,c]),
list([b,c,a]), list([b,c,b]), list([b,c,c]),
list([b,b,a]), list([b,b,b]), list([b,b,c]),
list([b,a,a]), list([b,a,b]), list([b,a,c]),
list([c,c,a]), list([c,c,b]), list([c,c,c]),
list([c,b,a]), list([c,b,b]), list([c,b,c]),
list([c,a,a]), list([c,a,b]), list([c,a,c]),
append([a],[a],[a,a]), append([a],[b],[a,b]),
append([a],[c],[a,c]), append([a,c],[],[a,c]),
append([a,b],[],[a,b]), append([a,a],[],[a,a]),
append([b],[a],[b,a]), append([b],[b],[b,b]),
append([b],[c],[b,c]), append([b,c],[],[b,c]),
append([b,b],[],[b,b]), append([b,a],[],[b,a]),
append([c],[a],[c,a]), append([c],[b],[c,b]),
append([c],[c],[c,c]), append([c,c],[],[c,c]),
append([c,b],[],[c,b]), append([c,a],[],[c,a]),
append([],[c,a],[c,a]), append([],[c,b],[c,b]),
append([],[c,c],[c,c]), append([],[b,a],[b,a]),
append([],[b,b],[b,b]), append([],[b,c],[b,c]),
append([],[a,a],[a,a]), append([],[a,b],[a,b]),
append([],[a,c],[a,c]),
list([a,c]), list([a,b]), list([a,a]), % D=3 %
list([b,c]), list([b,b]), list([b,a]),
list([c,c]), list([c,b]), list([c,a]),
append([a],[],[a]), append([b],[],[b]),
append([c],[],[c]), append([],[c],[c]),
append([],[b],[b]), append([],[a],[a]),
list([a]), list([b]), list([c]), % D=2 %
append([],[],[]),
thing(c), thing(b), thing(a), % D=1 %
list([]) ]
At depth 1, only domain clauses are satisfied; at depth 2 the first append literal appears. Depths 3 and 4 add list literals for all lists of length 2 and 3, and append literals for all lists of length 1 and 2, respectively.