Prolog Tricks for Constructing Hilbert-Style Proofs

The missing Prolog occurs check notoriously causes problems. The Jekejeke Prolog Minlog Extension provides a sto/1 constraint. We deviced a little demo that does an iterative deepening search of a Hilbert Style proof. We use a very minimal Hilberttyle few rules. For brevity we omit parenthesis and write A1 -> ... -> An instead of (A1 -> ... (... -> An) ...) :

ax-1: A->B->A

ax-2: ((A->B->C)->(A->B)->(A->C))

         A -> B       A
ax-mp:   --------------
                B

This can be readily translated into a predicate hilbert/2 that does a backward chaining proof search. Since the inference rule ax-mp introduceds a new formula A, the backward chaining proof search will introduce Prolog variables, which act as meta variables for propositional formulas To avoid cyclic terms, we deploy our sto/1 subject to occurs check constraint. The predicate hilbert/2 is seen in the Prolog text hilbert.p . It reads as follows:

:- use_module(library(term/herbrand)).

hilbert((A->_->A),  _).
hilbert(((A->B->C)->(A->B)->(A->C)), _).
hilbert(B, N) :-
   N > 0,
   M is N-1,
   sto(A),
   hilbert((A->B), M),
   hilbert(A, M).

We can use this predicate to check whether a formula has a proof or not. We just supply a proof depth in the second argument, and can then iteratively try to find a proof. This is the only hint that the predicate hilbert/2 accepts. Here is a verification that p->p is provable, there are 3 proofs of depth 2:


A yes-no answer is not very satisfactory. We might want to see the proof as well. To enable proof extraction, we can add a further parameter to the predicate hilbert/2 and turn it into a predicate hilbert/3. For axiom schemas , that do not have additional parameters, we simply return the name of the axiom. For the only inference rule modus ponens, we return the invented formula A beside the two sub proofs P and Q.

The predicate hilbert/3 is found in the Prolog text hilbert2.p :

:- use_module(library(term/herbrand)).

hilbert((A->_->A), 'ax-1', _).
hilbert(((A->B->C)->(A->B)->(A->C)), 'ax-2', _).
hilbert(B, 'ax-mp'(P,Q,A), N) :-
   N > 0,
   M is N-1,
   sto(A),
   hilbert((A->B), P, M),
   hilbert(A, Q, M).

If we run the predicate hilbert/3, we do get proof trees, but they contain Prolog variables, which are formula meta variables. We also see the residual sto/1 constraints. The proof trees are not yet pretty printed:


Prolog text hilbert2.p contains also some code to pretty print the proof tree. This works in two phases. In the first phase we replace the meta variables by new names. And in the second phase we number the proof steps and show them line by line. The predicate disp/2 does the job: