Automated Theorem Provers in Prolog

The following is from Jens Otten's

Otten describes and implements several provers on

I'm primarily interested in the sequent calculus prover, because I find its method of operation understandable. I've gotten a bit dim in my dotage.

Propositional Logic

(also called "propositional calculus", or sentential calculus), e.g.

    p ∧ (p → q) → q

The logical symbols are:

    →  Implication
    ∧  Conjunction
    ∨  Disjunction
    ¬  Negation

We can use these (Unicode) symbols directly in Prolog with the following operator definitions:

    :- op(1110, xfy, →).
    :- op(1000, xfy, ∧).
    :- op(1100, xfy, ∨).
    :- op( 500, fy, ¬).

See:

After that we can do e.g.:

    ?- write(p ∧ (p → q) → q).
    p∧(p→q)→q
    true.

We could express this directly in Prolog like so:

    p.
    q :- p.

And then pose the query:

    ?- q.
    true.

So that's nice.

Sequent Prover for Propositional Logic

The prolog code follows the `CSM </source/CSM.html>`_ expressions:

    prove(Formula) :-
        Formula \= (_>_),
        prove([] > [Formula]).

The axiom:

    prove(Gamma > Delta) :-
        member(A, Gamma),
        member(A, Delta), !.

As an aside, the axiom predicate above is quadratic, so that's not ideal, but if we stick to small formulas it won't matter much.

Let's start with the Gamma terms:

    % implication
    prove(Gamma > Delta) :-
        select(A → B, Gamma, Gamma1), !,
        prove(   Gamma1  > [A|Delta]),
        prove([B|Gamma1] >    Delta ).

    % conjunction
    prove(Gamma > Delta) :-
        select(A ∧ B, Gamma, Gamma1), !,
        prove([A, B|Gamma1] > Delta).

    % disjunction
    prove(Gamma > Delta) :-
        select(A ∨ B, Gamma, Gamma1), !,
        prove([A|Gamma1] > Delta),
        prove([B|Gamma1] > Delta).

    % negation
    prove(Gamma > Delta) :-
        select(¬A, Gamma, Gamma1), !,
        prove(Gamma1 > [A|Delta]).

Then the Delta terms:

    % implication
    prove(Gamma > Delta) :-
        select(A → B, Delta, Delta1), !,
        prove([A|Gamma] > [B|Delta1]).

    % conjunction
    prove(Gamma > Delta) :-
        select(A ∧ B, Delta, Delta1), !,
        prove(Gamma > [A|Delta1]),
        prove(Gamma > [B|Delta1]).

    % disjunction
    prove(Gamma > Delta) :-
        select(A ∨ B, Delta, Delta1), !,
        prove(Gamma > [A, B|Delta1]).

    % negation
    prove(Gamma > Delta) :-
        select(¬A, Delta, Delta1), !,
        prove([A|Gamma] > Delta1).

That's it. That's all the code to make the sequent prover in Prolog. It's not very dramatic but it works:

    ?- prove(p ∧ (p → q) → q).
    true.

You can trace it to see the proof unfold. Or you can add an extra-logical predicate to print intermediate stages as they unfold::

    prove(F) :- writeln(F), fail.

Giving::

    ?- prove(p ∧ (p → q) → q).
    []>[(p∧(p→q)→q)]
    [(p∧(p→q))]>[q]
    [p,(p→q)]>[q]
    [p]>[p,q]
    [q,p]>[q]
    true .

Neat, eh?

I find the operation of and proofs generated by the sequent prover to be very understandable. You can add some extra cruft to record the steps taken, and then graph out the proof tree or whatever.

First-order Logic

First-order logic— also known as predicate logic, quantificational logic, and first-order predicate calculus —is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable.[1] This distinguishes it from propositional logic, which does not use quantifiers or relations;[2] in this sense, propositional logic is the foundation of first-order logic.

Effectively this means we add::

    ∀x
    ∃x

Sequent Prover for First-order Logic

For universal and existential quantifiers:

    :- op( 500, fy, ∀).   %   universal quantifier: ∀[X]:
    :- op( 500, fy, ∃).   % existential quantifier: ∃[X]:
    :- op( 500,xfy, :).

And so::

    ?- write_term((∃[X]: ∀[Y]: (¬s(Y,Y) → s(X,Y)) → ∃[Z]: s(Z,Z)), [variable_names(['X'=X, 'Y'=Y, 'Z'=Z])]).
    ∃[X]: ∀[Y]:(¬s(Y,Y)→s(X,Y))→ ∃[Z]:s(Z,Z)
    true.

And add rules for them::

    TBD