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

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

However, Prolog is

Theorem provers often require some kind of

Here as an example of a theorem prover written in Prolog, implementing the

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

?- Clauses =It leads to the following refutation chain:[[p,not(q)], [not(p),not(s)], [s,not(q)], [q]], pl_resolution(Clauses, Rs), maplist(portray_clause, Rs).

[p, not(q)]-[not(p), not(s)] --> [not(q), not(s)]. [s, not(q)]-[not(q), not(s)] --> [not(q)]. [q]-[not(q)] --> [].Note in particular:

- We are
*not*using Prolog's built-in search strategy as the search strategy of the prover! In this case, the prover uses**iterative deepening**to guarantee*refutation-completeness*:*If*a refutation exists,*then*it is found. Iterative deepening is easy to implement in Prolog, since`length/2`creates longer and longer lists on backtracking, and they can be used for limiting the search. Iterative deepening may seem like a very inefficient search strategy at first glance, but it is in fact an*optimal*search strategy under very general assumptions. - We are
*not*using Prolog variables to represent variables from the object level! In this case, Prolog*atoms*represent propositional variables. This is called a**ground representation**of variables. If we use Prolog variables instead, then we can use**Boolean constraints**as an alternative solution method for showing that the formula is unsatisfiable:?- sat(P + ~Q), sat(~P + ~S), sat(S + ~Q), sat(Q).

The choice of data representation can thus significantly influence how we can reason about such formulas.**false**.

That being said, many properties make Prolog an

- Prolog's built-in
**search**and**backtracking**can be readily used when searching for proofs and counterexamples **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 like**unification** - built-in
**constraints**allow for declarative**specifications**that often lead to very elegant and efficient programs.

**Presprover**: Proves formulas of*Presburger arithmetic*: Implements a completion procedure for`trs.pl`*Term Rewriting Systems*in Prolog.