%%% %%% lolliCoP2 : a lean connection-method theorem prover %%% Lolli/LLP implementation of leanCoP %%% %%% Version : 1.0 %%% %%% Author : Naoyuki Tamura (tamura@kobe-u.ac.jp) %%% Joshua S. Hodas (hodas@cs.hmc.edu) %%% %%% lolliCoP http://www.cs.hmc.edu/~hodas/research/lollicop/ %%% Lolli http://www.cs.hmc.edu/~hodas/lolli/ %%% LLP http://bach.seg.kobe-u.ac.jp/llp/ %%% main :- read(f(Mat)), write('START lolliCoP2 1.0 '), nl, flush_output(user_output), prolog_flag(occurs_check, _, on), statistics(runtime, [T1|_]), (prove(Mat) -> write('OK ') ; write('NG ') ), statistics(runtime, [T2|_]), T is T2 - T1, write(T), nl. prove(Mat) :- reverse(Mat, Mat1), (ground(Mat1) -> propositional => pr(Mat1) ; pr(Mat1) ). pr([]) :- p(1). pr([Cla|Mat]) :- (ground(Cla) -> (forall [PathLim] \ cl(Cla, PathLim)) -<> pr(Mat) ; (forall [Cla1,PathLim] \ cl(Cla1, PathLim) :- PathLim > 0, copy_term(Cla, Cla1)) => pr(Mat) ). p(PathLim) :- cl(Cla1, PathLim), \+ member(-_, Cla1), prove(Cla1, PathLim). p(PathLim) :- \+ propositional, PathLim1 is PathLim + 1, p(PathLim1). prove([], _) :- erase. prove([Lit|Cla], PathLim) :- (-NegLit=Lit; -Lit=NegLit) -> ( path(NegLit), erase ; cl(Cla2, PathLim), append(ClaA, [NegLit|ClaB], Cla2), append(ClaA, ClaB, Cla3), PathLim1 is PathLim - 1, path(Lit) => prove(Cla3, PathLim1) ) & prove(Cla, PathLim). member(X, [X|_]). member(X, [_|L]) :- member(X, L). append([], Zs, Zs). append([X|Xs], Ys, [X|Zs]) :- append(Xs, Ys, Zs). reverse(Xs, Zs) :- reverse(Xs, [], Zs). reverse([], Zs, Zs). reverse([X|Xs], Ys, Zs) :- reverse(Xs, [X|Ys], Zs).