% Pure leanTAP: leanTAP in Horn-clause logic % % leanTAP is an elegant theorem prover for first-order logic based % on semantic tableaux. It was introduced in %% ;@article{ beckert95leantap, %% ; author = "Bernhard Beckert and Joachim Posegga", %% ; title = "{leanTAP}: Lean Tableau-based Deduction", %% ; journal = "Journal of Automated Reasoning", %% ; volume = "15", %% ; number = "3", %% ; pages = "339-358", %% ; year = "1995", %% ; url = "http://citeseer.ist.psu.edu/beckert95leantap.html" % % The original code contained cuts in almost every clause. In addition, % the code relied on copy_term/2. Cut and copy_term are extra-logical % facilities, which may lead to unsoundness. % % To avoid cuts, we modify the syntax of terms and formulas % and represent a term (f a) as [f a], a term b as [b], % a positive literal P(a,b) as % [+p,[a],[b]] and the negative literal NOT (P(a,b)) as [-p,[a],[b]]. % We represent universally quantified formula as usual: % all(X,[+p,X]) % VarLim is supposed to be an unary numeral such as [u,u,u,u] % All rules are disjoint here... prove((A,B), UnExp, Lits, VarLim) :- prove(A, [B|UnExp], Lits, VarLim). prove((A;B), UnExp, Lits, VarLim) :- prove(A, UnExp, Lits, VarLim), prove(B, UnExp, Lits, VarLim). prove(all(X,Body), UnExp, Lits, [u|VarLim]) :- X = w([_|_],X2), split_inst(Body,Body1,Body2), append(UnExp,[all(X2,Body2)],UnExp1), prove(Body1,UnExp1,Lits,VarLim). % Choice point here prove([L|Arg], _, Lits, _) :- negate(L,Lneg), member_s([Lneg|Arg],Lits). prove([L|Arg],[Next|UnExp],Lits,VarLim) :- prove(Next,UnExp,[[L|Arg]|Lits],VarLim). % negate a literal negate(+X,-X). negate(-X,+X). % member with a sound unification member_s(X,[Y|_]) :- unify_with_occurs_check(X,Y). member_s(X,[_|Y]) :- member_s(X,Y). % This is like copy_term, but implemented in Prolog itself split_inst((A,B),(A1,B1),(A2,B2)) :- split_inst(A,A1,A2), split_inst(B,B1,B2). split_inst((A;B),(A1;B1),(A2;B2)) :- split_inst(A,A1,A2), split_inst(B,B1,B2). split_inst([L|A],[L|A1],[L|A2]) :- split_inst_lst(A,A1,A2). split_inst(all(X,B),all(X1,B1),all(X2,B2)) :- X=w(X1,X2), split_inst(B,B1,B2). split_inst_lst([],[],[]). split_inst_lst([w(X1,X2)|T],[X1|T1],[X2|T2]) :- split_inst_lst(T,T1,T2). split_inst_lst([[L|A]|T],[[L|A1]|T1],[[L|A2]|T2]) :- split_inst_lst(A,A1,A2), split_inst_lst(T,T1,T2). ?- split_inst(all(X,all(Y,[p,X])),R1,R2). ?- split_inst(all(X,all(Y,[p,X,Y,X])),R1,R2). % allX P(X) & (~P(A);~P(B)) ?- prove(all(X,([+p,X],([-p,[a]];[-p,[b]]))),[],[],[u,u,u,u,u]). % X = w([a], w([b], _G435)) % we can see X must be instantiated twice. % simple tests % (Ax px) => (Ex px) % negated and normalized: (all(X,[+p,X]), all(X,[-p,X])) ?- prove((all(X,[+p,X]), all(X,[-p,X])),[],[],[u,u,u,u,u]). % X = w([_G320], _G318) % (Ex px) => (Ax px) -- invalid % negated and normalized: ([+p,[s1]], [-p,[s2]]) ?- prove(([+p,[s1]], [-p,[s2]]),[],[],[u,u,u,u,u]). % Pelletier Problem 18: Ey Ax ((f y) => (f x)) % Negation gives: Ay Ex (not ((not fy) or fx)) % or Ay Ex (fy and (not fx)) % Skolemizing % Ay (fy and (not (f (s y)))) ?- prove(all(Y, ([+f,Y], [-f,[s,Y]])),[],[],[u,u,u,u,u]). % Y = w([_G326|_G327], w([s, [_G326|_G327]], _G393)) %% Pelletier Problem 39: %% (not (Ex (Ay ((f y x) <=> (not (f y y)))))) % Negating and skolemizing % Ay (not fyS ; (not fyy)) , (fyy ; fyS) ?- prove(all(Y, (([-f,Y,[s]];[-f,Y,Y]), ([+f,Y,Y];[+f,Y,[s]]))),[],[],[u,u,u,u,u]). % Y = w([s], _G389) Contradiction achieved by instantiating Y to s. % Pelletier-35 % Ex Ey ((p x y) => (Ax (Ay (p x y)))) %% NNF is: (and (a x (a y (and (p x y) (not (p (sk (not (a y (p ex y)))) (sk (not (p (sk (not (a y (p ex y)))) ex))))))))) ?- prove(all(X,all(Y,([+p,X,Y],[-p,[s1],[s2]]))),[],[],[u,u,u,u,u]). % of course several solutions are possible... %% X = w([s1], _G354) %% Y = w(w([s2], _G429), _G362) ; %% ; %% X = w([_G356], w([s1], _G519)) %% Y = w(w([_G431], _G429), w(w([s2], _G597), _G527)) %------------------------------------------------------------------------ % Computing the negation normal form % We do skolemization a bit differently from Beckert and Posegga, % although the end result is equivalent. % When processing the formula ex(X,Fml), we instantiate X with a skolem % term of the form [pu,X1,X2 ,,, Xn] % where pu is a unique symbol, and X1, X2, ... Xn are % the variables that are free in ex(X,Fml). % When processing all(X,Fml), we unify X with w(Xnew) (where Xnew is % a free logic variable. Thus, all free variables in Fml have the form % w(Xnew), and so can be easily detected. % % We assume that in the original formula, all bound variables are represented % by distinct logic variables. That restriction can be lifted using % the technique from our lambda calculator in pure Prolog. % Without loss of purity, we shall use gensym to generate the unique % symbols for skolemization -- rather than thread a counter to build % such symbols. % more convenient syntax for the surface formulas ?- op(400,yfx,&). ?- op(500,yfx,v). ?- op(700,xfx,=>). ?- op(700,xfx,<=>). % All clauses are disjoin here % Tautologies nnf(-(-A), NNF,Paths) :- nnf(A, NNF,Paths). nnf(-all(X,F), NNF,Paths) :- nnf(ex(X,-F), NNF,Paths). nnf(-ex(X,F), NNF,Paths) :- nnf(all(X,-F), NNF,Paths). nnf(-(A v B), NNF,Paths) :- nnf(-A & -B, NNF,Paths). nnf(-(A & B), NNF,Paths) :- nnf(-A v -B, NNF,Paths). nnf((A => B), NNF,Paths) :- nnf(-A v B, NNF,Paths). nnf(-(A => B), NNF,Paths) :- nnf(A & -B, NNF,Paths). nnf((A <=> B), NNF,Paths) :- nnf((A & B) v (-A & -B), NNF,Paths). nnf(-(A <=> B), NNF,Paths) :- nnf((A & -B) v (-A & B), NNF,Paths). nnf(all(X,F),all(Xnew,NNF),Paths) :- X=w(Xnew), nnf(F,NNF,Paths). % skolemization nnf(ex(X,Fml),NNF,Paths) :- get_fv(ex(X,Fml),FV,ex(X1,Fml1)), gensym(sk,L), X1 = [L|FV], nnf(Fml1,NNF,Paths). nnf(A & B,(NNF1,NNF2),Paths) :- nnf(A,NNF1,Paths1), nnf(B,NNF2,Paths2), Paths is Paths1 * Paths2. nnf(A v B,NNF,Paths) :- nnf(A,NNF1,Paths1), nnf(B,NNF2,Paths2), Paths is Paths1 + Paths2, (Paths1 > Paths2, NNF = (NNF2;NNF1); Paths1 =< Paths2, NNF = (NNF1;NNF2)). nnf(-[L|A],[-L|AR],1) :- nnf_args(A,AR). nnf([L|A],[+L|AR],1) :- nnf_args(A,AR). % Now we unquote the free variables nnf_args([],[]). nnf_args([w(X)|T],[X|TR]) :- nnf_args(T,TR). nnf_args([[L|LA]|T],[[L|LR]|TR]) :- nnf_args(T,TR), nnf_args(LA,LR). % get_fv(F,FV,FR) % Given a formula F return the list of free variables in the formula. % All free variables have the form w(X) where X is a free logic variable. % As we traverse the formula F, we may need to instantiate variables % in the binding forms all(X,F) and ex(X,F). We instantiate these variables % as w1(Xnew), where Xnew is fresh. We `unquote' such variables (remove the % w1 wrapper) as we traverse the formula and its terms. % Therefore we must return a copy of the formula FR, where the logic % variables in all the bindings are free. get_fv(-A,FV,-AR) :- get_fv(A,FV,AR). get_fv(A v B,FV,AR v BR) :- get_fv(A,FVA,AR), get_fv(B,FVB,BR), append(FVA,FVB,FV). get_fv(A & B,FV,AR & BR) :- get_fv(A,FVA,AR), get_fv(B,FVB,BR), append(FVA,FVB,FV). get_fv(A => B,FV,AR => BR) :- get_fv(A,FVA,AR), get_fv(B,FVB,BR), append(FVA,FVB,FV). get_fv(A <=> B,FV,AR <=> BR) :- get_fv(A,FVA,AR), get_fv(B,FVB,BR), append(FVA,FVB,FV). get_fv(all(X,B),FV,all(Xnew,BR)) :- X = w1(Xnew), get_fv(B,FV,BR). get_fv(ex(X,B),FV,ex(Xnew,BR)) :- X = w1(Xnew), get_fv(B,FV,BR). get_fv([L|A],FV,[L|AR]) :- get_fv_args(A,FV,AR). % Traverse lists of terms and do the unquoting get_fv_args([],[],[]). get_fv_args([w(X)|T],[w(X)|FV],[w(X)|TR]) :- get_fv_args(T,FV,TR). get_fv_args([w1(X)|T],FV,[X|TR]) :- get_fv_args(T,FV,TR). get_fv_args([[L|LA]|T],FV,[[L|LR]|TR]) :- get_fv_args(T,FVT,TR), get_fv_args(LA,FVA,LR), append(FVA,FVT,FV). ?- get_fv(ex(X,([p,X] & all(Y,[q,X,Y]))),FV,R). % R = ex(_G325, [p, _G325]&all(_G339, [q, _G325, _G339])) ; % tests of normalization % (Ax px) => (Ex px) ?- nnf((all(X,[p,X]) => ex(Y,[p,Y])), R,_). % R = [-p, [sk4]];[+p, [sk5]] ; % negated and normalized: (all(X,[+p,X]), all(X,[-p,X])) ?- nnf(-(all(X,[p,X]) => ex(Y,[p,Y])), R,_). % R = all(_G319, [+p, _G319]), all(_G337, [-p, _G337]) ; % (Ex px) => (Ax px) -- invalid % negated and normalized: ([+p,[s1]], [-p,[s2]]) ?- nnf(-(ex(X,[p,X]) => all(Y,[p,Y])), R,_). % R = [+p, [sk6]], [-p, [sk7]] ; ?- nnf(all(Y,ex(X,[p,X,Y])), R,_). % R = all(_G301, [+p, [sk28, _G301], _G301]) ; % Pelletier-35 % Ex Ey ((p x y) => (Ax (Ay (p x y)))) ?- nnf(-(ex(X,ex(Y, [p,X,Y] => all(X1,all(Y1,[p,X1,Y1]))))), R,_). % R = all(_G373, all(_G383, ([+p, _G373, _G383], [-p, [sk30], [sk31]]))) ; %------------------------------------------------------------------------ % Complete prover: negating, normalizing, and proving fullprove(F,Limit) :- nnf(-F,FN,_), prove(FN,[],[],Limit). % simple tests % (Ax px) => (Ex px) ?- fullprove(all(X,[p,X]) => ex(Y,[p,Y]),[u,u,u,u,u]). % (Ex px) => (Ax px) -- invalid ?- fullprove(ex(Y,[p,Y]) => all(X,[p,X]),[u,u,u,u,u]). % Pelletier Problem 18: Ey Ax ((f y) => (f x)) ?- fullprove(ex(Y,all(X,[f,Y] => [f,X])),[u,u,u,u,u]). % Y = w(w([_G414|_G415], w([sk41, [_G414|_G415]], _G481))) % X = w1([sk41, w(w([_G414|_G415], w([sk41, [_G414|...]], _G481)))]) % Pelletier Problem 35 % Ex Ey ((p x y) => (Ax (Ay (p x y)))) ?- fullprove((ex(X,ex(Y, [p,X,Y] => all(X1,all(Y1,[p,X1,Y1]))))),[u,u,u,u,u]). % X = w(w([sk42], _G504)) % Y = w(w(w([sk43], _G579), _G512)) % Pelletier Problem 17: % ((p & (q => r)) => s) <=> % (((not p) v q v s) & ((not p) v (not r) v s)) ?- fullprove( (([p] & ([q] => [r])) => [s]) <=> (((- [p]) v [q] v [s]) & ((-[p]) v (-[r]) v [s])),[u,u,u,u,u]). % Pelletier Problem 19: % Ex Ay Az (((p y) => (q z)) => ((p x) => (q x))) ?- fullprove(ex(X,all(Y,all(Z, (([p,Y] => [q,Z]) => ([p,X] => [q,X]))))), [u,u,u,u,u]).