Theorem Proving with Prolog

First, I realized that the beautiful theorems of Sturm and Liouville are of no use whatsoever. (Gian-Carlo Rota, Ten lessons I wish I had learned before I started teaching differential equations)

Is Prolog a theorem prover? Richard O'Keefe said it best:

Prolog is an efficient programming language because it is a very stupid theorem prover.

Thus, there is a connection between Prolog and theorem proving. In fact, execution of a Prolog program can be regarded as a special case of resolution, called SLDNF resolution.

However, Prolog is not a full-fledged theorem prover. In particular, Prolog is logically incomplete due to its depth-first search strategy: Prolog may be unable to find a resolution refutation even if one exists.

But, and that is the critical point, we can of course implement theorem provers in Prolog! This is because Prolog is a Turing complete programming language, and every theorem prover that can be implemented on a computer can also be implemented in Prolog.

Theorem provers often require some kind of search, such as a search for proofs or counterexamples. It is very easy to implement various search strategies in Prolog: We can, but need not, reuse its built-in depth-first search.

Here as an example of a theorem prover written in Prolog, implementing the resolution calculus for propositional logic:
pl_resolution(Clauses0, Chain) :-
        maplist(sort, Clauses0, Clauses), % remove duplicates
        length(Chain, _),
        pl_derive_empty_clause(Chain, Clauses).

pl_derive_empty_clause([], Clauses) :-
        member([], Clauses).
pl_derive_empty_clause([C|Cs], Clauses) :-
        pl_resolvent(C, Clauses, Rs),
        pl_derive_empty_clause(Cs, [Rs|Clauses]).

pl_resolvent((As0-Bs0) --> Rs, Clauses, Rs) :-
        member(As0, Clauses),
        member(Bs0, Clauses),
        select(Q, As0, As),
        select(not(Q), Bs0, Bs),
        append(As, Bs, Rs0),
        sort(Rs0, Rs), % remove duplicates
        maplist(dif(Rs), Clauses).
The complete file is available from

Here is an example query, using portray_clause/1 to print the resulting refutation chain in such a way that any subsequent program that verifies the proof can easily read it with the built-in predicate read/1:
?- Clauses = [[p,not(q)], [not(p),not(s)], [s,not(q)], [q]],
   pl_resolution(Clauses, Rs),
   maplist(portray_clause, Rs).
It leads to the following refutation chain:
[p, not(q)]-[not(p), not(s)] -->
	[not(q), not(s)].
[s, not(q)]-[not(q), not(s)] -->
[q]-[not(q)] -->
Note in particular: Therefore, when discussing theorem provers that are implemented using Prolog, we must keep in mind that the way Prolog works internally can differ significantly from the implemented behaviour of the prover itself: Its search strategy, its representation of variables, its logical properties, and indeed anything at all can differ from the way Prolog—regarded as a simplistic theorem prover—works internally, since we are using Prolog only as one of many possible implementation languages for theorem provers.

That being said, many properties make Prolog an especially suitable language for implementing theorem provers. For example: Other examples of theorem provers implemented in Prolog are: New combinatorial theorems that were recently established with the help of Prolog are described in You need 27 tickets to guarantee a win on the UK National Lottery and A Prolog assisted search for new simple Lie algebras.

Many logic puzzles can be solved by applying some form of theorem proving.

More about Prolog

Main page