Jason (jcreed) wrote,
Jason
jcreed

Fiddled around with ileansep today. I finally got in the mood try to get some empirical tests of the idea (which I've believed for some time) that you should be able to get a reasonable focused theorem prover out of an unfocused (first-order intuitionistic) one just by adding two specific "jumbo" connectives and translating focused propositions into the enlarged language.

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).
Tags: focusing, logic, math, theorem proving
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment