SWI Prolog and SLD REesolution

General
1

Is there documentation the explains the relation of SWI Prolog to SLD resolution?

The literature generally claims that Prolog uses SLD resolution, e.g., “Logic for Computer Science”, by Jean Gallier, Chapter 9, pp. 410-447. But it does not seem that this is how SRI Prolog works. There is another algorithm called “pattern search” discussed in the textbook “Artificial Intelligwence: Structure and Strategies for Problem Solving, 6th Edition”, by George F. Luger, pp. 198-199, which is claimed to be the Prolog algorithm. As a simple example, suppose you are given the knowledge base

  1. Q AND R → P
  2. Q
  3. R

and it is desired to show that the goal P is true. Pattern search proceeds by matching this goal with the conclusion of Item 1, leading to the subgoal

Q AND R

Recursively applying pattern search to the Q leads to the unification of this with fact 2, yielding “true”. Then the algorithm proceeds to apply pattern search to the subgoal R, unifies this with Item 3, yielding “true”, and then “true” is passed back along the recursive chain and applied to P.

If I encode this as a Prolog program:

p :- q, r.
q.
r.

and run this with the trace function in SWI Prolog I get:

[trace] ?- p.
Call: (12) p ? creep
Call: (13) q ? creep
Exit: (13) q ? creep
Call: (13) r ? creep
Exit: (13) r ? creep
Exit: (12) p ? creep
true.

This indicates that SWI-Prolog actually is using the pattern search algorithm.

However, if your are to perform the same exercise using Resolution, you would first need to transform the foregoing program into a set of Horn clauses:

NOT Q OR NOT R OR P, Q, R

add to this set the negation of the goal, NOT P, and then apply resolution as follows. Clash the goal NOT P with the occurrence of P in the foregoing set, yielding the resolvent set

NOT Q OR NOT R, Q, R.

Next clash the NOT Q with Q, yielding the resolvent set

NOT R, R.

Finally clash these two propositions, yielding the empty clause. By the Resolution principle, this establishes that P is a logical consequence of the given three propostions.

But, as shown in the foregoing, this does not seem to be how SWI Prolog actually works. Based on this example, however, it does seem that pattern search and resolution are equivalent when applied to Horn clauses. Only it is not obvious that this is generally correct. Has anyone ever written out a proof of this?

2

Actually, all Prolog systems do implement SLD resolution! The only difference is syntactic: instead of using the classic clausal form to represent the Horn clauses in the program (disjunction of a number of negated literals and one or zero non-negated literals) an equivalent and more convenient syntax is used which uses a single implication with a conjunction of non-negated literals on the antecedent side and zero or one literal on the consequent side. If I remember well this idea is due to Kowalski. Btw, the earliest Prolog systems of Colmerauer et al did use the classic disjunction representation, using + and - to mark positive and negative literals (see, e.g., “The Birth of Prolog” or “50 years of Prolog and beyond", etc.).

1 Like
3

Hello Manuel (or is it Herme),

Thank you for your reply. I have downloaded the two publications you cited,
plus a few otheres I found on Google Scholar. I will look into them.

You say that the differences between the two procedures I described are
merely syntactic, but they look to me like two different algorithms, and
it’s not obvious to me that they are equivalent. This seems to me to be
something that would need to be proven.

But before passing judgement on this, I’ll surely look at those references.

Best regards,

Dan Schwartz

Prof. Daniel G. Schwartz Office 850-644-5875
Dept. of Computer Science, MC 4530 CS Dept 850-644-4029
Florida State University Fax 850-644-0058
Tallahassee, FL 32306-4530 dgschwartz@fsu.edu
U.S.A. http://www [dot] cs [dot] fsu [dot] edu/~schwartz