The main thing I have to say about it is hooray for tiny, adorable prolog programs that are easy to understand and modify. Didn't take me more than a half an hour I think to actually add in the stuff I wanted to the prover, and another little while to jot down the translation. Wasted a bunch of time trying to figure out how to convert and run the ILTP test suite and still haven't finished figuring that out, but I'm sure it can be done.

One one manual test, at least, namely proving the proposition

a => (a => a => a => a => b) => (a => a => a => a => c) => (b, c)(that comma is prolog for "and") it blows regular ileansep out of the water, replacing a ~10s time to proof to essentially 0s. What goes wrong in unfocused proof search is that you dither around removing copies of "a=>" from one or the other of the two hypotheses that have lots of them, and you try every possible interleaving of these removals, so that's like 8! = 40320 stupid different ways to try doing the thing that's going to succeed any way.

The focused prover is

*compelled*to first invert on the goal (b,c) (I notice ileansep has a notion of invertibility for which it smartly does a prolog-cut after decomposing an invertible connective to avoid backtracking it, but I don't think it does anything to prioritize decomposing invertible stuff first), and then discovers the suitability (respectively, unsuitability) of the assumption (a => a => a => a => b) for discharging the goal b (respectively, the goal c) in time linear in its size.

Anyway here's the code:

%% Hacked up version of ileansep by Jens Otten to support focused %% proof search via translation. %% See original at: www.leancop.de/ileansep/ %% Copyright: (c) 2005 by Jens Otten (modifications by Jason Reed) %% License: GNU General Public License :- op(1130, xfy, <=>). :- op(1110, xfy, =>). :- op(500, fy, ~). :- op( 500, fy, all). :- op( 500, fy, ex). :- op(500,xfy, :). :- op( 500, fy, uu). :- op(1110, xfy, -*). :- op(500, xfy, *). :- op(500, xfy, &). :- op(500, fy, ^). :- op(500, fy, v). cvtLeftNeg(P -* N, X, (Pc, Nc)) :- cvtRightPos(P, Pc), cvtLeftNeg(N, X, Nc). cvtLeftNeg(N1 & N2, X, (N1c; N2c)) :- cvtLeftPos(N1, X, N1c), cvtLeftPos(N2, X, N2c). cvtLeftNeg(@(X), Y, @(X, Y)). cvtLeftNeg(^ P, X, Pc) :- cvtLeftPos(P, #(X), Pc). cvtRightNeg(P -* N, Pc) :- cvtRightNeg(N, Nc), cvtLeftPos(P, Nc, Pc). cvtRightNeg(N1 & N2, (N1c, N2c)) :- cvtRightNeg(N1, N1c), cvtRightNeg(N2, N2c). cvtRightNeg(@(X), uu Y: @(X, Y)). cvtRightNeg(^ P, uu X: ff(X, Pc)) :- cvtRightPos(P, Pc). cvtLeftPos((P1; P2), A, (P1c, P2c)) :- cvtLeftPos(P1, A, P1c), cvtLeftPos(P2, A, P2c). cvtLeftPos((P1 * P2), A, P1c) :- cvtLeftPos(P2, A, P2c), cvtLeftPos(P1, P2c, P1c). cvtLeftPos(@(X), A, @(X) => A). cvtLeftPos(v N, A, (uu Y: Nc) => A) :- cvtLeftNeg(N, Y, Nc). cvtRightPos((P1; P2), (P1c; P2c)) :- cvtRightPos(P1, P1c), cvtRightPos(P2, P2c). cvtRightPos((P1 * P2), (P1c, P2c)) :- cvtRightPos(P1, P1c), cvtRightPos(P2, P2c). cvtRightPos(@(X), @(X)). cvtRightPos(v N, Nc) :- cvtRightNeg(N, Nc). %%% prove formula prove(F) :- Time1 is cputime, prove(F,1), Time2 is cputime, Time is Time2-Time1, print(Time). prove(F,VLim) :- display(VLim), nl, prove([],[F],l,[],VLim). prove(F,VLim) :- \+ no_mul([([F],0)]), VLim1 is VLim+1, prove(F,VLim1). provelim(F,VLim) :- display(VLim), nl, prove([],[F],l,[],VLim). %%% check multiplicities no_mul([]). no_mul([([F],Pol)|T]) :- (F=(A,B);F=(A;B)) -> !, no_mul([([A],Pol),([B],Pol)|T]). no_mul([([F],Pol)|T]) :- fml(F,Pol,_,L1,R1,L2,R2,_,_,V,U,U,_), !, V==[], no_mul([(L1,1),(R1,0),(L2,1),(R2,0)|T]). no_mul([_|T]):- no_mul(T). %%% specification of inference rules % fml(formula, polarity, invertible/noninvertible, add to left side % of 1st premise, right side of 1st premise, add to left side % of 2nd premise, right side of 2nd premise, position, free % variables, new free variable, term to be copied, copy of term, % thing the rhs must be right now) fml((A,B), 1,inv,[A,B], [], [], [], _, _,[], [], [], [] ). fml((A,B), 0,inv,[], [A],[], [B],_, _,[], [], [], [] ). fml((A;B), 1,inv,[A], [], [B],[], _, _,[], [], [], [] ). fml((A;_), 0,nin,[], [A],[], [], _, _,[], [], [], [] ). fml((_;B), 0,nin,[], [B],[], [], _, _,[], [], [], [] ). fml((A=>B), 1,nin,[(A=>B)], [C],[D],[], _, _,[!],A:B,C:D, []). fml((A=>B), 0,inv,[A], [B],[], [], _, _,[], [], [], [] ). fml((A<=>B),1,inv,[((A=>B),(B=>A))],[], [], [], _, _,[], [], [], [] ). fml((A<=>B),0,inv,[], [((A=>B),(B=>A))],[], [], _, _,[], [], [], [] ). fml((~A), 1,nin,[~A], [C],[], [], _, _,[!], A, C , [] ). fml((~A), 0,inv,[A], [], [], [], _, _,[], [], [], [] ). fml(all X:A,1,nin,[C,all X:A], [], [], [], _, _,[Y],X:A,Y:C,[] ). fml(all X:A,0,inv,[], [C],[], [], S,FV,[],(X,A),(S^FV,C),[] ). fml(ex X:A, 1,inv,[C], [], [], [], S,FV,[],(X,A),(S^FV,C),[] ). fml(ex X:A, 0,nin,[], [C],[], [], _, _,[Y],X:A,Y:C,[]). fml(uu X:A,1,nin,[uu X:A], [C], [], [], _, _,[Y],X:A,Y:C,[#(Y)]). fml(uu X:A,0,inv,[C], [#(S^FV)],[], [], S,FV,[],(X,A),(S^FV,C),[]). fml(ff(X,A),1,nin,[ff(X,A)], [C], [], [], _, _,[!], A, C , [#(X)] ). fml(ff(X,A),0,inv,[A], [#(X)], [], [], _, _,[], [], [], [] ). %%% proof search % prove(left side, right side, position, free variables, variable limit) prove(Left,Right,S,FreeV,VarLim) :- write_term(seq(Left, Right), []), nl, write_term(other(S, FreeV, VarLim), []), nl, ( (append(LeftA,[F|LeftB],Left), Pol=1, append(LeftA,LeftB,LeftP), RightP=Right ; [F]=Right, Pol=0, LeftP=Left, RightP=[]), fml(F,Pol,inv,L1,R1,L2,R2,S,FreeV,V,Cpy,Cpy1,RMust), ! ; (append(LeftA,[F|LeftB],Left), Pol=1, append(LeftA,LeftB,LeftP), RightP=Right ; [F]=Right, Pol=0, LeftP=Left, RightP=[]), fml(F,Pol,nin,L1,R1,L2,R2,S,FreeV,V,Cpy,Cpy1,RMust) ), % write_term(trying(F), []), nl, ( RMust=[] -> true ; % write_term(about_to_unify(Right, RMust), []), unify_with_occurs_check(Right, RMust) ), ( V=[] -> true ; \+ length(FreeV,VarLim) ), copy_term((Cpy,FreeV),(Cpy1,FreeV)), append(FreeV,V,FreeV1), append(LeftP,L1,Left1), ( R1=[] -> Right1=RightP ; Right1=R1 ), append(LeftP,L2,Left2), ( R2=[] -> Right2=RightP ; Right2=R2 ), prove(Left1,Right1,l(S),FreeV1,VarLim), ( L2=[],R2=[] -> true ; prove(Left2,Right2,r(S),FreeV1,VarLim) ). prove(Left,Right,_,_,_) :- member(F,Left), unify_with_occurs_check([F],Right).