forward chaining

the forward-chaining algorithm (which stands for "propositional logic forward chaining entails" and is shown in fig-forward-chaining-2) determines if a single proposition symbol –the query–is entailed by a knowledge base of definite clauses. it begins from known facts (positive literals) in the knowledge base. if all the premises of an implication are known, then its conclusion is added to the set of known facts. for example, if and are known and is in the knowledge base, then can be added. this process continues until the query is added or until no further inferences can be made. it is important to remember that this algorithm runs in linear time.

the best way to understand the algorithm is through an example and a picture. fig-forward-chaining-1 shows a simple knowledge base of horn clauses with and as known facts and the knowledge base drawn as an graph.

in graphs, multiple edges joined by an arc indicate a conjunction-—every edge must be proved—-while multiple edges without an arc indicate a disjunction—-any edge can be proved. it is easy to see how forward chaining works in the graph. the known leaves (here, and ) are set, and inference propagates up the graph as far as possible. wherever a conjunction appears, the propagation waits until all the conjuncts are known before proceeding.

the backward chaining algorithm, as its name suggests, works backward from the query. if the query is known to be true, then no work is needed. otherwise, the algorithm finds those implications in the knowledge base whose conclusion is . if all the premises of one of those implications can be proved true (by backward chaining), then is true. when applied to the query in fig-forward-chaining-1, it works back down the graph until it reaches a set of known facts, and , that forms the basis for a proof. as with forward chaining, an efficient implementation runs in linear time.

fig-forward-chaining-3 shows a simple forward chaining inference algorithm for first-order logic. starting from the known facts, it triggers all the rules whose premises are satisfied, adding their conclusions to the known facts. the process repeats until the query is answered (assuming that just one answer is required) or no new facts are added. notice that a fact is not "new" if it is just a renaming of a known fact—-a sentence is a renaming of another if they are identical except for the names of the variables. for example, and are renamings of each other. they both mean the same thing: "everyone likes ice cream."

fig-forward-chaining-4 shows a backward-chaining algorithm for definite clauses. will be proved if the knowledge base contains a rule of the form , where lhs (left-hand side) is a list of conjuncts. an atomic fact like is considered as a clause whose lhs is the empty list. now a query that contains variables might be proved in multiple ways. for example, the query could be proved with the substitution as well as with . so we implement as a generator—-a function that returns multiple times, each time giving one possible result. works by fetching all clauses that might unify with the goal, standardizing the variables in the clause to be brand new variables, and then, if the of the clause does indeed unify with the goal, proving every conjunct in the , using . that function works by proving each of the conjuncts in turn, keeping track of the accumulated substitution as it goes. backward chaining, as we have written it, is clearly a depth-first search algorithm. this means that its space requirements are linear in the size of the proof. it also means that backward chaining (unlike forward chaining) suffers from problems with repeated states and incompleteness. despite these limitations, backward chaining has proven to be popular and effective in logic programming languages.