%% Copyright 2008 Crip5 Dominique Pastre %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Muscadet version 3.0a %% %% 03 sep 2008 %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%% %% declarations %% %%%%%%%%%%%%%%%%%% :-dynamic hyp/3. :-dynamic hyp_treated/3. :-dynamic hyp_treated/2. :-dynamic or_applique/1. :-dynamic concl/3. :-dynamic link/2. :-dynamic subth/2. :-dynamic objet/2. :-dynamic rulactiv/2. :-dynamic rule/2. :-dynamic concept/1. :-dynamic fonction/2. :-dynamic type/2. :-dynamic withseulile/0. :-dynamic definition/2. :-dynamic definition1/2. %1. :-dynamic lemma/2. :-dynamic lemma1/2. :-dynamic version/1. :-dynamic write0buildrules/0. :-dynamic timelimit/1. :-dynamic tempspasse/1. :-dynamic conjecture/2. :-dynamic seulile/1. :-dynamic include/1. :-dynamic fof/3. :-dynamic fof_treated/3. :-multifile fof/3. :- dynamic problem/1. :- dynamic priority/2. :- dynamic prioritys/1. :- dynamic step/1. prioritys(with). problem(pas_encore_de_problem). timelimit(40). tempspasse(0). conjecture(no_conjecture,false). seulile(niouininot). withseulile. :-op(99,fx,'$'). :-op(100,fx,++). :-op(100,fx,--). :-op(100,xf,'!'). :-op(400,xfx,'..'). :-op(400,fx,!). :-op(400,fx,?). :-op(400,fx,^). :-op(400,fx,:=). :-op(405,xfx,'='). :-op(405,xfx,'~='). :-op(440,xfy,>). :-op(450,xfy,:). :-op(404,xfy,::). :-op(450,xfy,:=). :-op(450,fy,~). :-op(501,yfx,@). :-op(502,xfy,'|'). :-op(502,xfy,'~|'). :-op(502,xfy,'+'). :-op(503,xfy,&). :-op(503,xfy,~&). :-op(503,xfy,'*'). :-op(504,xfy,=>). :-op(504,xfy,<=). :-op(505,xfy,<=>). :-op(505,xfy,<~>). :- op(450,fx,..). :- op(600,fx,if). :- op(610,xfx,then). :- op(200,xfy,elt). l(rule(Nom)) :- clause(rule(_,Nom ),Q), assert(rr(rule(Nom),Q)), l(rr),retract(rr(_)). l(rule(_)) :- !. l(P) :- listing(P). ll(P) :- listingg(P). rule(Nom) :- clause(rule(_,Nom ),Q), write1(Q). applirulactiv(0) :- rulactiv(0,LR),write1(rulactiv-LR),fail. applirulactiv(N) :- repeat, ( concl(N, true, _) -> proved(N) ; concl(N, _/timeout, _) -> !, notproved(N) ; rulactiv(N,LR) -> ( applireg(N,LR)-> fail ;! ) ) . applireg(N,_) :- tempsdepasse(N),!,notproved(N),fail. applireg(N,[R|RR]) :- (rule(N,R ) -> write0_tirets([rule,R]) ; applireg(N,RR) ) . applireg(N,[]) :- notproved(N), fail. tempsdepasse(N) :- statistics(cputime,T),tempspasse(TP),timelimit(TL), TT is TP+TL , T>TT, concl(N,C, _), newconcl(N,C/timeout, _), write1('time over'-N-C), message('time over'-N-C), ! . proved(N) :- write1([theorem,N,proved]), ( N=0 -> ( version(tptp),conjecture(no_conjecture,_) -> message('no conjecture, problem montre insatisfaisable') ; concat_atom([theorem,N,proved],' ',ThNdem),message(ThNdem) ), ( version(casc)-> nl, (conjecture(no_conjecture,_) -> write('SZS status Unsatisfiable for ') ; write('SZS status Theorem for ') ), problem(P),write(P) ; true) ; true ) . notproved(N) :- write1([theorem,N,not,proved]), ( N=0 -> message('theorem not proved'), ( version(casc) -> nl, write('SZS status GaveUp for '), problem(P),write(P) ; true ) ; true), !. %%%%%%%%%%%%%%%%%%%%%%%%%% %% some functions %% %%%%%%%%%%%%%%%%%%%%%%%%%% varatom(X) :- (var(X);atom(X)). vars([X|L]) :- var(X), vars(L). vars([]). element(X,E) :- (X=E -> true ; E=[] -> fail ; E=[A|_], X == A -> true ; E=[A|_],\+ atom(A),\+ var(A),\+ number(A),element(X,A) -> true ; E=[_|L] -> element(X,L) ; E=..L -> element(X,L) ). element2(X,(X,_)). element2(X,(_,S)) :- element2(X,S). element2(X,X) :- \+ X=(_,_). suc(X,X1) :- name(X,L),sucliste(L,L1),name(X1,L1). sucliste(X,X1):- last(X,D), D>=48, D=<56,D1 is D+1, append(Y,[D],X), append(Y,[D1],X1),!. sucliste(X,X1) :- last(X,57),append(Y,[57],X),sucliste(Y,Y1), append(Y1,[48],X1),!. sucliste(X,X1):- append(X,[49],X1). ajoufin([X|L],A,[X|L1]) :- ajoufin(L,A,L1). ajoufin([],A,[A]). ajoufinseq(S,A,SA) :- ( S = (X,L) -> ajoufinseq(L,A,L1), SA = (X,L1) ; S = [] -> SA = A ; SA = (S,A) ). ajouseqavantobjet(S,A,SA) :- ( A = obj_cte(_,_) -> ajoufinseq(S,A,SA) ; S=(obj_cte(_,_),L) -> SA = (A,S) ; S = (X,L) -> ajouseqavantobjet(L,A,L1), SA = (X,L1) ; S = [] -> SA = A ; S = obj_cte(_,_) -> SA = (A,S) ; SA = (S,A) ) . obj_cte(N,X) :- objet(N,X) ; objet(-1,X). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% affecter(X) :- X =.. [P,_],Y=..[P,_],retractall(Y),assert(X). affecter(X) :- X =.. [P,_,_],Y=..[P,_,_],retractall(Y),assert(X). affecter(X) :- X =.. [P,_,_,_],Y=..[P,_,_,_],retractall(Y),assert(X). oter(_,_,_) :- timeover_ltb(oter). oter(X,[X|L],L) :- !. oter(X,[Y|L],[Y|L1]) :- oter(X,L,L1),!. oter(_,[],[]). clos(E) :- not(var(E)), ( E=[] -> true ; E=[X|L] -> clos(X),clos(L) ; E=(![X|XX]:EX) -> replace(EX,X,x,Exx), ( XX=[] -> Ex=Exx ; Ex=(!XX:Exx) ), clos(Ex) ; E=(?[X|XX]:EX) -> replace(EX,X,x,Exx), ( XX=[] -> Ex=Exx ; Ex=(?XX:Exx) ), clos(Ex) ; E=only(FX::X,PX) -> clos(FX),replace(PX,X,x,Px),clos(Px) ; E=..[_|L]-> clos(L) ; write1(clos-E-not) ). :- dynamic file/1. telll(F) :- tell(F), retractall(file(_)), assert(file(F)). toldd :- retractall(file(_)),told. tellling(F) :- file(F),!. tellling(user). appendd(F) :- append(F), retractall(file(_)), assert(file(F)). listingg(Pred) :- Tete =.. [Pred], clause(Tete,Corps), write1(Tete:-Corps),fail. listingg(Pred) :- Tete =.. [Pred,_], clause(Tete,Corps), write1(Tete:-Corps),fail. listingg(Pred) :- Tete =.. [Pred,_,_], clause(Tete,Corps), write1(Tete:-Corps),fail. listingg(Pred) :- Tete =.. [Pred,_,_,_], clause(Tete,Corps), write1(Tete:-Corps),fail. listingg(Pred) :- Tete =.. [Pred,_,_,_,_,_], clause(Tete,Corps), write1(Tete:-Corps),fail. listingg(_Pred). travail1 :- verifdef,elifundef, buildrules, typesdonnees, told. typesdonnees :- clause(rule(_,Nom),_), \+ type(Nom,_), assert(type(Nom,donnee)),fail. typesdonnees. prove(Theoreme) :- (version(th) -> effacertout ; true), ( version(casc) -> true %; shell('echo `hostname -s`\. > zzzmachine;echo >> zzzmachine'), ; shell('echo `hostname`\. > zzzmachine;echo >> zzzmachine'), see(zzzmachine),read(HostName),seen, write1(machine:HostName), message(HostName) ), write1('****************************************'), write0('****************************************'), ( version(casc) -> true ; write1(['theorem to be proved']), write1([Theoreme]) ), affecter(step(0)), newconcl(0 , Theoreme, E/**/), traces(0, action(ini), [], newconcl(0 , Theoreme, E), E,'initial theorem',[] ), activreg, applirulactiv(0 ), told, ! . createsubth(N,N1,A,E) :- assert(subth(N,N1)), ligne,write1([************************************************]), write0([sub-theorem, N1,*****]), newconcl(N1,A,E ), copitem(N,N1). prove_conj(N,C,Econj, Efin) :- ( C = (A & B) | (C = A , B=true) ), atom_concat(N,-,N0), gensym(N0,N1), createsubth(N,N1,A,Ecreationsubth), (B=true -> Cond=[], Expli='proof of the last element of the conjunction' ; Cond=concl(N, C, Econj), Expli='to prove a conjunction, prove all the elements of the conjunction'), traces(N1,action(prove_conj), Cond, %(concl( C/*, Econj*/)), [createsubth(N,N1,A,Ecreationsubth), newconcl(N1,A,Ecreationsubth)], (Ecreationsubth), Expli, ([Econj])), write0_tirets([action,prove_conj]), applirulactiv(N1), !, concl(N1,true,Edemsubth), newconcl(N,B,Eretourth), traces(N, action(return_proof), concl(N1,true,Edemsubth), newconcl(N,B,Eretourth), (Eretourth), ['the conclusion',A, 'of (sub)theorem',N, 'has been proved ( subtheorem',N1,')'], ([Econj , Ecreationsubth,Edemsubth]) ), write0_tirets([action,return_proof]), ( B = true -> Eretourth=Efin ; prove_conj(N,B,Eretourth,Efin) ) . demdij(N,C,Edij, Efin) :- ( C = (A | B) | (C = A , B=true) ), atom_concat(N,+,N0), gensym(N0,N1), createsubth(N,N1,A,Ecreationsubth), traces(N,action(demdij),(concl(N, C, Edij)), createsubth(N,N1,A,Ecreationsubth), (Ecreationsubth), ['creation of subtheorem',N1,'with conclusion',A], ([Edij])), write0_tirets([action,demdij]), applirulactiv(N1), !, concl(N1,C1,Edemsubth), ( C1=true -> newconcl(N,true,Eretourth), traces(N, action(return_proofdij), (subthdem), newconcl(N,true,Eretourth), (Eretourth), ['the conclusion',A, 'of (sub)theorem',N, 'has been proved'], ([Edij , Edemsubth]) ), write0_tirets([action,return_proofdij]) ; B \=true -> write0_tirets([action,return_proofdij]), write1('on eie al disjonction suivante'), demdij(N,B,Edij,Efin) ; write1('la disjonction n\'a pas ete provede') ) . retirer(A, C, C1) :- ( C = (A1 & B1 & B2), A =@= A1 -> C1 = (B1 & B2) ; C = (A1 & B) , A =@= A1 -> C1 = B ; C = (B & A1), A =@= A1 -> C1 = B ; A =@= C -> C1 = true ; C = (D & E) -> retirer(A, E, E1),C1 = (D & E1) ; write1([on, n, a, pas, trouve, A, in, C, pour, le, retirer]) ) . copitem(N,M) :- hyp(N, H,I), assert(hyp(M,H,I/**/)) /* pas de message */, fail. copitem(N,M) :- hyp_treated(N, H,E), assert(hyp_treated(M,H,E),E) , fail. copitem(N,M) :- objet(N, H), assert(objet(M,H)) ,fail. copitem(N,M) :- rulactiv(N, LR), assert(rulactiv(M,LR)), fail. copitem(_, _) . proveconclexi(N, ? [X|XX]:C, Eexi, Efin):- obj_cte(N,Ob), write1(['*** on essaie',Ob,'***']), atom_concat(N,+,N0), gensym(N0,N1), replace(C,X,Ob,C0), ( XX=[] -> C1=C0 ; C1= (?XX:C0)), createsubth(N,N1,C1,Ecreationsubth), traces(N1, action(proveconclexi), concl(N, ? [X]:C, Eexi), [createsubth(N,N1,C1,Ecreationsubth), newconcl(N1,C1,Ecreationsubth)], Ecreationsubth, [Ob,'is tried for the existential variable'], [Eexi] ), write0_tirets([action,proveconclexi]), write1('++++++++++= prove'-C1), applirulactiv(N1), ( concl(N1, true, E1) -> newconcl(N,true,Efin), traces(N, action(return_proofexi), concl(N1, true, E1), newconcl(N,true, Efin), Efin, ['la conclusion du (sub-)theorem',N, 'has been proved (sub-theorem',N1,')'], [Eexi, E1] ) ; write1('on essaie l\'objet suivant'),fail ). newconcl(N,C, E2) :- \+ concl(N, C, _), (step(E1),var(E2) -> E2 is E1+1, affecter(step(E2)) ; true), retractall(concl(N,_,_)),assert(concl(N,C,E2/**/)), write1([E2:N,newconcl(C)]). addhyp(N, H, E2) :- (var(E2) -> step(E1), E2 is E1+1, affecter(step(E2));true), ( H = (A & B) -> addhyp(N, A, E2), addhyp(N,B, E2) ; hyp(N, H,_) -> true ; H =(X,A) -> ( var(I1) -> step(I), I1 is I+1, affecter(step(I1)) ; true), assert(hyp(N,H,I1)), create_objet(N,z,X1), replace(A,X,X1,A1), addhyp(N,A1,I1) ; H = (Y=X), atom(X), atom(Y), avant(X,Y), addhyp(N,(X=Y),E2) ; H = (..[R, X, Y]) -> (H1 =..[R, X, Y]), addhyp(N, H1, E2) ; H = (..[F, X]::Y) -> (Y1 =..[F, X]), addhyp(N, Y1:Y, E2) ; H=only(A::X,Y)-> ( hyp(N,A::X1,_I) -> write1([replace,X,par,X1,in,Y]), replace(Y,X,X1,Y1),addhyp(N,Y1,E2 ), write1ettrace(N,'', addhyp(N,Y1,I1),addhyponly) ; create_objet(N,z,X1),addhyp(N,A::X1, E2 ), replace(Y,X,X1,Y1),addhyp(N,Y1, E2 ), write1ettrace(N,'', addhyp(N,A::X1 & Y1, I1),addhyponly) )%, ; H = (~ only(FX::Y,P)) -> addhyp(N,only(FX::Y, ~ P ), E2) ; H = (!_: _) -> ( var(E2) -> step(E0), E2 is E0+1, affecter(step(E2)) ; true), atom_concat(rulhyp__,E2,ReghypE2), atom_concat(ReghypE2,'__',Reghyp), write1([E2:N,'treat l\'hypothesis universelle',H]), create_nom_rule(Reghyp,Nom), buildrules(H, _,Nomfof,N+H,Nom,[],[E2]), Imoins1 is E2-1, write1ettrace(N,hyp(N,'',Imoins1),addhyp(N,H,I1), I1) ; H = (~ (?XX:A)) -> create_nom_rule(rulhyp,Nom), buildrules( (!XX:(~ A)), _, Nomfof, N+H, Nom, [],[]) ; H = (A =>B) -> create_nom_rule(rulhyp,Nom), buildrules( H,_,Nomfof,N+H,Nom,[],[]) ; ( var(E2) -> step(E0), E2 is E0+1, affecter(step(E2)) ; true), assert(hyp(N, H,E2)), write1([E2:N,addhyp(H)]), (H=p(X) -> ajobjet(N,X) ; H=q(X) -> ajobjet(N,X) ; true) ) . avant(Z1,Z2) :- ( name(Z1,[122|L1]), name(N1,L1), number(N1), name(Z2,[122|L2]), name(N2,L2), number(N2) -> N1 true ; assert(objet(N, X)), (N=(-1)-> true ; step(E), write1([E:N, add,objet,X])) ) . ajconcept(P) :- (concept(P) -> true; assert(concept(P))). ajfonction(F,N) :- (fonction(F,N)-> true;assert(fonction(F,N))). buildrules :- effacer_regcons,fail. buildrules :- definition(Nomfof,A<=> ~ B), A=..[P|L], vars(L), ajconcept(P), atom_concat(not,P,NonP),ajconcept(NonP), NonA =.. [NonP|L], \+ NonA = B, asserta(definition(Nomfof,A <=> ~ NonA)),asserta(definition(Nomfof,NonA <=> B)), create_nom_rule(P,Nom), assert((rule(_,Nom):- hyp(N,~ A,I), \+ hyp(N,NonA,_), addhyp(N,NonA,_), traces(N,rule(Nom), hyp(N,~ A,I), addhyp(N,NonA,E),E, ['because',P,and,notP], [I] ) )), assert(type(Nom,P)), fail. buildrules :- definition(Nomfof, A<=>B), not(var(A)), ( A=(C::_) -> C =..[P|_] ; A=..[_,_,E],not(var(E)),E=..[_|_] -> fail ; A=..[P|_] ), ajconcept(P), create_nom_rule(P,Nom), (A=(X=Y)-> replace(B,Y,X,B1),buildrules(B1,N,Nomfof,P,Nom,objet(N,X),[]) ; buildrules(A=>B,_,Nomfof,P,Nom,[],[]), (write0buildrules -> write1('+++buildrules contraposee'/A=>B);true), (B = (_ | _) -> buildrules(B=>A,_,Nomfof,P,Nom,[],[]);true) ), fail. buildrules :- definition(Nomfof,A=B), not(B=[_,_]), A =.. [F|_], ajconcept(F), create_nom_rule(F,Nom), elifun4(B::X,B1X), buildrules(A::X => B1X,_,Nomfof,F,Nom,[],[]), fail. buildrules :- definition(Nomfof,A<=>D), ( A =..[R,X,E],not(var(E)),E=..[F|_] ) , ajconcept(F), create_nom_rule(F,Nom), ( atom(E) -> buildrules((!XX:(A =>D)),_,Nomfof,F,Nom,[],[]) ; XappW =.. [R,X,W],buildrules((E::W)=>!XX:(XappW <=>D),_,Nomfof,F,Nom,[],[]) ), fail. buildrules :- lemma(Nomfof,E),atom_concat(Nomfof,'_',Nom0), create_nom_rule(Nom0,Nom1), buildrules(E,_,Nomfof,lemma,Nom1,[],[]), fail. buildrules. buildrules(E,N,Concept,Nom,Cond,An):- write1(reste_buildrules_a_6_arg), write1([buildrules,'\n','Concept'=Concept, '\n','Nom '=Nom, '\n','N '=N, '\n','Cond '=Cond, '\n','E '=E, '\n','An '=An]), fail. buildrules(E,N,Nomfof,Concept,Nom,Cond,Antecedants):- write0buildrules, nl, write1([buildrules,'\n','Concept'=Concept, '\n','Nomfof '=Nomfof, '\n','Nom '=Nom, '\n','N '=N, '\n','Cond '=Cond, '\n','Antecedants'=Antecedants, '\n','E '=E]), fail. buildrules(E,N,Nomfof,Concept,Nom,Cond,Antecedants) :- \+ timeover_ltb(buildrules), ( E = (A | B => C) -> buildrules((A=>C)&(B=>C),N,Nomfof,Concept,Nom,Cond,Antecedants) ; E = ((X=Y) => C), (var(X) | var(Y)) -> ( var(X) -> replace(Cond,X,Y,Cond1), replace(C,X,Y,C1) ; var(Y) -> replace(Cond,Y,X,Cond1), replace(C,Y,X,C1) ), buildrules(C1,N,Nomfof,Concept,Nom,Cond1,Antecedants) ; E = (~ D => B) -> ajoucond(N,Cond,Antecedants, ~ D, Cond1,Antecedants1), buildrules(B, N, Nomfof,Concept, Nom, Cond1,Antecedants1), create_nom_rule(Nom, Nom1), buildrules(D | B, N, Nomfof,Concept,Nom1,Cond,Antecedants) ; E = (~ D & A1 =>B) -> ajoucond(N,Cond,Antecedants,~ D,Cond1,Antecedants1), buildrules(A1 => B,N,Nomfof,Concept,Nom,Cond1,Antecedants1), create_nom_rule(Nom, Nom1), buildrules(A1 => D | B, N, Nomfof,Concept,Nom1,Cond,Antecedants) ; E = (A1 & A2 => B) -> buildrules(A1 => (A2 => B),N,Nomfof,Concept,Nom,Cond,Antecedants) ; E = (A => B), A = (!_:_) -> ajouseqavantobjet(Cond,concl(N,B,I),Cond1), ajoufinseq(Cond1,newconcl(N,A,I1),CondAct2), atom_concat(Nom, '_cs', Nom_cs), ajoufinseq(CondAct2, traces(N,rule(Nom_cs), concl(N,B,I), newconcl(N,A,I1), I1, 'sufficient condition', [I]), Regle), ajoureg(N, Concept, Nom_cs, Regle) , create_nom_rule(Nom, Nom1), atom_concat(Nom1, cs_endernier, Nom_cs_endernier), ajouseqavantobjet(Cond, %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% (concl(N,C,II),hyp(N,H,I2),not(atom(C)),functor(C,Q,_), not(atom(H)),functor(H,Q,_), clos(A), newconcl(N,A &(B=>C),II1)), CondAct4), append(Antecedants,[I2,II],An1), ajoufinseq(CondAct4, traces(N,rule(Nom_cs_endernier), Cond+concl(N,C,II)+hyp(N,H,_)+averifier, newconcl(N,A & (B=>C),II1), II1, 'sufficient condition', An1 ), Regle2), ajoureg(N, endernier, Nom_cs_endernier, Regle2) ; E = (A=>B) -> ajoucond(N,Cond,Antecedants,A,Cond1,Antecedants1), buildrules(B,N,Nomfof,Concept,Nom,Cond1,Antecedants1) ; E = (A<=>B) -> buildrules((A=>B)&(B=>A),N,Nomfof,Concept,Nom,Cond,Antecedants) ; E = (A & B) -> create_nom_rule(Nom, Nom1),buildrules(A,N,Nomfof,Concept,Nom1,Cond,Antecedants), create_nom_rule(Nom1, Nom2),buildrules(B,N,Nomfof,Concept,Nom2,Cond,Antecedants) ; E = (![X]:B),(var(X); atom(X)) -> ajoucond(N,Cond,Antecedants,objet(N,X),Cond1,Antecedants1), buildrules(B,N,Nomfof,Concept,Nom,Cond1,Antecedants) ; E = (![X|XX]:B),(var(X); atom(X)) -> ajoucond(N,Cond,Antecedants,objet(N,X),Cond1,Antecedants1), buildrules(!XX:B,N,Nomfof,Concept,Nom,Cond1,Antecedants) ; E = only(FX::Y, B) -> ajoucond(N,Cond,Antecedants,FX::Y,Cond1,Antecedants1), buildrules(B,N,Nomfof,Concept,Nom,Cond1,Antecedants1), ( seulile(oui),seulile(not)->true ; seulile(not)-> true ; seulile(oui) -> atom_concat(Nom, '_crea_only', Nom2), create_nom_rule(Nom2, Nom1), ajouseqavantobjet(Cond, \+ hyp(N,FX::Y,_), Cond3), buildrules((?[Y]:((FX::Y) & B)),N,Nomfof,Concept,Nom1,Cond3,Antecedants) ; true ) ; E = (~ (?[X]:A)) -> buildrules((![X]:(~ A)),N,Nomfof,Concept,Nom,Cond,Antecedants) ; E = (~ ~ A) -> buildrules(A,N,Nomfof,Concept,Nom,Cond,Antecedants) ; E = (~ A), \+(A=(!_:_)) -> ajoucond(N, Cond, Antecedants,A, Cond1,Antecedants1), buildrules(false,N,Nomfof,Concept,Nom,Cond1,Antecedants1) %; E = (~ A), \+ A = (_=_) -> ajoucond(N, Cond, Antecedants,A, Cond1,Antecedants1), ; E = (_=_) -> Cond=Cond0, ajoufinseq(Cond, \+ E, Cond1), ajoufinseq(Cond1, addhyp(N,E,I1), CondAct2), Act=addhyp(N,E,I1), (Cond0=[] -> SiAlorsAct=Act;SiAlorsAct=(if Cond0 then Act)), copy_term(SiAlorsAct,SiAlorsActCop), ( Concept=(_ + HypUnivImp) ->affecter(zut(HypUnivImp)), zut(HypU), Expli = ['local rule\n',SiAlorsActCop, '\n(rule built from the universal hypothesis', HypU,')'] ; Concept=lemma -> Expli = [rule,SiAlorsActCop, 'built from the axiom', Nom,'(fof',Nomfof,')'] ; Expli= [rule,SiAlorsActCop, '\nbuilt from the definition of',Concept, '(fof',Nomfof,')'] ), ajoufinseq(CondAct2, traces(N,rule(Nom), Cond0, addhyp(N,E,I1),I1, Expli, Antecedants ), Regle), ajoureg(N, Concept, Nom, Regle) ; E = (Z::Y), \+ var(Z), Z= (..[F,X]) -> sup_objet(Cond,Cond0), ajoufinseq(Cond,T=..[F,X],C1), ajoufinseq(C1,\+hyp(N,T::Y,_),C2), ajoufinseq(C2, addhyp(N,T::Y,I1),CondAct3), ajoufinseq(CondAct3, traces(N,rule(Nom), Cond0, addhyp(N,E,I1),I1, ['because of',Concept], Antecedants ), Regle ), ajoureg(N, Concept, Nom, Regle) ; E = (..[R,X,Y]) -> sup_objet(Cond,Cond0), ajouseqavantobjet(Cond,T=..[R,X,Y],C1), ajoufinseq(C1,\+hyp(N,T,_),C2), ajoufinseq(C2, addhyp(N,T,I1),CondAct3), ajoufinseq(CondAct3, trace(N,rule(Nom), Cond0, addhyp(N,E,I1),I1, ['because of',Concept], Antecedants ), Regle ), ajoureg(N, Concept, Nom, Regle) ; E = (A | B),definition(Nomfof,A <=> ~ A1), A =..[_|L],vars(L), A1 =..[_|_] -> write1('buildrules or1 not Nom/E'=Nom/E), sup_objet(Cond,Cond0), ajoufinseq(Cond, \+ hyp(N,E,_), Cond1) , ajoufinseq(Cond1, addhyp(N,E,I1), CondAct2), atom_concat(Nom, ounotpourquoi, Nom11), create_nom_rule(Nom11,Nom1), ajoufinseq(CondAct2, write1ettrace(N,Cond,addhyp(N,E,I1),Nom1),Regle), ajoureg(N, Concept, Nom1, Regle), ajoufinseq(Cond, A1, Cond3), ajoufinseq(Cond3, traces(N,rule(Nom1), Cond,addhyp(N,E,I1),I1, ['because of',Concept], Antecedants ), Regle2 ), buildrules(B,N,Nomfof,Concept,Nom1,Regle2,Antecedants) ; E = (B | A),definition(Nomfof,A <=> ~ A1), A =..[_|L],vars(L), A1 =..[_|_] -> write1('buildrules or2 not Nom/E'=Nom/E), sup_objet(Cond,Cond0), ajoufinseq(Cond, \+ hyp(N,E,_), Cond1) , ajoufinseq(Cond1, addhyp(N,E,I1), CondAct2), atom_concat(Nom, ounotpourquoi, Nom11), create_nom_rule(Nom11,Nom1), ajoufinseq(CondAct2, traces(N,rule(Nom1), Cond0,addhyp(N,E,I1),I1, ['because of',Concept], Antecedants ), Regle1 ), ajoureg(N, Concept, Nom1, Regle1), ajouseqavantobjet(Cond, A1, Cond3), ajoufinseq(Cond3, traces(N,rule(Nom1), Cond,addhyp(N,E,EE),EE, ['because of',Concept], Antecedants ), Regle2 ), buildrules(B,N,Nomfof,Concept,Nom1,Regle2,Antecedants) ; Cond=Cond0, ajoufinseq(Cond, \+ hyp(N,E,_), Cond1), Act=addhyp(N,E,I1), %Act_simpli=addhyp(E), ajoufinseq(Cond1, Act , CondAct2), ( E = (?_:_) -> Priorite = 2, atom_concat(Nom, existe, Nom1) ; E = (_ | _) -> Priorite = 2, atom_concat(Nom, or, Nom1) ; Nom = Nom1, Priorite = 1), create_nom_rule(Nom1,Nom2), assert(priority(Nom2,Priorite)), (Cond0=[] -> SiAlorsAct=Act;SiAlorsAct=(if Cond0 then Act)), copy_term(SiAlorsAct,SiAlorsActCop), ( Concept=(_ + HypUnivImp) ->affecter(zut(HypUnivImp)), zut(HypU), Expli = ['local rule2\n',SiAlorsActCop, '\n(rule built from the universal hypothesis',HypU] ; Concept=lemma -> Expli = [rule2,SiAlorsActCop, '\nbuilt from the axiom', Nomfof] ; Expli= [rule2,SiAlorsActCop, '\nbuilt from the definition of',Concept, '(fof',Nomfof,')']), ajoufinseq(CondAct2, traces(N,rule(Nom2),Cond0,addhyp(N,E,I1),I1, Expli, Antecedants), Regle ), ( E = false, atom(Concept) -> assert(type(Nom2,enpremier)), Type= enpremier ; Type = Concept), ajoureg(N, Concept , Nom2, Regle)%, ). sup_objet((X,L),L1) :- (X = obj_cte(_,_)|X=objet(_,_)), sup_objet(L,L1),!. sup_objet((X,L),X) :- sup_objet(L,[]),!. sup_objet((X,L),(X,L1)) :- sup_objet(L,L1),!. sup_objet(X,[]) :- (X = obj_cte(_,_)|X=objet(_,_)), !. sup_objet(X,X). ajoucond(_,C,A,_) :- write1(appel_ajoucond/4-'C'/C-'\nA'/A). ajoucond(N,C,An,A,CA,AnA) :- ( var(A) -> ajoufinseq(C,hyp(N,A,_),CA) ; A = (A1 & A2) -> ajoucond(N,C,An,A1,C1,An1), ajoucond(N,C1,An1,A2,CA,AnA) ; A = (?_:B) -> ajoucond(N,C,An, B, CA,AnA) ; A = only(FX::Y,B) -> ajoucond(N,C,An,FX::Y,CB,AnB), ajoucond(N,CB,AnB,B,CA,AnA) ; A = (B=D), (var(B);var(D)) -> ajoufinseq(C,A,CA), AnA=An % ; A = (B=D), (var(B) ; var(C)) -> write1('??????????B=Dbis') ; A = (..[F,X]::Y) -> ajouseqavantobjet(C,T=..[F,X],C1), ajouseqavantobjet(C1,hyp(N,T::Y,_),CA) ; A = (..[R,X,Y]) -> ajouseqavantobjet(C,T=..[R,X,Y],C1), ajoucond(N,C1,An,T,CA,AnA) ; A = objet(N,X) -> ajoufinseq(C,obj_cte(N,X),CA), AnA=An ; A = (!_:_) -> fail ; A = (~ only(FX::Y,P)) -> ajoucond(N,C,An,only(FX::Y,~ P),CA,AnA) ; ajouseqavantobjet(C,hyp(N,A,Etape),CA), ajoufin(An,Etape,AnA) ) . ajoureg(N, Arg, Nom, Corps) :- sup_cond_equal(Corps, Corps0), (write0buildrules -> nl,write1('apres sup_cond_equal'-Corps0);true), ( Arg=(Nsth+H) -> step(E),assert(rulehypuniv(Nom,H,E)), ajoureglocale(Nsth,(rule(N,Nom):-Corps0), Nom) ; assert((rule(N,Nom) :- Corps0)), assert(type(Nom,Arg)), (Nom=disjoint -> message(ajouregdisjoint-Corps0) ;true) ). numberth(N) :- atom_concat(0,_,N). sup_cond_equal(Corps,Corps0) :- ( sup_equal(X=Y,Corps, Corps1) -> ( var(X) -> replace(Corps1,X,Y,Corps2) ; var(Y) -> replace(Corps1,Y,X,Corps2) ), sup_cond_equal(Corps2,Corps0) ; Corps0=Corps ). sup_equal(X=Y,(X=Y,L),L) :- !. sup_equal(X,(Y,L),(Y,L1)) :- sup_equal(X,L,L1),!. sup_equal(X=Y,X=Y,[]) :- ! . ajoureglocale(Arg,R, Nom) :- rulactiv(Arg,LR), R= (rule(_,Nom):-Corps), step(E), write1([E:Arg,'add the local rule']), write0(R), write1('at the end of universal rules'),ligne, assert(type(Nom,Arg)), rules_univ(LRU),append(LRU,LRNU,LR), ( compareg(Corps,LRNU,L2,R3,L3) -> append([R3,Nom|L2],L3,NLR), write1([and,put,R3,avant]),ligne ; NLRNU=[Nom|LRNU] ), append(LRU,NLRNU,NLR), retract(rulactiv(Arg,LR)), assert(rulactiv(Arg,NLR)), assert(R),!. desactiver(N,Nom) :- rulactiv(N,LR),member(Nom,LR),oter(Nom,LR,LR1), retract(rulactiv(N,LR)), assert(rulactiv(N,LR1)), write1([N,remove,active,rule,Nom]). desactiver(_,_). activreg :- acti_link, acti_univ, acti_enpremier, acti_ro, acti_and, acti_def1, acti_exists, acti_or, acti_def2, acti_concl_exists, acti_endernier, ordoreg,! . timeover_ltb(Pred) :- version(ltb), statistics(cputime,T), tempsfinal(TF), T>TF, nl,write(T-' temps depasse in '-Pred),nl, resul(Res),tell(Res),write(T), nl,write('SZS status GaveUp for '), problem(P), write(P),nl, halt. acti_link :- forall(concept(C),assert(link(0,C))). acti_univ :- rules_univ(LR), assert(rulactiv(0,LR)). acti_ro :- prioritys(sans), rulactiv(0,LR), write1('\nacti_ro sans priority'), ( bagof(R, P^( link(0,P),type(R,P)),RR)-> true ; RR= [] ), append(LR, RR, LRR1), ( bagof(R, ( type(R,lemma)),RR1) -> append(LRR1, RR1, LRR) ; LRR = LRR1 ) , retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)), fail. acti_ro :- prioritys(with), rulactiv(0,LR), ( bagof(R, P^( link(0,P),type(R,P),\+ priority(R,2),\+ type(R,enpremier),\+ type(R,endernier)),RR)-> true ; RR= [] ), append(LR, RR, LRR1), ( bagof(R,(type(R,lemma),\+ priority(R,2),\+ type(R,enpremier),\+ type(R,endernier)),RR1) -> append(LRR1, RR1,LRR2) ; LRR2 = LRR1 ) , ( bagof(R, P^( link(0,P),type(R,P),priority(R,2)),RR2) -> append(LRR2,RR2,LRR3) ; LRR3 = LRR2 ), ( bagof(R,(type(R,lemma),priority(R,2)),RR3) -> append(LRR3, RR3,LRR) ; LRR = LRR3 ) , retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)), fail. acti_ro . acti_enpremier :- rulactiv(0,LR), ( bagof(R, ( type(R,enpremier)),RR1) -> append(LR,RR1,LRR) ; LRR=LR ) , retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)), fail. acti_enpremier. acti_endernier :- rulactiv(0,LR), ( bagof(R, ( type(R,endernier)),RR1) -> append(LR,RR1,LRR) ; LRR=LR ) , retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)), fail. acti_endernier. acti_and :- rulactiv(0,LR), rules_and(RET), append(LR,RET,LRR), retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)). acti_or :- rulactiv(0,LR), rules_or(ROU), append(LR,ROU,LRR), retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)). acti_def1 :- rulactiv(0,LR), rules_defconcl1(RR), append(LR,RR,LRR), retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)). acti_def2 :- rulactiv(0,LR), rules_defconcl2(RR), append(LR,RR,LRR), retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)). acti_exists :- rulactiv(0,LR),rules_existe(RILE),append(LR,RILE,LRR), retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)). acti_concl_exists :- rulactiv(0,LR), rules_concl_existe(RILE), append(LR,RILE,LRR), retractall(rulactiv(_,_)), assert(rulactiv(0,LRR)). ordoreg. compareg(_,_,_,_,_) :- write1('compareg sert a quoi ?'),fail. hyp_treated(N,H) :- hyp_treated(N,H,_), write1(hyp_treated_a_2_arg_restant-N-H). treatequal(N, X, Y, Ixy) :- \+ timeover_ltb(treatequal1), hyp(N, H,I), \+ H =(X=Y), replace(H,Y,X,H1),\+ H=H1, retract(hyp(N,H,_)), \+ hyp(N, H1,_), addhyp(N, H1,I1), write1ettrace(N,(hyp(N,X=Y,Ixy),hyp(N,H,I)), addhyp(N, H1,I1),equal), traces(N,action(treatequal_hyp), (hyp(N,X=Y,Ixy),hyp(N,H,I)), addhyp(N, H1,I1),I1, [Y,'is replaced by',X,'in the hypotheses'], [I,Ixy] ), write1('-------------------------------- treatequal'), fail. treatequal(N, X, Y,_) :- \+ timeover_ltb(treatequal2), hyp_treated(N, H,_), \+ H =(_=_), replace(H,Y,X,H1),\+ H=H1, retract(hyp_treated(N,H)), \+ hyp(N, H1,_), addhyp_treated(N, H1), fail. treatequal(N,X,Y,Ixy) :- \+ timeover_ltb(treatequal3), concl(N, X=Y,I), newconcl(N, true,I1), write1ettrace(N,(hyp(N,X=Y,Ixy),concl(N, X=Y,I)), newconcl(N, true,I1),=), traces(N,action('treatequal_concl='), (hyp(N,X=Y,Ixy),concl(N, X=Y,I)), newconcl(N, true,I1),I1, [Y,'is replaced by',X,'in the conclusion'], [I,Ixy] ), write1('-------------------------------- treatequal'). treatequal(N,X,Y,Ixy) :- \+ timeover_ltb(treatequal4), concl(N, C, I), replace(C, Y,X,C1), \+ C=C1, newconcl(N, C1, I1), write1ettrace(N,(hyp(N,X=Y,Ixy),concl(N, C, I)), newconcl(N, C1, I1),equal), traces(N,action(treatequal_concl), (hyp(N,X=Y,Ixy),concl(N, C, I)), newconcl(N, C1, I1),I1, [Y,'is replaced by',X,'in the conclusion'], [I,Ixy] ), write1('-------------------------------- treatequal'), fail. treatequal(N,X,Y,I) :- \+ timeover_ltb(treatequal5), clause(rule(L,Nom),Q), \+ Nom = ! , \+ Nom = concl_only , \+ timeover_ltb(treatequal5a), rulactiv(N,LR),member(Nom,LR), replace(Q, Y,X,Q1), \+ Q=Q1, sup_cond_triviales(Q1,Q2), Q3=Q2, create_nom_rule(Nom,Nom1),R = (rule(L,Nom1):-Q3), ajoureglocale(N,R,Nom1), write1(anciennerule/Nom-nouvrule/Nom1), step(E), traces(N,action(treatequal_rule), rule(Nom),create_rule(Nom1),E, [Y,'is replaced by',X,'in the rule',Nom, 'to give the rule',Nom1], [I] ), desactiver(N,Nom), write1('-------------------------------- treatequal'), fail. %%%%%%%%% nov 04 %%%%%%%%% %%% treatequal(N,X,Y,_) :- \+ timeover_ltb(treatequal6), retract(hyp(N,X=Y,_)), write1([remove,hypothesis,X=Y]), retract(objet(N,Y)),write1([remove,objet,Y]). treatequal(_,_,_,_). sup_cond_triviales( (hyp(_,X=X,_)),[]) :- !. sup_cond_triviales( (hyp(_,X=X,_),Q),Q1) :- sup_cond_triviales(Q,Q1),!. sup_cond_triviales( (Q,hyp(_,X=X,_)),Q) :- !. sup_cond_triviales((X,Q),(X,Q1)) :- sup_cond_triviales(Q,Q1),!. sup_cond_triviales(Q,Q). verifdef. elifundef :- timeover_ltb(elifundef). elifundef :- definition(Nomfof,D), D=(!_:(A=B)), assert(definition1(Nomfof,A=B )), retract(definition(Nomfof,D)), fail. elifundef :- definition(Nomfof,D), D=(!_:(~(A=B))), assert(definition1(Nomfof,~(A=B))), retract(definition(Nomfof,D)), fail. elifundef :- definition(Nomfof,D), D=(!_:(A<=>B)), elifun(B,B1), assert(definition1(Nomfof,A<=>B1)), retract(definition(Nomfof,D)), fail. elifundef :- definition1(Nomfof,D), retract(definition1(Nomfof,D)),assert(definition(Nomfof,D)),fail. elifundef :- lemma(Nom,B),elifun(B,B1), retract(lemma(Nom,B)),assert(lemma1(Nom,B1)), ( withseulile -> ( element(H=>only(FXY,C),B1),\+ (seulile(oui)) -> assert(seulile(oui)) ; B1 = only(FXY,C),\+ (seulile(oui)) -> assert(seulile(oui)) ; element(H=>C1 & only(FXY,C),B1),\+ (seulile(oui)) -> assert(seulile(oui)) ; element(H=>only(FXY,C) & C1,B1),\+ (seulile(oui)) -> assert(seulile(oui)) ; element(H<=>only(FXY,C),B1),\+ (seulile(not)) -> assert(seulile(not)) ) ; true ), fail. elifundef :- lemma1(Nom,B), retract(lemma1(Nom,B)),assert(lemma(Nom,B)), fail. elifundef :- definition(Nomfof,D),D=(!_:De), retract(definition(Nomfof,D)), assert(definition(Nomfof,De)), fail. elifundef . elifun(_,_) :- timeover_ltb(elifun). elifun(E, E1) :- ( (var(E);E=false;objet(_,E)) -> E1=E ; (atom(E);number(E)) -> ajobjet(-1,E), E1 =E ; E =..[P,A,B], (P= => ; P = (&) ; P=(|); P= <=> ; P='.' ) -> elifun(A,A1),elifun(B,B1),E1 =..[P,A1,B1] ; E = (..L) -> elifun(L, L1), E1 = (..L1) ; E =(!XX:P) -> elifun(P,P1), E1 = (!XX:P1) ; E =(?XX:P) -> elifun(P,P1), E1 = (?XX:P1) ; E =only(_,_) -> elifun2(E,E1) ; E =(_::_) -> E=E1%, ; E = (~ A) -> elifun(A, A1), E1 = (~ A1) ; E = (A=B), varatom(A), \+ varatom(B) -> elifun3((B::A),E1) ; E = (A=B), varatom(B), \+ varatom(A) -> elifun3((A::B),E1) ; E =..[P|_] -> elifun1(E,E1) ), ! . elifun2(E,E5) :- E = only(FX::Y,E1), FX =.. [F|Args], length(Args,N), ajfonction(F,N), member(Arg,Args), \+var(Arg), \+objet(_,Arg), ( (atom(Arg);number(Arg)) -> ajobjet(-1,Arg),fail ; replace(Args,Arg,Z,Args1), FX1 =.. [F|Args1], elifun2(only(FX1::Y,E1),E3), E4=only(Arg::Z,E3),elifun2(E4,E5) ), !. elifun2(E,E). elifun1(E,E4) :- (E=(_::_) -> E4=E;true), E =.. [P|Args], \+ P = only, member(Arg,Args), \+var(Arg), \+ objet(_,Arg), ( (atom(Arg);number(Arg)) -> ajobjet(-1,Arg),fail ; replace(Args,Arg,Y,Args1), E1 =.. [P|Args1], elifun(E1,E2),elifun1(E2,E22),E3=only(Arg::Y,E22), elifun2(E3,E4) ), !. elifun1(E,E). elifun4(FY::X,(Z,E1 & E2)) :- FY =.. [F|Args], member(Arg,Args), \+ atom(Arg), \+var(Arg), \+number(Arg), replace(Args,Arg,Z,Args1), FY1 =.. [F|Args1], elifun4(FY1::X, E1), elifun4(Arg::Z,E2), !. elifun4(E,E). elifun3(FX::Y,E) :- FX =.. [F|Args], member(Arg,Args), \+var(Arg), \+ objet(_,Arg), ( (atom(Arg);number(Arg)) -> ajobjet(-1,Arg),fail ; replace(Args,Arg,Z,Args1), FY1 =.. [F|Args1], elifun3(FY1::Y,FY1Y), elifun2(only(Arg::Z,FY1Y),E) ), !. elifun3(E,E). treat(N,(?[X|XX]:P),I1) :- ( var(X) ; atom(X)), !, ( P = (Q & R & S) -> \+ (hyp(N, Q1,_), eg(Q,Q1), hyp(N, R1,_), eg( R,R1), hyp(N, S1,_), eg(S,S1)) ; P = (Q & R) -> \+ (hyp(N, Q1,_), eg(Q,Q1), hyp(N, R1,_), eg( R,R1)) ; \+ (hyp(N, P1,_), eg(P,P1)) ) , create_objet(N,z,X1), ajobjet(N,X1), replace(P,X,X1,P1), write1ettrace(N,hyp(N,(?[X];P),I) , (ajobj(N,X1,I1),treat(N,P1,I1)),treatedment_exists), traces(N,action(treat_exi), (?[X|XX]:P),treat(N,P1,I1),I1, treat_exi, [] ), ( XX=[] -> treat(N, P1, I,I1) ; treat(N,(? XX:P1),I1) ) . treat(N,H,I,I1) :- addhyp(N, H,I1), write1ettrace(N,hyp(N,'',I),addhyp(N, H,I1),treat-I1). eg(P,P1) :- ( P = P1 ; P1 = (F1::Y) , P = (F::Y), F1=..L,F = (..L), message([eg,oui,ce,cas,se,produit]),read(_) ) . effacertout :- effacer([subth(_,_), hyp(_,_,_), hyp_treated(_,_,_), or_applique(_), concl(_,_,_), link(_,_), objet(_,_), fonction(_,_), rulactiv(_,_), tracedem(_,_,_,_,_,_,_), conjecture(_,_), fof(_,_,_), include(_), problem(_), definition(_Nomfof,_), lemma(_,_), priority(_,_), file(_), concept(_), rulehypuniv(_,_,_), step(_), fof_treated(_,_,_), seulile(_), version(_) ]), assert(problem(pas_encore_de_problem)), assert(conjecture(no_conjecture, false)), assert(seulile(niouininot)), effacer_regcons, reset_gensym, %(z) told. effacer([Item|Items]) :- effacer(Item), effacer(Items),!. effacer(Item) :- retractall(Item). effacer([]). effacer_regcons :- type(R,C), \+ C=donnee, retract((rule(_,R):- _)),retract(type(R,_)),fail. effacer_regcons :- effacer(type(_,_)). listeth :- liste([hyp, concl, objet]). listetout :- liste([hyp, hyp_treated, concl, /*objet,concept,fonction,*/ rulactiv,conjecture, fof ]). liste([Item|Items]) :- (listing(Item);true), liste(Items). liste([]). create_objet(N,X,XX) :- gensym(X,XX), ajobjet(N,XX). create_objets_and_replace(N,[X|XX],CX,C1,OO) :- create_objets_and_replace(N,[X|XX],CX,C1,[],OO). %, create_objets_and_replace(N,[X|XX],CX,C1,OO1,OO2) :- gensym(z, Z), ajobjet(N, Z), ligne,tab(3), replace(CX,X,Z,CZ), create_objets_and_replace(N,XX, CZ,C1,[Z|OO1],OO2). create_objets_and_replace(_N,[],C,C,OO,OO). create_nom_rule(R,RR) :- ( type(R,_) -> suc(R,R1),create_nom_rule(R1,RR) ; RR = R). replace(E, X, Y, E1) :- ( E == X -> E1 = Y ; (var(E) ; atom(E)) -> E1 = E ; E = [] -> E1 = [] ; E = [A|L] -> replace(A, X, Y, A1), replace(L, X, Y, L1), E1 = [A1|L1] ; E =..[F|A] -> replace(A, X, Y, A1), E1 =..[F|A1] ). hypor(A | B => C, (A => C) & BC) :- hypor(B => C, BC),!. hypor(T,T). or_and(A & B,C) :- or_and(A,A1), or_and(B,B1),assoc(A1 & B1,C),!. or_and(A | (B & C),F) :- or_and((A | B) & (A | C),F),!. or_and((A & B) | C, F) :- or_and((A | C) & (B | C),F),!. or_and(A | B,F):- or_and(A,A1),or_and(B,B1),not((A=A1,B=B1)), or_and(A1 | B1, F),!. or_and(A,A). assoc((A & B) & C,F) :- assoc(A & B & C,F),!. assoc(A & B,A1 & B1) :- assoc(A,A1), assoc(B,B1),!. assoc((A | B) | C,F) :- assoc(A | B | C,F),!. assoc(A | B,A1 | B1) :- assoc(A,A1), assoc(B,B1),!. assoc(A, A). or_not(A | ~ B, A, B) :- ! . or_not(A | B, A | Aplus, Amoins) :- or_not(B, Aplus,Amoins). elt_or(A,A | _) :- !. elt_or(A,_ | A) :- !. elt_or(X, _ | B) :- elt_or(X,B),!. elt_or_bis(N, A | _) :- elt_or_bis(N, A),!. elt_or_bis(N, A) :- A = only(FX::Y,P), hyp(N,FX::Y,_), hyp(N,P,_), write1(elt_or_bis-'FX::Y'/(FX::Y)-'P'/P), !. elt_or_bis(N, A) :- A = only(FX::Y,Z=T), hyp(N,FX::Y,_), Y=Z, Y=T, write1(elt_or_bis-'FX::Y'/(FX::Y)-'Y'/Y-'Z'/Z-'T'/T), !. elt_or_bis(N, _ | B) :- elt_or_bis(N, B), write1(elt_or_bis_), !. write1(L):- ligne, write0(L). write0_tirets(E) :- ligne, write0([---------------------------------------------------------]), write0(E). write0(_) :- version(casc),!. write0(E) :- (var(E) -> write(E) ;E = [X|L] -> write0(X), tab(1), write0(L) ;E=[] -> true ;write0AA(E) ). write0AA(T) :- numbervars(T,0,_,[singletons(true)]), write_term(T,[numbervars(true),max_depth(9)]), fail. write0AA(_). write0V(E) :- (var(E) -> write(E) ; (element(!,E);element(?,E);element(only,E)) -> writeV(E) ; E=(_ :- _) -> writeV(E) ; write(E) ). writeV(E) :- assert(-(E)),listing(-),retract(-(E)). ligne :- version(casc),!. ligne :- nl. message(M) :- tellling(F),toldd,write1(M),appendd(F). message(Fich,M) :- tellling(F), appendd(Fich), problem(Probleme), write1(Probleme),write1(M),appendd(F). traces(N,Nom,Cond,A,E,Expli,Antecedants) :- (Cond=[] -> true;write1(['\n*** because',Cond])), write1(['arcs',Antecedants-E]), write1(Expli), assert(tracedem(N,Nom,Cond,A,E,Expli,Antecedants)). write1ettrace(_,_,_,_):- write1(write1ettrace). modifytime(TL) :- affecter(timelimit(TL)). tptp :- write1(' TPTP MENU\n'), write1(['To prove a theorem of the TPTP Library', 'call tptp with arguments :', '\n a path or a file or a TPTP problem name ', '\n or a domain and two numbers i and j', '\n then eventually a time limit. ']), write1(['Parameters must be ', 'valid Prolog strings or numbers.']), write1('Do not forget the period at the end.\n'), write1( 'The detailed proof will be in the file res_'), write1(' followed by only the useful steps of the proof'), write1('To obtain only the useful trace, use the casc command'), write1(['\nExamples :', '\n tptp(''tptp/Problems/SET/SET027+4.p'').', '\n tptp(file_of_the_current_directory).', '\n tptp(''copy_of_SET027+4.p'').', '\n tptp(''SET027+4.p'').', '\n tptp(''SET'',27,4).']), timelimit(TL), write1(['\nThe default time limit is',TL,'secondes.']), write1(['To modify it type', '\n modifytime().', '\nor give it as a last agument', '(and it will be modified).']), write1(['To know it type', '\n timelimit(TL).']), write1(['\nExamples :', '\n tptp(''tptp/Problems/SET/SET741+4.p'',25).', '\n tptp(file_of_the_current_directory,40).', '\n tptp(''SET741+4.p'',25).', '\n tptp(''SET'',741,4,25).']). m :- [muscadet-enco]. t :- test. t1 :- abimpab. abimpab :- effacertout, tell(res_abimpab), prove(a & b => a & b). abimpac :- effacertout, prove(a & b => a & c). abimpcb :- effacertout, prove(a & b => c & b). aimpab :- effacertout, prove(a => a & b). pab :- effacertout, prove(p(a) & p(b) & q(b)=> ? [X]: (p(X) & q(X))). t2 :- aimpboua. aimpboua :- effacertout, tell(res_aimpboua), prove(a => b|a). test :- tptp('SET',2,4). tt :- tptp('SET',27,4). t3 :- effacertout, listetout,tptp(setequal). t3n :- effacertout, listetout,tptp(setequalnot). tc :- testcasc. testcasc :- casc('Problems/SET/SET002+4.p'). testcascsyn :- casc('Problems/SYN/SYN075+1.p'). tcs :- testcascsyn. agt(I) :- agt(I,1). agt(I,J) :- tptp('AGT',I,J). agt(I,J,T) :- tptp('AGT',I,J,T). alg(I) :- tptp('ALG',I,1). alg(I,T) :- tptp('ALG',I,1,T). c0 :- casc('tptp/Problems/SET/SET002+4.p'). geo(I) :- tptp('GEO',I,1). gra(I) :- tptp('GRA',I,1). krs(I) :- tptp('KRS',I,1). lcl(I) :- tptp('LCL',I,1). mgt(I) :- tptp('MGT',I,1). mgt2(I) :- tptp('MGT',I,2). nlp(I) :- tptp('NLP',I,1). se :- set10. set10 :- tptp('SET010+3.p'). set27 :- tptp('SET027+4.p'). set(I,J) :- tptp('SET',I,J). se(T) :- tptp('SET',745,4,T). set(I,J,T) :- tptp('SET',I,J,T). set1(I) :- modifytime(30),tptp(6,'SET',1,I). set3(I) :- tptp('SET',I,3). seu(I) :- tptp('SEU',I,1). seu(I,J) :- tptp('SEU',I,J). seu(I,J,T) :- tptp('SEU',I,J,T). swv(I) :- tptp('SWV',I,1). sy :- syn75. s :- syn75. syn75 :- tptp('SYN075+1.p'). syn(I) :- effacertout,tptp('SYN',I,1). syn :- effacertout, syn(973). tptp(_) :- effacertout, affecter(version(tptp)),fail. tptp(CHEMIN) :- file_base_name(CHEMIN,FICHIER), atom_concat(res_,FICHIER,RES), atom_concat(reg_,FICHIER,REG), exists_file(CHEMIN),tptp3(CHEMIN,REG,RES),!. tptp(NOM) :- sub_atom(NOM,0,3,_,DOM), concat_atom(['tptp/Problems/',DOM,'/',NOM],FICH), atom_concat(reg_,NOM,REG), atom_concat(res_,NOM,RES), exists_file(FICH), tptp3(FICH,REG,RES) ,!. tptp(CHouNOM) :- write1(['no file ni de problem',CHouNOM]). tptp(X,Temps) :- ( number(Temps) -> T is Temps*2, modifytime(T ), tptp(X) ; write1([Temps,'n''est pas un nombre']) ). tptp(Nom,apartirde,I) :- name(Nom,[_,_,_,N,U,M|_]), name(NUM,[N,U,M]), ( NUM < I -> write1([NUM,'est plus petit que',I]) ; tptp(Nom) ), ! . tptp(DOM,I,J) :- ( number(I), number(J) -> ( I<10 -> atom_concat(DOM,'00',D1) ; I<100 -> atom_concat(DOM,'0',D1) ; I >999 -> fail ; D1=DOM ) , atom_concat(D1,I,F1), atom_concat(F1,'+',F2), atom_concat(F2,J,F3),atom_concat(F3,'.p',FICH), tptp(FICH) ; write1([I,or,J,'n''est pas un nombre']) ). tptp(Nom,apartirde,I,Temps) :- ( number(Temps)-> modifytime(Temps),tptp(Nom,apartirde,I) ; write1([Temps,'n''est pas un nombre']) ). tptp(DOM,I,J,Temps) :- (number(Temps)->modifytime(Temps),tptp(DOM,I,J) ;write1([Temps,'n''est pas un nombre']) ). tptp3(FICH,_,_) :- not(exists_file(FICH)), write1(['no file ',FICH]),!. tptp3(FICH,REG,RES) :- message('---------------------------------------------------'), tempspasse(TP), affecter(problem(FICH)), lire(FICH), charger_axioms, travail1, telll(REG), listingg(rule), l(type),l(priority),l(definition),l(lemma), conjecture(Nom,TH), told,write1('TH'=TH), telll(RES), write1(FICH), write1(Nom), prove(TH), statistics(cputime,Tapresdem),Tdem is Tapresdem-TP, appendd(RES), write('('),write(Nom),write(')'), messagetemps(Tdem), appendd(RES), step(NH), write1([in,NH,steps]), statistics(cputime,Tavantutile), (concl(0,true,_) -> ligne, tracedemutile, statistics(cputime,Tapresutile), Tutile is Tapresutile-Tavantutile, write1([tracedemutile,en,Tutile,seconds]), concat_atom(['tracedemutile in ',Tutile,' seconds'],TU), message(TU) ; Tapresutile = Tavantutile), ligne,ligne, toldd, affecter(tempspasse(Tapresutile))%, . messagetemps(Tdem) :- write0(' in '),write0(Tdem),write0(' seconds'), write1(========================================), write0(========================================), toldd, told, write0(' in '),write0(Tdem), write0(' seconds'), message('---------------------------------------------------'). trad(E,E1) :- ( varatom(E) -> E1=E ; number(E) -> E=E1 ; E = (A=B), var(A) -> trad(B,B1),E1=(A=B1) ; E = ( A!=B) -> E1 = (~(A=B)) ; E = ( A <= B ) -> E1=(B => A) ; E = ( A <~> B ) -> E1=(~(B <=> A)) ; E = ( A ~& B ) -> E1=(~(B & A)) ; E = [L|LL] -> trad(L,L1),trad(LL,LL1), E1=[L1|LL1] ; E=..L -> trad(L,L1), E1=..L1 ; E=E1 ). lire(FICH) :- op(450,xfy,:), consult(FICH), fof(Nomfof,Nature,FormuleTPTP), trad(FormuleTPTP,Formule), (Nature = conjecture -> effacer([conjecture(_,_)]), assert(conjecture(Nomfof,Formule)) ;(Nature=axiom;Nature=hypothesis;Nature=lemma) -> (Formule=(! _ :(A=B)) -> assert(lemma(Nomfof,member(X,A <=> member(X,B)))), ( \+ var(A), A=..[P|L],vars(L), \+ element(P,B) -> assert(definition(Nomfof,Formule)) ; true ) ; Formule=(! _ :(A=B <=>!XX:C)),var(A), \+ var(B) -> replace(C,A,B,C1), assert(definition(Nomfof,!XX:C1)) ; true ), (Formule=(!_:(_=>(! XX :(A=B)))) -> assert(lemma(Nomfof,member(X,A) <=> member(X,B))), assert(definition(Nomfof,!XX:A=B)) ; true ), ( Formule=(!_:FT), FT=(A<=>_),A=..[_,X|_],var(X) -> assert(definition(Nomfof,Formule)) ; Formule=(!_:FT), FT=(ApplyR<=>_), ApplyR=..[Apply,R,_,_], write0('Formule'=Formule), atom(Apply),atom(R) -> assert(lemma(Nomfof,Formule)), assert(definition(Nomfof,FT)) ; assert(lemma(Nomfof,Formule)) ), ( Formule=(!_:FT), FT=(A =>_),A=..[P,X|_],var(X)-> ajconcept(P) ; true ) ; write1(type_de_fof_not_connu-FormuleTPTP) ), retract(fof(Nomfof,Nature,FormuleTPTP)), assert(fof_treated(Nomfof,Nature,FormuleTPTP)), fail. lire(_). charger_axioms :- include(Axioms), (getenv('TPTP',TPTPDirectory) -> atom_concat(TPTPDirectory,'/',Directory), atom_concat(Directory,Axioms,Axioms1), exists_file(Axioms1), lire(Axioms1), fail ; write1('Variable d''environnement TPTP not definie') ). charger_axioms. casc :- write1(' TPTP MENUU\n'), write1(['To prove a theorem of the TPTP Library', 'call casc with arguments ', 'an absolute or relative path to a TPTP problem name.' ]), write1('Do not forget the period at the end.\n'), write1( 'The useful steps of the proof will be on the standard output.'), write1('To obtain the detailed search, use the tptp command.'), write1(['\nExamples :', '\n casc(''/home/dominique/TPTP/TPTP-v3.5.0/Problems/SET/SET027+4.p'').', '\n casc(''tptp/Problems/SET/SET027+4.p'').', '\n casc(file_of_the_current_directory).' ]), write1(['\nThere is no time limit.']). casc(FICH) :- effacer([version(_)]),assert(version(casc)), affecter(timelimit(10000)), file_base_name(FICH,Probleme), affecter(problem(Probleme)), lire(FICH), charger_axioms, travail1, conjecture(Nom,TH), message(['theorem ',Nom]), prove(TH), nl , (concl(0, true,_) -> tracedemutile ; true). casc_ltb(Pb,Res,T1) :- assert(resul(Res)), statistics(cputime,Tavanteffacertout), Tfinal is Tavanteffacertout + T1, assert(tempsfinal(Tfinal)), assert(version(casc)), assert(version(ltb)), nl,write(timelimitpourladem=T1), affecter(timelimit(T1)), file_base_name(Pb,Probleme), affecter(problem(Probleme)), nl, write(problem=Probleme), (exists_file(Pb) -> true; write('no file'-Pb)), lire(Pb), charger_axioms, travail1, conjecture(Nom,TH), message(['theorem ',Nom]), prove(TH), statistics(cputime,Tapresdem), Tempstotaldem is Tapresdem-Tavanteffacertout, nl,write(tempstotaldem=Tempstotaldem),nl, tell(Res), (exists_file(Res)-> true;write('no file'-Res)), write(Tempstotaldem), nl, (concl(0, true,_) -> (conjecture(no_conjecture,_) -> write('SZS status Unsatisfiable for ') ; write('SZS status Theorem for ') ) ; write('SZS status GaveUp for ') ), write(Probleme), nl, told %, . csr(T) :- casc_ltb('Problems/CSR/CSR079+3.p',res,T). th :- write1(' menu th'), write1('To prove a theorem with a statement and data in a file f, call th(f).'), write1('Le theorem (unique) and les donnees doivent être ecrites of the facon suivante:'), write1(' theorem().'), write1(' definition().'), write1(' lemma().'), write1('Do not forget points (Prolog terms).'), write1('Example of file:'), write1(' theorem(![A,B,C]:(inc(A,B) & inc(B,C) => inc(A,C))).'), write1(' definition(inc(A,B) <=> ! [X]:(X elt A => X elt B)).'). th(Fth) :- [Fth], forall((definition(A<=>B), functor(A,P,_)),assert(definition(P,A<=>B))), elifundef,buildrules,theorem(Th),prove(Th), affecter(conjecture('','')), affecter(problem(problem)), tracedemutile . rules_and([concl_and]). rules_univ( [!, elifun, concl_exi_all, stop_hyp_concl, stop1a,stop_hyp_false,concl_or_stop3,concl_or_stop3bis, hyp_contradiction, equal,equaldef, hyp_or1,hyp_or23,hyp_or4,hyp_or5, concl_not,hypnot,hypnotnot,hypnotimp,hypimp, concl_not_or, concl_or_not, hypequ, hypnotequ, concl_or_and, =>,<=>, concl_only,..,..1, concl_ilec1, concl_ilec2, concl_ilec3,concl_ilec4, concl_ilec5, concl_ilec1a,concl_ilec1b, concl_ilec_only, concl_and_trivial_1,concl_and_trivial_2, concl_stop_trivial,concl_stop_trivial_or, concl2pts ] ) . rules_defconcl1([def_concl_pred,defconcl1a,defconcl1b,defconcl1bb]). rules_defconcl2([defconcl2,defconcl2app,defconcl2elt, defconcl2a,defconcl2b,defconcl3]). rules_existe([exists]). rules_or([hyp_or_cte, hyp_or]). rules_concl_existe([concl_exi,create_an_image_object]). rule(N, elifun) :- concl(N, C, I), elifun( C, C1), newconcl(N, C1,I1),!, traces(N,rule(elifun), concl(N, C, I), newconcl(N, C1, I1), I1, ['elimination of the functional symbols of the conclusion', '\nfor example, p(f(X)) is replaced by only(f(X)::Y, p(Y)'], [I]). rule(N,stop_hyp_concl ):- concl(N,C,IC), ground(C), hyp(N,C,I/**/), newconcl(N,true,NouvelleEtape), traces(N, rule(stop_hyp_concl), (hyp(N,C,I),concl(N,C,IC)), newconcl(N,true,NouvelleEtape), (NouvelleEtape), ['the conclusion',C,'to be proved is a hypothesis'], ([IC,I]) ). rule(N,stop1a):- concl(N,C,IC), ( C=(?_:_);C=(!_:_);C=(_ | _);C=(_<=>_) ;C=only(_::_,_) ), hyp(N,H,I), H =@= C, newconcl(N,true,I1), traces(N,rule(stop1a), (concl(N,C,IC),hyp(N,H,I)), newconcl(N,true,I1), I1, ['the conclusion',C,'to be proved is a hypothesis'], [IC,I] ), write1ettrace(N,(concl(N,C,IC),hyp(N,H,I)), newconcl(N,true,I1),stop1a). rule(N,stop_hyp_false):- hyp(N,false,I), newconcl(N,true,I1), traces(N,rule(stop_hyp_false), hyp(N,false,I),newconcl(N,true,I1), I1, ['a contradiction has been found'], [I]). rule(N,concl_or_stop3):-concl(N,A | B,I), hyp(N,H,II),elt_or(H,A | B), newconcl(N,true,I1), traces(N,rule(concl_or_stop3), (concl(N,A | B,I),hyp(N,H,II)), newconcl(N,true,I1),I1, 'one of the elements of the disjunctive conclusion is a hypothesis', [I,II] ). rule(N,concl_or_stop3bis):-concl(N,A | B,I), elt_or_bis(N,A | B), newconcl(N,true,I1), write1ettrace(N,concl(N,A | B,I), newconcl(N,true,I1),concl_or_stop3bis), traces(N,rule(concl_or_stop3bis), concl(N,A | B,I), newconcl(N,true,I1),I1, concl_or_stop3bis, [I]). rule(N,hyp_contradiction):- hyp(N,A,I), hyp(N,~ A,II), newconcl(N,true,I1), traces(N,rule(hyp_contradiction), (hyp(N,A,I), hyp(N,~ A,II)), newconcl(N,true,I1),I1, ['there is a contradiction'], [I,II] ). rule(N, equal) :- hyp(N, X=Y,I), A=X, B=Y, write1([replace,B,par,A,propager, and, remove,B]), treatequal(N,A,B,I). rule(N, equaldef) :- hyp(N,E::X,I), atom(X), hyp(N,E::Y,J), atom(Y), \+ X == Y, addhyp(N, X = Y, I1), write1ettrace(N,(hyp(N,E:X,I), hyp(N,E:Y,J), \+ X == Y), addhyp(N, X=Y, I1),equaldef), traces(N,rule(egadef), (hyp(N,E::X,I), hyp(N,E::Y,J), J), addhyp(N, X=Y, I1),I1, [X,and,Y,'have the same definition'], [I,J] ). rule(N, hyp_or1) :- hyp(N,A | A,I), \+ hyp_treated(N, A | A,_), addhyp(N,A,E),assert(hyp_treated(N, A | A,E)), traces(N,rule(hyp_or1),hyp(N,A | A,I), addhyp(N,A,E),E, '\n*** because a | a = a',[I]). rule(N, hyp_or23) :- hyp(N,A | B,I), elt_or(X=X, A | B), \+ hyp_treated(N, A | B,_), assert(hyp_treated(N, A | B,I)). rule(N, hyp_or4) :- hyp(N,A | B,I), \+ hyp_treated(N, A | B,_),hyp(N,A,_), assert(hyp_treated(N, A | B,I)). rule(N, hyp_or5) :- hyp(N,A | B,I), \+ hyp_treated(N, A | B,_),hyp(N,B,_), assert(hyp_treated(N, A | B,I)). rule(N, concl_not) :- concl(N,~ A,I), addhyp(N,A,I1), newconcl(N,false,I1), write1ettrace(N,concl(N,~ A,I), (addhyp(N,A,I1), newconcl(N,false,I1)), not), traces(N,rule(concl_not), concl(N,~ A,I), (addhyp(N,A,I1), newconcl(N,false,I1)),I1, ['assume',A,'and search for a contradiction'], [I] ). rule(N, hypnotnot) :- hyp(N,~ ~ A,I), addhyp(N, A, J), write1ettrace(N, hyp(N,~ ~ A,I), addhyp(N, A, J), hypnotnot), traces(N, rule(hypnotnot), hyp(N,~ ~ A,I), addhyp(N, A, J),J, '\n*** because ~ ~ a = a', [I,J] ). rule(N, hypnotimp) :- hyp(N,~(A=>B),I),\+ hyp(N,A ,_), addhyp(N,(A & ~ B),J), write1ettrace(N,hyp(N,~(A=>B),I), addhyp(N,(A & ~ B),J), hypnotimp), traces(N,rule(hypnotimp), hyp(N,~(A=>B),I), addhyp(N,(A & ~ B),J), J, '\n*** because ~(a=>b) = (a&~b)', [I] ). rule(N, hypnotequ) :- hyp(N,~(A<=>B),_), \+ hyp(N,(A & ~ B) | (~ A & B),_), addhyp(N,(A & ~ B) | (~ A & B),_). rule(N, hypequ) :- hyp(N,A <=> B,_),\+ hyp(N,(A & B) | (~ B & ~ A),_), addhyp(N, (A & B) | (~ B & ~ A),_). rule(N, hypnot) :- hyp(N,~ A,I), concl(N,false,IC), newconcl(N,A,I1), traces(N,rule(hypnot), (hyp(N,~ A,I), concl(N,false,IC)), newconcl(N,A,I1),I1, ['assume',A,'and search for a contradiction'], [I,IC] ). rule(N, concl_not_or) :- concl(N,~ A | B,I),addhyp(N,A,I1),newconcl(N,B,I1), traces(N,rule(concl_not_or), concl(N,~ A | B,I),(addhyp(N,A,I1), newconcl(N,B,I1)),I1, ['assume',A,'and prove',B], [I] ). rule(N, concl_or_not) :- concl(N,A | B,I), or_not(A | B,Aplus,Amoins), addhyp(N,Amoins,I1), newconcl(N,Aplus,I1), traces(N,rule(concl_or_not), concl(N,A | B,I), (addhyp(N,Amoins,I1), newconcl(N,Aplus),I1), I1, ['assume',Amoins, 'remove',~ Amoins,'of the conclusion'], [I] ). rule(N,concl_or_and) :- concl(N,A | B,I),or_and(A | B,C),newconcl(N,C,I1), traces(N,rule(concl_or_and), concl(N,A | B,I),newconcl(N,C,I1),I1, 'distributivity of | upon distributivite de | by rapport a &', [I] ). rule(N,=>) :- concl(N, A => B, IC), addhyp(N, A, NouvelleEtape), newconcl(N,B,NouvelleEtape), traces(N, rule(=>), (concl(N, A => B, IC)), [addhyp(N, A, NouvelleEtape), newconcl(N,B,NouvelleEtape)], (NouvelleEtape), 'to prove H=>C, assume H and prove C', ([IC]) ). rule(N,<=>) :- concl(N , A <=> B, E1), newconcl(N,(A => B) & (B => A), E2), traces(N,rule(<=>), concl(N, A <=> B, E1), newconcl(N,(A => B) & (B => A)), E2, ('A<=>B is replaced by (A=>B)&(B=>A)'), [E1]). rule(N, !) :- concl(N,(! XX : C), IC), step(E), NouvelleEtape is E+1,affecter(step(NouvelleEtape)), create_objets_and_replace(N,XX,C,C1,Objets), newconcl(N, C1,NouvelleEtape), traces(N, rule(!), concl((0,! XX : C), IC), [create_objets(Objets), newconcl(N, C1,NouvelleEtape)], (NouvelleEtape), 'the variables of the conclusion are instantiated', [IC] ). rule(N, concl_only) :- concl(N,only(A::X,B),I), ( hyp(N,A::Y,II) -> write1([replace,X,par,Y]), replace(B,X,Y,B1), newconcl(N,B1,I1), traces(N,rule(concl_only), (concl(N,only(A::X,B),I), hyp(N,A::Y,II)), newconcl(N,B1,I1), I1, X-is_replaced_by-Y-in-B, [I,II]) ; var(X) -> create_objet(N,z,X1), ajobjet(N, X1),addhyp(N,A::X1,I1), replace(B,X,X1,B1), newconcl(N,B1,I1), traces(N,rule(concl_only), concl(N,only(A::X,B),I), (addhyp(N,A::X1,I1),newconcl(N,B1,I1)), I1, ['creation of object',X1,'and of its definition'], [I]) ; write1([rule,only,cas, not,prevu]) ). rule(N, ..) :- concl(N, ..[R, X, Y], I), C=..[R, X, Y], newconcl(N, C, I1), traces(N,rule(..), concl(N, ..[R, X, Y], I), newconcl(N, C, I1),I1, '\n*** because ..[r,a,b] = r(a,b)', [I] ). rule(N, ..1) :- concl(N, ..[F, X]::Y,I), Z=..[F, X], newconcl(N, Z::Y,I1), traces(N,rule(..1), concl(N, ..[F, X]::Y,I), newconcl(N, Z::Y,I1),I1, '\*** because ..[f,x] = f(x)', [I] ). rule(N,concl_exi_all) :- concl(N,(?[X]:(![Y]:(A=>C))),E), addhyp(N,(![X]:(?[Y]:(A&(~C)))),E1), newconcl(N,false,E1), message(concl_exi_all), traces(N,rule(concl_exi_all), concl(N,(?[X]:(![Y]:(A=>C))),E), (addhyp(N,(![X]:(?[Y]:(A&(~C)))),E1), newconcl(N,false,E1)),E1, 'proof by contradiction', [E] ). rule(N, concl_ilec1) :- concl(N,(?[X]:C),I), (atom(X);var(X)),hyp(N,C,II), ground(C), newconcl(N, true, I1), replace((?[X]: C),X,_XX,CC), write1ettrace(N,(concl(N, CC,I), hyp(N,C,II)), newconcl(N, true, I1),concl_ilec1), traces(N,rule(concl_ilec1), (concl(N, CC,I), hyp(N,C,II)), newconcl(N, true, I1),I1, ['the object',X,'verifies the conclusion'], [I,II] ). rule(N, concl_ilec2) :- concl(N, (?[X]: (B & C)),I),(atom(X);var(X)), hyp(N,B,II),ground(B), hyp(N,C,III), ground(C), newconcl(N,true,I1), replace((?[X]:(B & C)),X,_XX,CC), traces(N, rule(concl_ilec2), ( concl(N, CC,I),hyp(N,B,II), hyp(N,C,III)), newconcl(N,true,I1), I1, ['the object',X,'verifies the conclusion'], [I,II,III] ). rule(N, concl_ilec3) :- concl(N, (?[X]: B | C),I),(atom(X);var(X)), ( hyp(N,B,II),ground(B) -> BouC=B ; hyp(N,C,II),ground(C) -> BouC=C), newconcl(N,true,I1), replace((?[X]: B | C),X,_XX,CC), write1ettrace(N,(concl(N, CC,I), hyp(N,BouC,II)), newconcl(N,true,I1),concl_ilec3). rule(N, concl_ilec4) :- concl(N, (?[X]: B => C),I),(atom(X);var(X)), ( hyp(N,~ B,II),ground(B)-> NBouC=(~ B) ; hyp(N,C,II),ground(C)-> NBouC=C), newconcl(N, true, I1), replace((?[X]: B => C),X,_XX,CC), write1ettrace(N,(concl(N, CC,I),hyp(N,NBouC,II)), newconcl(N, true, I1),concl_ilec4). rule(N, concl_ilec5) :- concl(N, (?XX: (~ C)),I), newconcl(N,false,I1),addhyp(N, (!XX:C),I1), write1ettrace(N,concl(N, (?[X]:( ~ C)),I), (newconcl(N,false,I1),addhyp(N, for_all(X,C),I1)), concl_ilec5). rule(N,concl_exi) :- write1(concl_exi), concl(N, ? XX:C, Eexi), write1(rule-concl_exi-XX-C), proveconclexi(N,? XX:C, Eexi,EEE), write1(rule-concl_exi-step-EEE). rule(N, create_an_image_object) :- objet(N,X), fonction(F,1), FX =.. [F,X], \+ hyp(N,_::X,_), \+ hyp(N,(?_:(FX::Y)),_), addhyp(N,(?[Y]:(FX::Y)),I1), traces(N,rule(create_an_image_object), [objet(N,X), fonction(F,1)], addhyp(N,(?[Y]:(FX::Y)),I1),I1, create_an_image_object, [] ), write1ettrace(N,creation, addhyp(N,(?_:(FX::Y)),I1), create_an_image_object). rule(N, concl_and_trivial_1) :- concl(N, A & B, I), hyp(N, A, II), write1([A, est, true]),newconcl(N, B, I1), write1ettrace(N,(concl(N, A & B, I),hyp(N, A, II)), newconcl(N, B, I1), concl_and_trivial_1), traces(N,rule(concl_and_trivial_1), (concl(N, A & B, I),hyp(N, A, II)), newconcl(N, B, I1),I1, 'one of the elements of the conjunctive conclusion is a hypothesis', [I,II] ). rule(N, concl_and_trivial_2) :- concl(N, A & B,I), hyp(N, B, II), write1([B, est, true]),newconcl(N, A, I1), write1ettrace(N,(concl(N, A & B,I), hyp(N, B, II)), newconcl(N, A, I1), concl_and_trivial_2), traces(N,rule(concl_and_trivial_2), (concl(N, A & B,I), hyp(N, B, II)), newconcl(N, A, I1), I1, 'one of the elements of the conjunctive conclusion is a hypothesis', [I,II] ). rule(N, concl_stop_trivial) :- concl(N, A = A, I), newconcl(N,true, I1), write1ettrace(N,concl(N, A = A, I), newconcl(N,true, I1), concl_stop_trivial), traces(N,rule(concl_stop_trivial), concl(N, A = A, I), newconcl(N,true, I1),I1, 'trivial conclusion', [I] ). rule(N, concl_stop_trivial_or) :- concl(N, A | B, I), elt_or(X=X,A | B), newconcl(N,true, I1), write1ettrace(N,concl(N, A | B, I), newconcl(N,true, I1), concl_stop_trivial_or), traces(N,rule(concl_stop_trivial_or), concl(N, A | B, I), newconcl(N,true, I1),I1, 'one of the elements of the disjunctive conclusion is a trivial', [I] ). rule(N, concl_and) :- concl(N, A & B, Eavant ), prove_conj(N, A & B, Eavant, _Eapres), (concl(N, true, _) -> Expli=['all the elements of the conjunctive conclusion of the theorem',N, 'have been proved'] ; Expli=['all the elements of the conjunctive conclusion of the theorem',N, 'n\'ont pas ete proveds'] )%, . rule(N, concl_or ) :- concl(N, A | B, Eavant ), demdij(N, A | B, Eavant, _Eapres), (concl(N, true, EE),message(stepfinale-EE) -> Expli=['one element of the disjunctive conclusion of theorem',N, 'has been proved'] ; Expli=['aucun element of the conclusion disjonctive du theorem',N, 'n\'has been proved'] )%, . rule(N, def_concl_pred) :- concl(N, C, I), definition(Nomfof,C <=> D), write1([N, 'definition of the conclusion']), newconcl(N, D, I1), traces(N, rule(def_concl_pred), concl(N, C, I), newconcl(N, D, I1), I1, ['the conclusion ',C,'is replaced by its definition(fof',Nomfof,')'], [I] ). rule(N, defconcl1a) :- concl(N, C | A, I), definition(Nomfof,C <=> D), write1([N, 'definition of the conclusion']), newconcl(N, D | A, I1), write1ettrace(N,concl(N, A | C, I), newconcl(N, D | A, I1), defconcl1a), traces(N,rule(defconcl1a), concl(N, A | C, I), newconcl(N, A | D, I1),I1, [definition,Nomfof], [I] ). rule(N, defconcl1b) :- concl(N, A | C, I), definition(Nomfof,C <=> D), write1([N, 'definition of the conclusion']), newconcl(N, A | D, I1), write1ettrace(N,concl(N, A | C, I), newconcl(N, A | D, I1), defconcl1b), traces(N,rule(defconcl1b), concl(N, A | C, I), newconcl(N, A | D, I1),I1, [definition,Nomfof], [I]). rule(N, defconcl1bb) :- concl(N, A | only(Y::X,only(Z::T,C)), I), definition(Nomfof,C <=> ~ D), write1([N, 'definition of the conclusion']), newconcl(N, A | ~ only(Y::X,only(Z::T,D)), I1), write1ettrace(N,concl(N, A | only(Y::X,only(Z::T,C)), I), newconcl(N, A | ~ only(Y::X,only(Z::T,D)), I1), defconcl1bb), traces(N,rule(defconcl1bb), concl(N, A | only(Y::X,only(Z::T,C)), I), newconcl(N, A | ~ only(Y::X,only(Z::T,D)), I1),I1, [definition,Nomfof], [I] ). rule(N, concl2pts) :- concl(N, FX::Y, I), newconcl(N, only(FX::Z, Z=Y), I1), traces(N,rule(concl2pts), concl(N, FX::Y, I), newconcl(N, only(FX::Z, Z=Y), I1),I1, ' FX::Y is rewriten only(FX::Z, Z=Y)', [I] ) . rule(N, defconcl2elt) :- concl(N, C, I), C =.. [R, A, B], hyp(N, D::B, II), definition(Nomfof,XappD <=> P), XappD =.. [R,X,D1],\+ var(D1), D=D1 , replace(P, X, A, P1), write1(['definition of the conclusion']), newconcl(N, P1, I1), write1ettrace(N,(concl(N, C, I), hyp(N, D:B, II)), newconcl(N, P1, I1), defconcl2elt) , traces(N,rule(defconcl2elt), (concl(N, C, I), hyp(N, D::B, II)), newconcl(N, P1, I1),I1, [definition,Nomfof], [I,II] ) . rule(N, exists) :- hyp(N, (?XX:P),I), \+ hyp_treated(N, (?XX:P),I), ( var(X) ; atom(X)), ( P = (Q & R & S) -> \+ (hyp(N, Q1,_), eg(Q,Q1), hyp(N, R1,_), eg( R,R1), hyp(N, S1,_), eg(S,S1)) ; P = (Q & R) -> \+ (hyp(N, Q1,_), eg(Q,Q1), hyp(N, R1,_), eg( R,R1)) ; \+ (hyp(N, P1,_), eg(P,P1)) ) , step(E), I1 is E+1, affecter(step(I1)), create_objets_and_replace(N,XX,P,P1,Objets), addhyp(N,P1,I1), addhyp_treated(N,(?XX:P),I), traces(N,rule(exists), hyp(N,(?XX:P),I), [create_objets(Objets), addhyp(N,P1,I1)], I1, 'treatment of the existential hypothesis', [I] ) . rule(N, hyp_or) :- hyp(N, (A | B),I), \+ hyp_treated(N, (A | B),_), \+ (or_applique(N)), concl(N, C, II), write1([N,treatment,of,the,disjunctive,hypothesise,(A | B)]), hypor(A | B => C, T), newconcl(N,T, I1), traces(N,rule(hyp_or), (hyp(N, A | B,I),concl(N, C, II)), newconcl(N,T, I1), I1, ['the conclusion has to be proved in both cases'], [I,II]), addhyp_treated(N, (A | B),I1), assert(or_applique(N)) . rule(N, hyp_or_cte) :- hyp(N, A | B,I), \+ hyp_treated(N, A | B,_), \+ (or_applique(N)), A=(A1=A2), B=(B1=B2), atom(A1), atom(A2), atom(B1), atom(B2), concl(N, C, II), write1([N,treatment,of,the,disjunctive,hypothesis,(A | B)]), hypor(A | B => C, T), newconcl(N,T, I1), traces(N,rule(hyp_or_cte), (hyp(N, A | B,I),concl(N, C, II)), newconcl(N,T, I1),I1, ['the conclusion has to be proved in both cases'], [I,II] ), addhyp_treated(N, A | B,I1), assert(or_applique(N)) . orphelin(L) :- tracedem(_,_,_,_,_,_,L),var(L),!. orphelin(E) :- tracedem(_,_,_,_,_,_,L),member(E,L), (var(E)-> write0('il reste une variable in tracedem'-L) ; E =\= 1), \+ tracedem(_,_,_,_,E,_,[_|_]). tracedemutile :- write1('graph : '), forall(tracedem(_,_,_,_,Etape,_,Antecedants), write0([Antecedants-Etape,''])), ( concl(0,true,Efin) -> bagof(B-A,C^D^E^F^G^tracedem(C,D,E,F,B,G,A),L1), step(Efin), ( reachable(Efin,L1,L11), sort(L11,VT) -> nl,write('useful steps':L11), write1('\n*****************\n* proof *\n*****************\n'), retractall(version(casc)), problem(P), write1('SZS output start proof for '), write(P), write1('\n* * * * * * * * * * * * * * * * * * * * * * * *'), write1('in the following, N is the number of a (sub)theorem'), write1(' E is the current step'), write1('hyp(N,H,E) means that H is an hypothesis of (sub)theorem N'), write1('concl(N,C,E) means that C is the conclusion of (sub)theorem N'), write1('obj_cte(N,C) means that C is a created object or a given constant'), write1('addhyp(N,H,E) means add H as a new hypothesis for N'), write1('newconcl(N,C,E) means that the new conclusion of N is C'), write1(' (C replaces the precedent conclusion)'), write1('a subtheorem N0-i or N0+i is a subtheorem of the (sub)theorem N0'), write1(' N0 is proved if all N0-i have been proved (&-node)'), write1(' or if one N0+i have been proved (|-node)'), write1('the initial theorem is numbered 0'), nl, write1('* * * theorem to be proved'), conjecture(_,TH), write1(TH), write1('\n* * * proof :'), write1('\n* * * * * * theorem 0 * * * * * *'), tracedemutile(VT), write1('then the initial theorem is proved'), (conjecture(no_conjecture,_) -> write0(' (no conjecture)') ;true), write1('* * * * * * * * * * * * * * * * * * * * * * * *\n'), write1('SZS output end proof for '), write(P),nl ; true ) ; write1('initial theorem not proved') ). tracedemutile([U|LU]) :- tracedem(_N,Nom,Cond,Act,(U),Expli,_Antecedants), write0trace(Act), (Cond=[] -> true ;write1(['\n*** because',Cond])), write1('\n*** explanation : '),write0(Expli), write0_tirets(Nom), tracedemutile(LU). tracedemutile([]). write0trace([Act|AA]) :- write0trace(Act), write0trace(AA),!. write0trace([]). write0trace(addhyp(N,A & B,E)) :- write0trace(addhyp(N,A,E)), tab(1), write0trace(addhyp(N,B,E)),!. write0trace(addhyp(N,only(FX::Y,A),E)) :- hyp(N,FX::Obj,Eobj), replace(A,Y,Obj,A1), (E=Eobj -> write0trace(addhyp(N,FX::Obj,E)),nl,tab(5) ; true), write0trace(addhyp(N,A1,E)),!. write0trace(createsubth(N,N1,_A,_E)) :- write1(['\n* * * * * * creation * * * * * * sub-theorem', N1,'* * * * *']), write1(['all the hypotheses of (sub)theorem',N, 'are hypotheses of subtheorem',N1]). write0trace(create_objets(OO)) :- write1(['create object(s)',OO]). write0trace(E) :- write1(['***',E]).