Theorem Proof Using Prolog

Question

How can I write theorem proofs using Prolog?

I have tried to write it like this:

parallel(X,Y) :-
    perpendicular(X,Z),
    perpendicular(Y,Z),
    X \== Y,
    !.

perpendicular(X,Y) :-
    perpendicular(X,Z),
    parallel(Z,Y),
    !.

Can you help me?

Cleanthes

Prolog is a programming language, not a theorem prover. – Euphemiah

Prolog is often described as a backward chaining inference method, i.e. given a goal, the Prolog engine seeks a "depth-first" way to satisfy that goal. Theorem Provers often use more versatile strategies, adding forward chaining inference methods. – Subtotal

@Subtotal and what about SETHEO? – Muscadel

@false: Yes, SETHEO is a (modular) theorem prover, although not one written in Prolog. The OP Aman may not be asking about writing a general theorem prover, but have a more limited aim of understanding why Prolog behaves as it did when given those two rules ("axioms"). – Subtotal

@hardmath: Prolog systems are becoming cleaner, we have already 4 active systems with occurs-check (SWI, XSB, CX, Qu) and with excellent performance for it (SWI). In such a situation I am a bit unhappy about this "it is not a theorem prover" mindset. – Muscadel

@false: Not my phrase, but Prolog uses only a limited fragment of propositional logic (Horn clauses), so as a "theorem prover" the Prolog engine has definite limitations. Of course as a general purpose programming language Prolog has many advantages for symbolic processing and for search processes other than depth-first. It's simply a matter of writing the code, not having it "out of the box". – Subtotal

I like this quote from Richard O'Keefe: "Prolog is an efficient programming language because it is a very stupid theorem prover." – Rifling

@mat: Thanks, I'm a huge fan of R. O'Keefe but hadn't seen that quote! – Subtotal

Answer 1

I was reluctant to post an Answer because this Question is poorly framed. Thanks to theJollySin for adding clean formatting! Something omitted in the rewrite, indicative of what Aman had in mind, was "I inter in Loop" (sic).

We don't know what query was entered that resulted in this looping, so speculation is required. The two rules suggest that Goal involved either the parallel/2 or the perpendicular/2 predicate.

With practice it's not hard to understand what the Prolog engine will do when a query is posed, especially a single goal query. Prolog uses a pretty simple "follow your nose" strategy in attempting to satisfy a goal. Look for the rules for whichever predicate is invoked. Then see if any of those rules, starting with the first and going down in the list of them, can be applied.

There are three topics that beginning Prolog programmers will typically struggle with. One is the recursive nature of the search the Prolog engine makes. Here the only rule for parallel/2 has a right-hand side that invokes two subgoals for perpendicular/2, while the only rule for perpendicular/2 invokes both a subgoal for itself and another subgoal for parallel/2. One should expect that trying to satisfy either kind of query inevitably leads to a Hydra-like struggle with bifurcating heads.

The second topic we see in this example is the use of free variables. If we are to gain knowledge about perpendicularity or parallelism of two specific lines (geometry), then somehow the query or the rules need to provide "binding" of variables to "ground" terms. Again without the actual Goal being queried, it's hard to guess how Aman expected that to work. Perhaps there should have been "facts" supplied about specific lines that are perpendicular or parallel. Lines could be represented merely as atoms (perhaps lowercase letters), but Prolog variables are names that begin with an uppercase letter (as in the two given rules) or with an underscore (_) character.

Finally the third topic that can be quite confusing is how Prolog handles negation. There's only a touch of that in these rules, the place where X\==Y is invoked. But even that brief subgoal requires careful understanding. Prolog implements "negation as failure", so that X\==Y succeeds if and only if X==Y does not succeed. This latter goal is also subtle, because it asks whether X and Y are the same without trying to do any unification. Thus if these are different variables, both free, then X==Y fails (and X\==Ysucceeds). On the other hand, the only way for X==Yto succeed (and thus for X\==Y to fail) would be if both variables were bound to the same ground term. As discussed above the two rules as stated don't provide a way for that to be the case, though something might have taken care of this in the query Goal.

The homework assignment for Aman is to learn about these Prolog topics:

• recursion
• free and bound variables
• negation

Perhaps more concrete suggestions can then be made about Prolog doing geometry proofs!

Added: PTTP (Prolog Technology Theorem Prover) was written by M.E. Stickel in the late 1980's, and this 2006 web page describes it and links to a download.

It also summarizes succinctly why Prolog alone is not " a full general-purpose theorem-proving system." Pointers to later, more capable theorem provers can be followed there as well.

Subtotal