Prolog for deductive proofs

Main article: Logic

Intro to Prolog

SWI-Prolog was used here, from which the 64-bit Windows version was installed. Versions for Linux and other OS’s exist. It is distributed with the Simplified BSD license.

https://www.swi-prolog.org/

SWI Prolog presents the user with a command prompt in which to enter queries and an editor for entering facts. Any editor can be used but the built-in one offers some syntax highlighting. After saving an edited file use the following command, eg, to load it into Prolog:

[1]  ?- consult('c:/a/peerverity/logic/prolog2.pl').

Facts are expressed by saying, eg:

Sally wears red:
wearsred(sally).

Bill likes soccer:
likessoccer(bill).

These facts can then be queried after saving the file:

?- wearsred(sally).
true.

?- likessoccer(wanda).
false.

There is no fact in the database about Wanda, so Prolog returns false by default. Note that the names must be lower case. Upper case is reserved for variables. We could ask Prolog to “solve” for a variable:

?- wearsred(X).
X = sally.

We can do more complex cases:

wearsred(sally).
wearsred(jane).
hasadrink(sally).
hasadrink(jane).
isnothungry(sally) :- false.
isnothungry(jane).
ishappy(X) :- (wearsred(X);hasadrink(X)),isnothungry(X)).

A query for X at this point will lead to:

?- ishappy(X).
X = jane.

The query would simply return false if it can’t find a solution.

Symbols in Prolog:

:- means if, eg ispresident(mike) :- wonelection(mike).
; means or
, means and
\+ means not or ~, eg \+dances(jill) means jill does not dance.

Proving a simple argument in Prolog

Consider a very simple argument, the Disjunctive Syllogism:

${\textstyle P\lor Q}$
${\textstyle \neg P}$
${\textstyle \therefore Q}$

We could attempt the following Prolog program to do this:

exists(paul).
premise1 :- exists(p);exists(q).
premise2 :- \+exists(p).
conclusion :- (\+premise1;\+premise2);exists(q).

?- conclusion.
true.

We state that Paul exists on line 1 in order to instantiate the “function” exists. Without it, Prolog will simply give an error. Note also that the conclusion is framed as a statement which says that “if the premises are true then the conclusion is true”, which is just another way to state the argument itself. The form of the conclusion is made possible through the use of our equivalence rules:

${\textstyle (premise1\land premise2)\implies Q}$

${\textstyle \neg (premise1\land premise2)\lor Q}$…. by Material Implication, ie ${\textstyle P\implies Q\equiv \neg P\lor Q}$

${\textstyle (\neg premise1\lor \neg premise2)\lor Q}$…. by De Morgan’s rule, ie ${\textstyle \neg (P\land Q)\equiv (\neg P\lor \neg Q)}$

The reason we perform these manipulations is, for one, because we cannot include an if statement within another if statement. Another reason is that Prolog prefers negation inside parenthesis (operating on an individual literal), rather than outside (operating on many literals at once). This is known as CNF (conjunctive normal form). It should be noted that outside the parenthesis negation does seem to work with the version of Prolog we are using here. Perhaps the stricter rule applied to earlier implementations of Prolog.

In any event, as shown above, this input leads to a true conclusion. This is what we’d expect, of course, but it really isn’t proving the result the way we’d expect.

Why? Prolog starts by querying its database of facts. It matches its known facts to the rules until the rules are satisfied. Since no facts about the existence of p and q were given, these are taken as false. So, since both exists(p) and exists(q) is false, premise1 is false and premise2 is true. Since one of the premises is false, the negation of that premise is true and the concluding argument (which is nothing more than an or statement of negated premises along with the conclusion itself) is true. Thus, Prolog didn’t really prove anything. It merely confirmed the truth of the concluding argument given facts about p and q. In this case, since we are dealing with a valid argument, all combinations of p and q truth values will lead to a true conclusion.

We cannot force our way out of this situation. If we try, for instance, to constrain the premises to be true we will still get an incorrect answer:

exists(paul).
premise1 :- exists(p);exists(q).
premise2 :- \+exists(p).
conclusion :- (\+premise1;\+premise2);exists(q).
premise1 :- true.
premise2 :- true.

[1]  ?- exists(q).
false.

Note here that we don’t even care about the conclusion. Our interest is in getting Prolog to “solve for” the fact that q must exist given the way we have set up the problem. There is only 1 solution, which is that q exists and p does not. But clearly Prolog does not work this way. To Prolog, the existence of p and q starts out as false since nothing was said about them. Therefore exists(q) is false, regardless of what else was said.

Let’s look at an even simpler version of this.

exists(p).
exists(q).
premise1 :- exists(p);exists(q).
premise1 :- false.

[1]  ?- premise1.
true .

Here, since Prolog sees that p and q exist, it uses the first premise1 to conclude true. The second premise1 is simply ignored. When faced with multiple paths to a solution, Prolog simply picks one and goes with it. This appears to be what is known as Prolog’s “depth-first” solution strategy.

Now, if we return to the disjunctive syllogism argument as a whole and simply place a negation sign in front of the conclusion and try to validate that argument, we will also get a true value for the conclusion. We know the argument to be invalid but it so happens that if both p and q are false, then the concluding statement is true. We would have to go through all the possible values of p and q to establish a false case (this happens when q is true and p is false).

One may argue that this isn’t so bad. In a sense we have created a foolproof method for proving any deductive argument. But in fact it is no better than a truth table method because it requires that we go through every truth combination of the inputs. In essence, it is a truth table method. It is not using inference & equivalence rules to perform proofs in the manner that discussed here.

This is how Prolog works. It starts from concrete facts and uses logical rules to confirm or deny queries. It cannot will facts into existence based on an abstract logical argument as we would like it to do here.

However, Prolog, like any language, can be programmed to provide the theorem proving capabilities that we’d like. Several sources on this exist:

Prolog as a theorem prover:

https://www.metalevel.at/prolog/theoremproving#:~:text=However%2C%20Prolog%20is%20not%20a,implement%20theorem%20provers%20in%20Prolog!

A theorem prover for Prolog:

https://www.ai.sri.com/~stickel/pttp.html

A survey of various theorem provers (Prolog is not among them):

https://arxiv.org/pdf/1912.03028.pdf#:~:text=Theorem%20provers%20are%20fundamentally%20based,logic%20is%20further%20discussed%20next.

A few more examples

Modus Ponens works in Prolog:

exists(p).
exists(q) :- exists(p).

[1]  ?- exists(q).
true.

This case is straightforward and conforms to Prolog’s internal operation. The existence of p is stated upfront. The existence of q has a rule based on the existence of p. There is only one way Prolog can solve this.

Modus Tollens, however, does not for the reasons given above even though it yields the “correct” answer.

exists(q) :- exists(p).
exists(q) :- false.

[1]  ?- exists(p).
false.

We can further verify that this doesn’t work by setting exists(q) to be true in an attempt to make exists(p) be true:

exists(q) :- exists(p).
exists(q) :- true.

[1]  ?- exists(p).
false.