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

4

No, no, I did not mean to say that the differences between the two procedures are syntactic, I meant that the two ways of representing clauses are equivalent. –Manuel

5

I believe that this chapter of this book should answer your question in some detail :sweat_smile:

Note that I did not find “pattern search” at all in the text of this chapter.

6

Hello Boris,

Thanks. I have the Gallier book, but have not read that chapter yet. I
guess it’s time for me to do this. The term “pattern search” came from
George Luger’s AI textbook, 6th edition. I don’t know where he got it.
There are no references.

Dan

7

I’d have to see the book, but I think “pattern search” is a general, non-technical, term that applies more generally to the domain of logic programming, SLD is a specific procedure that applies specifically to (surely) Prolog. But I too do not have references…

On another note, possibly relevant (and possibly obvious): Prolog is not Horn clauses, unless one does pure Prolog, i.e. pure facts and rules and not even cuts.

8

Good point Julio: Horn clauses is a subset of Prolog, i.e., one can do pure Horn clause programming in Prolog, and then much more. In our classes at the uni a large first part of the course is devoted to programming in pure Prolog, and then the other (very useful) bits and pieces are brought in, each with a corresponding discussion of to how they affect correctness or completeness.

9

Cheers. But I hope it is a computer science class what you are talking about… :wink: Or, a bit more seriously, I could say that, as a programmer (engineer), I am a big fan of the operational semantics of Prolog as the only one relevant…

10

Yes, I mean CS students. Totally agreed on the relevance of the operational semantics, and that a lot of the power of Prolog comes from it, so IMHO teaching it is indispensable. I remember there was a time when people advocated only teaching the declarative semantics, and even designed LP ‘programming’ languages that were said to not have a procedural semantics. Having said this, at least for CS students (but I actually think for all), I believe it is important to teach the beauty of the declarative aspects of the LP paradigm. Asking in advance to excuse me for the self-reference, here is a somewhat recent paper on the topic.

11

Hello Julio,

Here are the pages from George Luger’s AI textbook showing what he calls
“pattern_search”. The reference to his Chapter 14 is where he presents SLD
resolution.

I have found that when I run an SWI-Prolog program with the trace function,
the program execution follows this pattern_search process, working with
Prolog style rules and facts.

It seems that somehow the SLD resolution process with Horn clauses is being
transformed into this pattern_search process. I’m curious regarding how
this is being done and if anyone has ever proven that the two processes are
equivalent. It’s not obvious to me.

Dan Schwartz

(Attachment Pages from Luger-6th-ed.pdf is missing)

12

Hello Julio,

You can get the relevant pages describing that “pattern search” algorithm

www.cs.fsu.edu/~schwartz/Pages_from_Luger-6th-ed.pdf

I tried to send this to the SWI list, but the list replied that it won’t
accept PDF attachments.

The reference in that material to Chapter 14 is where Luger presents SLD
resolution.

I have found that when I run an SWI-Prolog program with the trace function,
the program execution follows this pattern_search process. My simple
example was

p :- q, r.
q.
r.

Running this with trace gives:

[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 clearly is following that pattern_search algorithm.

To perform the equivalent verification using resolution would require
transforming the given Prolog program into a set of Horn clauses:

{p OR NOT q OR NOT r, q, r}

adjoining the negation of the goal p, i.e. NOT p

and then proceeding to repeatedly apply resolution until arriving at the
empty clause.

It is claimed that Prolog is an application of SLD resolution, but this is
not what I see when I run a program in SWI-Prolog. It seems to be using a
completely different algorithm.

Probably the two algorithms can be proven to be equivalent, but what is the
justification for claiming that SLD resolution is involved?

Thanks,

Dan Schwartz

13

Note that ‘p :- q, r.’ (equivalent to ‘p ← q ^ q’, i.e., equivalent to ‘p v not q v not r’) IS a Horn clause, it is just written using different connectives because it is simpler (you avoid all the cumbersome NOTs). And Prolog very definitely runs SLD resolution. The pattern_search algorithm described in the excellent book by George Luger, which uses unification (instead of, say, syntactic string matching), is equivalent to (an implementation of, another way of describing, etc.) SLD resolution.

1 Like
14

I do concur that understanding what “declarative” even means is essential, together with the other “modes”.

I’d also concur on the importance of “beauty”, though the emphasis in production (engineering) is quite different, and we call it “elegance”: and it comes from factors that are not the same as the mathematical ones, not even the definition of “correctness” is the same…

All that said, when I say that the operational semantics is the only one relevant, in production, I mean it: as far as we are concerned, whatever comes out of the magic box, a program is what a program does…

(I wouldn’t want to hijack the present thread: but I am quite available -time permitting- to continue looking into this, what even is “production”? :), just maybe in a separate discussion.)

15

Hello Manuel,

You say that Luger’s pattern_search is another way of “describing” SLD
resolution. I can’t see this. These look like two completely different
algorithms. Can you explain what you mean?

What I see is that pattern_search uses Modus Ponens for a backward chaining
depth-first search of the state space, achieving validation of the goal via
unifications with facts, whereas resolution uses the Resolution rule to
reduce the state space (sets of Horn clauses) to the empty clause. I can’t
see that either is a “desription” of the other.

My concern is what I wrote in my most recent email: that when you run a
program in SWI-Prolog, it clearly follows the pattern_search algorithm, not
resolution. So how can anyone claim that resolution is being employed?

Dan

16

Hi Dan, yes, Prolog is certainly based on SLD resolution. Or, perhaps more precisely, the (traditional) Prolog execution algorithm is a depth-first traversal of the SLD resolution tree. This is probably not the place to go into a detailed description of SLD resolution, but a good reference is the classic book by Gallier (that you mention in your first message). You can find a concise description, also relating Prolog and SLD, in these slides (from our LP/Prolog course materials, see slides 16, 17, and subsequent ones).

17

Hello Manuel,

Thank you for the PowerPoint slides. This is nice work. I teach a bit of
Prolog in my AI course, and these might be helpful.

I took another look at the Gallier book and realize that I need to take the
time to study it in detail.

However, it appears to me that what you call Standard Prolog on slide 17 is
exactly the pattern_search algorithm described in Luger’s book.

Best regards,

Dan

18

Hi Daniel, Manuel,

As far as I understand, pattern search was introduced as a pedagogical framework much later (around 1989) than Prolog was invented. Pattern search is a generic template that can accommodate SLD resolution, since “proof search” is indeed an instance of a search algorithm (where search algorithms are much older than Prolog of course). However, this does not mean that every proof search algorithm is simply pattern search. The devil is in the details: Prolog (and logic programming in general) usually deals more with the symbolic nature of the problem—unification, constraints, etc.—beyond just search.

By the way, this topic may be relevant to any Prolog implementation, so it could be of interest at https://discourse.prolog-lang.org/.

1 Like
19

Jose,

Thanks for your comments. Would you have a reference for “pattern search”?
I’d be interested to know where it was first proposed.

Dan

20

I saw it first proposed here:

You said there was no reference, maybe it was proposed by George F. Luger himself? Why not ask him?