Forward chaining – backward chaining

Backward Chaining

Putting all the above together, we formulate the following non-deterministic algorithm

for resolution in Horn theories. This is known as backward chaining.

bc(in P0 : negated goal;

GAMMA : set of facts and rules;)

{ if P0 = null then succeed;

pick a literal L in P0;

choose a clause C in GAMMA whose head resolves with L;

P := resolve(P0,GAMMA);

bc(P,GAMMA)

}

We are now ready to deal with (pure) Prolog, the major Logic Programming Language. It

is obtained from a variation of the backward chaining algorithm that allows Horn clauses

with the following rules and conventions:

• The Selection Rule is to select the leftmost literals in the goal.

• The Search Rule is to consider the clauses in the order they appear in the current

list of clauses, from top to bottom.

• Negation as Failure, that is, Prolog assumes that a literal L is proven if if it is

unable to prove (NOT L)

• Terms can be set equal to variables but not in general to other terms. For example,

we can say that x=A and x=F(B) but we cannot say that A=F(B).

are added to the bottom of the list of available clauses.

These rules make for very rapid processing. Unfortunately:

The Pure Prolog Inference Procedure is Sound but not Complete

This can be seen by example. Given

• P(A,B)

• P(C,B)

• P(y,x) < = P(x,y)

• P(x,z) < = P(x,y),P(y,z)

Real Prolog systems differ from pure Prolog for a number of reasons. Many of which

have to do with the ability in Prolog to modify the control (search) strategy so as to

achieve efficient programs. In fact there is a dictum due to Kowalski:

Logic + Control = Algorithm

But the reason that is important to us now is that Prolog uses a Unification procedure

which does not enforce the Occur Test. This has an unfortunate consequence that, while

Prolog may give origin to efficient programs, but

Prolog is not Sound

Actual Prolog differs from pure Prolog in three major respects:

• There are additional functionalities besides theorem proving, such as functions to

assert statements, functions to do arithmetic, functions to do I/O.

• The "cut" operator allows the user to prune branches of the search tree.

• The unification routine is not quite correct, in that it does not check for circular

bindings e.g. X -> Y, Y -> f(X).)

Forward chaining

An alternative mode of inference in Horn clauses is forward chaining . In forward

chaining, one of the resolvents in every resolution is a fact. (Forward chaining is also

known as "unit resolution.")

Forward chaining is generally thought of as taking place in a dynamic knowledge base,

where facts are gradually added to the knowledge base Gamma. In that case, forward

chaining can be implemented in the following routines.

The forward chaining algorithm may not terminate if GAMMA contains recursive rules.

Forward chaining is complete for Horn clauses; if Phi is a consequence of Gamma, then

there is a forward chaining proof of Phi from Gamma. To be sure of finding it if Gamma

contains recursive rules, you have to modify the above routines to use an exhaustive

search technique, such as a breadth-first search.

In a forward chaining system the facts in the system are represented in a working memory

which is continually updated. Rules in the system represent possible actions to take when

specified conditions hold on items in the working memory - they are sometimes called

condition-action rules. The conditions are usually patterns that must match items in the

working memory, while the actions usually involve adding or deleting items from the

working memory.

Choice between forward and backward chaining

Forward chaining is often preferable in cases where there are many rules with the same

conclusions. A well-known category of such rule systems are taxonomic hierarchies.