🚀 go-pugleaf

I have a simple program that finds proofs of theorems of propositional
logics. The logics are formulated as sets of axiom schemes and the
modus ponens inference rule. The axiom schemes (like A->(B->A)) are
represented as terms with uninstantiated variables.
The program works by trying out alternative ways of deriving
a theorem from the axioms (using MP). In this process the theorem
(and other formulae - possibly with uninstantiated variables - to be proved)
are unified with parts of the axiom schemes: the occurs check is needed to
avoid circular bindings.

Question 1: What implementations of Prolog implement the occurs check?
(Our university has both Sicstus and NU-Prolog.)

================================================================
The program:

/* Copyright 1992 Jussi Rintanen, Helsinki University of Technology */

?- dynamic(axiom/2).
?- dynamic(premise/1).
?- dynamic(bymp/2).
?- dynamic(derivable/2).

%premise(p).
axiom(impl(A,impl(B,A)),k).
axiom(impl(impl(A,impl(B,G)),impl(impl(A,B),impl(A,G))),s).
axiom(impl(impl(not(A),not(B)),impl(impl(not(A),B),A)),c).

% these clauses, as well as the clauses for predicate hr, can be
% easily computed from the axioms
bymp(impl(_,A),[k,Pr]) :- derivable(A,Pr).
bymp(impl(impl(A,B),impl(A,G)),[s,Pr]) :- derivable(impl(A,impl(B,G)),Pr).
bymp(impl(A,G),[s,Pr1,Pr2]) :-
	derivable(impl(A,impl(B,G)),Pr1),
	derivable(impl(A,B),Pr2).
bymp(G,[s,Pr1,Pr2,Pr3]) :-
	derivable(impl(A,impl(B,G)),Pr1),
	derivable(impl(A,B),Pr2),
	derivable(A,Pr3).

bymp(A,[c,Pr1,Pr2]) :-
	derivable(impl(not(A),not(B)),Pr1),
	derivable(impl(not(A),B),Pr2).

bymp(impl(impl(not(A),B),A),[c,Pr]) :-
	derivable(impl(not(A),not(B)),Pr).

derivable(P,premise) :- premise(P).
derivable(P,ax(Ax)) :- axiom(P,Ax).
derivable(P,Proof) :- bymp(P,Proof).

%
% Iterative deepening

iterdeep(Goal,Answer,Depth) :-
	iterdeep(Goal,Depth),
	write('Answer in depth '), write(Depth), nl.

iterdeep(Goal,Answer,Depth) :-
	Depth1 is Depth + 1,
	iterdeep(Goal,Answer,Depth1).

iterdeep(Goal,N) :- N > 0,
	clause(Goal,Body),
	N0 is N - 1,
	eachclause(Body,N0).
eachclause(true,_) :- !.
eachclause((A,B),N) :- !, eachclause(A,N), eachclause(B,N).
eachclause(C,N) :- iterdeep(C,N).

%
proof(A,P) :- iterdeep(derivable(A,P),P,1).

%
hr(P,premise,[(L,P,'P')|X]-X,L) :- premise(P).
hr(P,ax(Ax),[(L,P,Ax)|X]-X,L) :- axiom(P,Ax).

hr(F,[AN,P1,P2,P3],Proof,L5) :-
	axiom(AF,AN), AF = impl(S1,impl(S2,impl(S3,F))),
	hr(S1,P1,Sp1,L1),
	hr(S2,P2,Sp2,L2),
	hr(S3,P3,Sp3,L3),
	conc(Sp1,Sp2,Sp12),
	conc(Sp12,Sp3,Sp123),
	conc(Sp123,[(L4,AF,AN),(L5,F,mp(L1,L2,L3,L4))|X]-X,Proof).

hr(F,[AN,P1,P2],Proof,L5) :-
	axiom(AF,AN), AF = impl(S1,impl(S2,F)),
	hr(S1,P1,Sp1,L1),
	hr(S2,P2,Sp2,L2),
	conc(Sp1,Sp2,Sp12),
	conc(Sp12,[(L4,AF,AN),(L5,F,mp(L1,L2,L4))|X]-X,Proof).

hr(F,[AN,P1],Proof,L5) :-
	axiom(AF,AN), AF = impl(S1,F),
	hr(S1,P1,Sp1,L1),
	conc(Sp1,[(L4,AF,AN),(L5,F,mp(L1,L4))|X]-X,Proof).

lnumber([],_).
lnumber([(N,_,_)|Ls],N) :- N1 is N + 1, lnumber(Ls,N1).

sh(Formula,Proof) :-
	hr(Formula,Proof,Tabular-[],_),
	lnumber(Tabular,1),
	pt(Tabular).

giveproof(F) :- proof(F,P), sh(F,P).

pt([]) :- nl.
pt([(A,B,C)|Ls]) :- write(A), write(' '), write(B), write(' '), write(C), nl,
	pt(Ls).

conc(A-B,B-C,A-C).