Prolog implementation of Beckert & Posegga's algorithm

My notes on this. Not even executed once!

% Only for (classical logic) closed first-order formula in:
% Skolemized Negation Normal Form (which is set up by a preprocessor)
% "Closed" means "No free variables".
%
% Negation Normal Form: https://en.wikipedia.org/wiki/Negation_normal_form
%
% 1) The negation operator is only applied to propositional variables or literals.
% 2) Only operator AND and OR are allowed.
%
% Skolemized: https://en.wikipedia.org/wiki/Skolem_normal_form 
%
% 1) In Prenex normal form
% 2) With only universal first-order quantifiers
%
% i.e. the X in exists(X) have been replaced by skolem constants
%
% This is called
%
% prove(+Fml,UnExp,Lits,FreeV,VarLim)
% 
% but is actually
%
% disprove(+Fml,UnExp,Lits,FreeV,VarLim)
% 
% Because the query *succeeeds* if there is a closed tableau for the 
% first-order formula bound to Fml (i.e. the formula is unsatisfiable;
% one thus passes the negation of the formula to prove to disprove/5
% (the paper uses the adjective "inconsistent" instead of "unsatisfiable"
% but "inconsistency" is a system attribute, not a formula attribute)
%
% Method of analytical tableaux: 
% https://en.wikipedia.org/wiki/Method_of_analytic_tableaux
%
% Current branch:
%   Fml   : Formula being expanded
%   UnExp : List of formulae not yet expanded
%   Lits  : List of literals present on the current branch
%   FreeV : List of free variables on the branch (Prolog variables, possibly
%           bound to a term)
% VarLim : Upper bound for FreeV, used to initiate backtracking
%          The disprover stops its search if it has VarLim free variables on a
%          branch, and starts to backtrack. 
%
% Start with 
%
% disprove(Fml,[],[],[],VarLim)
%
% Succeed if Fml can be proven unsatisfiable without using more than VarLim
% free variables on each branch (path from root node to leaf), failure otherwise
% (i.e. either satisfiable or not enough resources -- can that be disentangled??)

% ---
% ***
% Needs a predicate which rewrites a formula into "Negation Normal Form"
% which is given in the second half of the paper, and which is a bit 
% larger than the prover itself.
% ***
% ---

% ---
% Alpha-Formula (the name for a conjunction as per Smullyan)
% Possible changes: Use a compound and/N for a conjunction of N subformulae
% ---

disprove((F1,F2),UnExp,Lits,FreeV,VarLim) :- 
  !,
  disprove(F1,[F2|UnExp],Lits,FreeV,VarLim).

% ---
% Beta-Formula (the name for a disjunction as per Smullyan)
% Possible changes: Use a compound or/N for a disjunction of N subformulae
% ---

disprove((F1;F2),UnExp,Lits,FreeV,VarLim) :- 
  !,
  disprove(F1,UnExp,Lits,FreeV,VarLim),
  disprove(F2,UnExp,Lits,FreeV,VarLim).

% ---
% Gamma-Formula (the name for an universally quantified formula)
% --- 

disprove(all(X,F),UnExp,Lits,FreeV,VarLim) :-
  !,
  \+length(FreeV,VarLim),                      % limit not reached, otherwise
                                               % fail, & backtrack over the 
                                               % two last clauses
  copy_term([X,F,FreeV],[X1,F1,FreeV]),        % create fresh variables for
                                               % all(X,F) but keep already seen
                                               % variables unique
  append(UnExp,[all(X,F)],UnExp1),             % append all(H,I) to UnExp
  disprove(F1,UnExp1,Lits,[X1|FreeV],VarLim).  % X1 is a new free variable on
                                               % this branch

% ---
% Closing a branch if the formula turns out to be a Literal
% i.e. determining that the branch cannot be satisfied because both a 
% Formula and its Negation appear on it. A "branch" is really a set
% of formulae, the size of which increases with the depth.
% (This code feels a bit inefficient).
% ---

disprove(Lit,_,[L|Lits],_,_) :-
   (Lit = -Neg; -Lit = Neg) 
   -> (unify_with_occurs_check(Neg,L) ; disprove(Lit,[],Lits,_,_)).

% ---
% Closing the branch failed.
% Add the current formula (a literal) to the list of literals on the branch
% and pick a formula waiting for expansion.
% ---

disprove(Lit,[Next|UnExp],Lits,FreeV,VarLim) :-
   disprove(Next,UnExp,[Lit|Lits],FreeV,VarLim).

% ---
% Wrapper for iterative deepening, calling disprove with higher and
% higher depth.
% ---

inc_disprove(Fml,VarLim) :- disprove(Fml,[],[],[],VarLim).
inc_disprove(Fml,VarLim) :- succ(VarLim,NewVarLim),inc_disprove(Fml,NewVarLim).

Ok, got a first version working. The first thing is to obtain the negation normal form. For more efficiency we replace positive and negative literals by a pos/1 and neg/1 wrapper:

% norm(+Form,-Norm)
norm(A, R) :- var(A), !, R = pos(A).
norm((A;B), R) :- !, norm(A, C), norm(B, D), R = or(C,D).
norm((A,B), R) :- !, norm(A, C), norm(B, D), R = and(C,D).
norm(all(A,B), R) :- !, norm(B, C), R = all(A,C).
norm(exist(A,B), R) :- !, norm(B, C), R = exist(A,C).
norm(-A, R) :- var(A), !, R = neg(A).
norm(- (A;B), R) :- !, norm(-A, C), norm(-B, D), R = and(C,D).
norm(- (A,B), R) :- !, norm(-A, C), norm(-B, D), R = or(C,D).
norm(- all(A,B), R) :- !, norm(-B, C), R = exist(A,C).
norm(- exist(A,B), R) :- !, norm(-B, C), R = all(A,C).
norm(- -A, R) :- !, norm(A, R).
norm(-A, R) :- !, R = neg(A).
norm(A, pos(A)).

The next step is simple, because we assume that the input formula has distinct variables. So we assume for example that the user does not input all(X,all(X,p(X)), but rather all(Y,all(X,p(X)):

% herbrand(+Norm, +List, +Integer, -Integer, -Herbrand)
herbrand(pos(A), _, N, N, pos(A)).
herbrand(neg(A), _, N, N, neg(A)).
herbrand(or(A,B), L, N, M, or(C,D)) :-
   herbrand(A, L, N, H, C),
   herbrand(B, L, H, M, D).
herbrand(and(A,B), L, N, M, and(C,D)) :-
   herbrand(A, L, N, H, C),
   herbrand(B, L, H, M, D).
herbrand(all(A,B), L, N, M, C) :-
   number_codes(N, R),
   atom_codes(F, [0'$|R]),
   A =.. [F|L],
   H is N+1,
   herbrand(B, L, H, M, C).
herbrand(exist(A,B), L, N, M, exist(A,C)) :-
   herbrand(B, [A|L], N, M, C).

The rest is then the prover from the abstract, using and/2 and or/2 instead. Further our implementation uses a different iterative deepening approach, so that we can better search for smaller proofs.

Testing is still ongoing, but we could already test Aristoteles syllogism test cases such as:

case(1, aristo_conversion1, (all(A, (b(A) -: -a(A))) -: all(B, (a(B) -: -b(B))))).
case(2, aristo_conversion2, (exist(A, (b(A), a(A))) -: exist(B, (a(B), b(B))))).
case(3, aristo_conversion3, (all(A, (b(A) -: a(A))), exist(B, b(B)) -: exist(C, (a(C), b(C))))).
case(4, barbara, (all(A, (b(A) -: a(A))), all(B, (c(B) -: b(B))) -: all(C, (c(C) -: a(C))))).
case(5, celarent, (all(A, (b(A) -: -a(A))), all(B, (c(B) -: b(B))) -: all(C, (c(C) -: -a(C))))).
Etc...

Running the test cases shows me the number of (∃C) rule applications. In total there are 21 test cases. They all pass!

?- show.
test 1 passed with 1 existential rule applications.
test 2 passed with 1 existential rule applications.
test 3 passed with 2 existential rule applications.
test 4 passed with 2 existential rule applications.
test 5 passed with 2 existential rule applications.
Etc..

I have named the file with the prover fitting.pl in honor of Melvin Fitting’s heroic 1990 book.

Source code:

Maslov Calculus over Herbrandisized Formulas
https://gist.github.com/jburse/820783d6e0fbfd55b907bdbe0e3e2c7e#file-fitting-pl

Aristoteles Test Cases from Isabelle/HOL
With Beckert and Posegga operators
https://gist.github.com/jburse/820783d6e0fbfd55b907bdbe0e3e2c7e#file-aristoteles-pl

Its also possible to implement the Beckert & Posegga's algorithm with the occurs check flag. We simply replace the following code line in our code:

prove(L, _, N, N) :- select(pos(A), L, R),
    member(neg(B), R),
    unify_with_occurs_check(A, B).

The unify_with_occurs_check/2 corresponds to the unify/2 call seen in the screenshot of the Beckert & Posegga's algorithm. When we use the occurs check flag, we can replace it by this code:

prove(L, _, N, N) :- select(pos(A), L, R),
    member(neg(A), R).

Here are some benchmark results, testing again the Aristoteles test suite for SWI-Prolog and Jekejeke Prolog. The explicit unify_with_occurs_check/2 is faster:

/* Jekejeke Prolog 1.4.7 */
?- time((between(1,100,_), test, fail; true)).
% Up 1,115 ms, GC 10 ms, Threads 1,102 ms (Current 02/05/21 12:36:51)
Yes
/* SWI-Prolog 8.3.18 */
?- time((between(1,100,_), test, fail; true)).
% 4,758,000 inferences, 0.354 CPU in 0.354 seconds (100% CPU, 13438628 Lips)
true.

The Prolog flag occurs_check is a slower. But SWI-Prolog has a much higher overhead than Jekejeke Prolog. I get for Jekejeke Prolog 1213/1115 = 109% and for SWI-Prolog 571/354 = 161%:

/* Jekejeke Prolog 1.4.7 */
?- time((between(1,100,_), test, fail; true)).
% Up 1,213 ms, GC 13 ms, Threads 1,197 ms (Current 02/05/21 12:36:46)
Yes
/* SWI-Prolog 8.3.18 */
?- time((between(1,100,_), test, fail; true)).
% 4,571,800 inferences, 0.570 CPU in 0.571 seconds (100% CPU, 8021222 Lips)
true.

Open source on gist:

Maslov Calculus over Herbrandisized Formulas
Explicit unify_with_occurs_check/2 call
file-fitting-pl

Maslov Calculus over Herbrandisized Formulas
Prolog flag occurs_check
file-fitting2-pl

Test Harness
file-aritstoteles-pl

Aristoteles Test Cases
file-koutsoukou-pl