The Prolog Inference Engine

A Prolog interpreter has two components: the console and the inference engine.

The console's read-infer-print loop perpetually:

1. displays a prompt
2. reads a query
3. asks the inference engine to determine if the query can be inferred from the k-base
4. displays the result: true, false, or a list of variable substitutions that make the query true.

The inference engine is goal-driven. Given a list of goals as input-- which initially consists only of the initial query-- the inference engine attempts to eliminate each goal either by matching it to a fact in the k-base, or by replacing it with the conditions of a rule having a conclusion matching the goal. Of course there may be many conclusions that match the goal, so the inference engine may do a ferocious amount of backtracking.

The inference engine has three important operations:

Unification

Given the goal daughter(lisa, A), the engine searches the KB looking for a matching clause using a pattern matching algorithm called unification.

Unification matches the head of the rule daughter(X, Y) :- parent(Y, X), female(X) but to do so it must make the substitutions X = lisa and Y = A. We call these substitutions a unifier, because making them unifies the goal with a clause in the KB.

Resolution

Resolution is the most used rule of inference in logic:

A=>B  A
B

In English: if we can prove "A implies B" and if we can prove "A", then we may infer "B".

In Prolog notation:

B :- A     A
B

We can extend this to lists of conditions:

B :- A1, A2, A3 ...    A1
B :- A2, A3, ...

For example, if we have proved:

1. daughter(lisa, marge) :- parent(marge, lisa), female(lisa) (B :- A1, A2)
2. parent(marge, lisa) (A1)
3. female(lisa) (A2)

Then we may infer:

daughter(lisa, marge) (B)

Backtracking

If a goal, G, can't be matched with anything in the KB, then the engine backtracks to the step where G was introduced. For example, this might have been a rule of the form: G1 :- G. From this point in the KB it continues searching for a match for G1. Of course if we have reached the end of the KB, then we may assume G is not achievable (and from the CWA we conclude that G is false.

Example

Let's attempt prove a from the KB:

c.
e.
a :- b.
b :- c, d.
a :- c, e.

We can think of a proof as a tree. A node is labeled by a list of goals. Its children show the possible results of resolving the first goal by every matching clause in the KB. The root of the tree contains the initial query, the statement we are trying to prove.

The job of the inference engine is to build this tree, searching for an empty node.

In the example above the root a can resolve with clauses 3 and 5 in the KB. The left child shows the result of resolving a with the third clause, the right child shows the result of resolving a with the fifth clause.

If the tree is constructed in a depth first manner (which results from resolution adding conditions to the end of the goal list instead of the front), then the inference engine can't eliminate the goal d. But instead of giving up, it backtracks to the last branch in the tree. Following/constructing this branch eventually reaches a node with no goals, and therefore a is proved.