The evaluation of non-floundering logic programs

24 Feb 2018, 05:00 • prolog, logic

This post is about an extension of Prolog which makes it a more useful and user-friendly logic programming language.

Prolog is a logic programming language which uses SLD resolution to evaluate goals. SLD resolution is based on philosopher Alan Robinson's resolution principle for Horn clauses that made up logic programs. A simple logic program is:

borders(canada, usa).
borders(canada, greenland).

The two predicates tell us that Canada borders the USA and has a (maritime) border with Greenland. The problem is that borders is commutative so we might be tempted to add the following rule:

borders(X, Y) :- borders(Y, X).

Declaratively, the rule makes the program fall in line with our commonsense knowledge but Prolog doesn't like it. The problem is that the evaluation of a goal is recursive so Prolog falls into an infinite loop. Luckily for us, there's an algorithm which lets us evaluate such programs and always terminates—the so-called SLG resolution.

In SLG resolution, to evaluate a goal such as borders(Y, X) (in borders(X, Y) :- borders(Y, X)) the extended Prolog "subscribes" to the goal. Since a goal with the same signature is already being evaluated (namely the head, borders(X, Y)), the goal becomes one of the "consumers" and receives "updates", that is, new grounded results. Thus the "consumers" of the goal are "notified" of the facts borders(canada, usa) and borders(canada, greenland) and subsequently of borders(usa, canada) and borders(greenland, canada) because the order of variables in the rule is reversed. Then the evaluation terminates because no more grounded results can be inferred.

Note the SLG resolution works also with negation (such as we find in Prolog, that is, negation as failure) provided only bound variables are used with negated predicates. Such logic programs are called non-floundering.