28:- [def_mm]. 29:- dynamic(pathlim/0), dynamic(lit/4). 30
31
33
34prove(F,Proof) :- prove2(F,[cut,comp(7)],Proof).
35
36prove2(F,Set,Proof) :-
37 (F=[_|_] -> M=F ; make_matrix(F,M,Set)),
38 retractall(lit(_,_,_,_)), (member([-(#)],M) -> S=conj ; S=pos),
39 assert_clauses(M,S), prove(1,Set,Proof).
40
41prove(PathLim,Set,Proof) :-
42 \+member(scut,Set) -> prove([-(#)],[],PathLim,[],Set,[Proof]) ;
43 lit(#,_,C,_) -> prove(C,[-(#)],PathLim,[],Set,Proof1),
44 Proof=[C|Proof1].
45prove(PathLim,Set,Proof) :-
46 member(comp(Limit),Set), PathLim=Limit -> prove(1,[],Proof) ;
47 (member(comp(_),Set);retract(pathlim)) ->
48 PathLim1 is PathLim+1, prove(PathLim1,Set,Proof).
49
51
52prove([],_,_,_,_,[]).
53
54prove([Lit|Cla],Path,PathLim,Lem,Set,Proof) :-
55 Proof=[[[NegLit|Cla1]|Proof1]|Proof2],
56 \+ (member(LitC,[Lit|Cla]), member(LitP,Path), LitC==LitP),
57 (-NegLit=Lit;-Lit=NegLit) ->
58 ( member(LitL,Lem), Lit==LitL, Cla1=[], Proof1=[]
59 ;
60 member(NegL,Path), unify_with_occurs_check(NegL,NegLit),
61 Cla1=[], Proof1=[]
62 ;
63 lit(NegLit,NegL,Cla1,Grnd1),
64 unify_with_occurs_check(NegL,NegLit),
65 ( Grnd1=g -> true ; length(Path,K), K<PathLim -> true ;
66 \+ pathlim -> assert(pathlim), fail ),
67 prove(Cla1,[Lit|Path],PathLim,Lem,Set,Proof1)
68 ),
69 ( member(cut,Set) -> ! ; true ),
70 prove(Cla,Path,PathLim,[Lit|Lem],Set,Proof2).
71
73
74assert_clauses([],_).
75assert_clauses([C|M],Set) :-
76 (Set\=conj, \+member(-_,C) -> C1=[#|C] ; C1=C),
77 (ground(C) -> G=g ; G=n), assert_clauses2(C1,[],G),
78 assert_clauses(M,Set).
79
80assert_clauses2([],_,_).
81assert_clauses2([L|C],C1,G) :-
82 assert_renvar([L],[L2]), append(C1,C,C2), append(C1,[L],C3),
83 assert(lit(L2,L,C2,G)), assert_clauses2(C,C3,G).
84
85assert_renvar([],[]).
86assert_renvar([F|FunL],[F1|FunL1]) :-
87 ( var(F) -> true ; F=..[Fu|Arg], assert_renvar(Arg,Arg1),
88 F1=..[Fu|Arg1] ), assert_renvar(FunL,FunL1).
89
90:- break.