Theorem Proving with Prolog
Is Prolog a theorem prover? Richard O'Keefe said it best:
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.
Prolog is an efficient programming language because it is a
very stupid theorem prover.
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
pl_derive_empty_clause(, Clauses) :-
pl_derive_empty_clause([C|Cs], Clauses) :-
pl_resolvent(C, Clauses, Rs),
pl_resolvent((As0-Bs0) --> Rs, Clauses, Rs) :-
select(Q, As0, As),
select(not(Q), Bs0, Bs),
append(As, Bs, Rs0),
sort(Rs0, Rs), % remove duplicates
The complete file is available
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]],
It leads to the following refutation chain:
[p, not(q)]-[not(p), not(s)] -->
[s, not(q)]-[not(q), not(s)] -->
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.
Other examples of theorem provers implemented in Prolog are:
- Prolog's built-in search and backtracking can
be readily used when searching for proofs and
- complete search strategies, such as iterative deepening,
can be easily expressed in Prolog
- Prolog's logical variables can often be used to
represent variables from the object level, allowing us
to absorb built-in Prolog features
- built-in constraints allow for
declarative specifications that often lead to very
elegant and efficient programs.
Many logic puzzles can be solved by applying
some form of theorem proving.
- Presprover: Proves formulas
of Presburger arithmetic
- trs.pl: Implements a
completion procedure for Term Rewriting Systems in
More about Prolog