%% Copyright 2008 Crip5 Dominique Pastre %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Muscadet version 3.0a %% %% 03 sep 2008 %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%% %% declarations %% %%%%%%%%%%%%%%%%%% :-dynamic hyp/3. :-dynamic hyp_traite/3. :-dynamic hyp_traite/2. :-dynamic ou_applique/1. :-dynamic concl/3. :-dynamic lien/2. :-dynamic sousth/2. :-dynamic objet/2. :-dynamic reglactiv/2. :-dynamic regle/2. :-dynamic concept/1. :-dynamic fonction/2. :-dynamic type/2. :-dynamic avecseulile/0. :-dynamic definition/2. :-dynamic definition1/2. %1. :-dynamic lemme/2. :-dynamic lemme1/2. :-dynamic version/1. :-dynamic ecrireconsreg/0. :-dynamic tempslimite/1. :-dynamic tempspasse/1. :-dynamic conjecture/2. :-dynamic seulile/1. :-dynamic include/1. :-dynamic fof/3. :-dynamic fof_traitee/3. :-multifile fof/3. :- dynamic probleme/1. :- dynamic priorite/2. :- dynamic priorites/1. :- dynamic etape/1. priorites(avec). probleme(pas_encore_de_probleme). tempslimite(40). tempspasse(0). conjecture(pas_de_conjecture,false). seulile(niouininon). avecseulile. :-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,si). :- op(610,xfx,alors). :- op(200,xfy,app). l(regle(Nom)) :- clause(regle(_,Nom ),Q), assert(rr(regle(Nom),Q)), l(rr),retract(rr(_)). l(regle(_)) :- !. l(P) :- listing(P). ll(P) :- listingg(P). regle(Nom) :- clause(regle(_,Nom ),Q), ecrire1(Q). appliregactiv(0) :- reglactiv(0,LR),ecrire1(reglactiv-LR),fail. appliregactiv(N) :- repeat, ( concl(N, true, _) -> demontre(N) ; concl(N, _/timeout, _) -> !, nondemontre(N) ; reglactiv(N,LR) -> ( applireg(N,LR)-> fail ;! ) ) . applireg(N,_) :- tempsdepasse(N),!,nondemontre(N),fail. applireg(N,[R|RR]) :- (regle(N,R ) -> ecrire_tirets([regle,R]) ; applireg(N,RR) ) . applireg(N,[]) :- nondemontre(N), fail. tempsdepasse(N) :- statistics(cputime,T),tempspasse(TP),tempslimite(TL), TT is TP+TL , T>TT, concl(N,C, _), nouvconcl(N,C/timeout, _), ecrire1('temps limite depasse'-N-C), message('temps limite depasse'-N-C), ! . demontre(N) :- ecrire1([theoreme,N,demontre]), ( N=0 -> ( version(tptp),conjecture(pas_de_conjecture,_) -> message('pas de conjecture, probleme montre insatisfaisable') ; concat_atom([theoreme,N,demontre],' ',ThNdem),message(ThNdem) ), ( version(casc)-> nl, (conjecture(pas_de_conjecture,_) -> write('SZS status Unsatisfiable for ') ; write('SZS status Theorem for ') ), probleme(P),write(P) ; true) ; true ) . nondemontre(N) :- ecrire1([theoreme,N,non,demontre]), ( N=0 -> message('theoreme non demontre'), ( version(casc) -> nl, write('SZS status GaveUp for '), probleme(P),write(P) ; true ) ; true), !. %%%%%%%%%%%%%%%%%%%%%%%%%% %% fonctions diverses %% %%%%%%%%%%%%%%%%%%%%%%%%%% 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(_,_,_) :- tempsdepasse_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) -> remplacer(EX,X,x,Exx), ( XX=[] -> Ex=Exx ; Ex=(!XX:Exx) ), clos(Ex) ; E=(?[X|XX]:EX) -> remplacer(EX,X,x,Exx), ( XX=[] -> Ex=Exx ; Ex=(?XX:Exx) ), clos(Ex) ; E=seul(FX::X,PX) -> clos(FX),remplacer(PX,X,x,Px),clos(Px) ; E=..[_|L]-> clos(L) ; ecrire1(clos-E-non) ). :- dynamic fichier/1. telll(F) :- tell(F), retractall(fichier(_)), assert(fichier(F)). toldd :- retractall(fichier(_)),told. tellling(F) :- fichier(F),!. tellling(user). appendd(F) :- append(F), retractall(fichier(_)), assert(fichier(F)). listingg(Pred) :- Tete =.. [Pred], clause(Tete,Corps), ecrire1(Tete:-Corps),fail. listingg(Pred) :- Tete =.. [Pred,_], clause(Tete,Corps), ecrire1(Tete:-Corps),fail. listingg(Pred) :- Tete =.. [Pred,_,_], clause(Tete,Corps), ecrire1(Tete:-Corps),fail. listingg(Pred) :- Tete =.. [Pred,_,_,_], clause(Tete,Corps), ecrire1(Tete:-Corps),fail. listingg(Pred) :- Tete =.. [Pred,_,_,_,_,_], clause(Tete,Corps), ecrire1(Tete:-Corps),fail. listingg(_Pred). travail1 :- verifdef,elifondef, consreg, typesdonnees, told. typesdonnees :- clause(regle(_,Nom),_), \+ type(Nom,_), assert(type(Nom,donnee)),fail. typesdonnees. demontrer(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, ecrire1(machine:HostName), message(HostName) ), ecrire1('****************************************'), ecrire('****************************************'), ( version(casc) -> true ; ecrire1(['theoreme a demontrer']), ecrire1([Theoreme]) ), affecter(etape(0)), nouvconcl(0 , Theoreme, E/**/), traces(0, action(ini), [], nouvconcl(0 , Theoreme, E), E,'theoreme initial',[] ), activreg, appliregactiv(0 ), told, ! . creersousth(N,N1,A,E) :- assert(sousth(N,N1)), ligne,ecrire1([************************************************]), ecrire([sous-theoreme, N1,*****]), nouvconcl(N1,A,E ), copitem(N,N1). demconj(N,C,Econj, Efin) :- ( C = (A & B) | (C = A , B=true) ), atom_concat(N,-,N0), gensym(N0,N1), creersousth(N,N1,A,Ecreationsousth), (B=true -> Cond=[], Expli='demonstration du dernier element de la conjonction' ; Cond=concl(N, C, Econj), Expli='pour demontrer une conjonction, on demontre successivement tous les elements de la conjonction'), traces(N1,action(demconj), Cond, %(concl( C/*, Econj*/)), [creersousth(N,N1,A,Ecreationsousth), nouvconcl(N1,A,Ecreationsousth)], (Ecreationsousth), Expli, ([Econj])), ecrire_tirets([action,demconj]), appliregactiv(N1), !, concl(N1,true,Edemsousth), nouvconcl(N,B,Eretourth), traces(N, action(retourdem), concl(N1,true,Edemsousth), nouvconcl(N,B,Eretourth), (Eretourth), ['la conclusion',A, 'du (sous-)theoreme',N, 'a ete demontree ( sous-theoreme',N1,')'], ([Econj , Ecreationsousth,Edemsousth]) ), ecrire_tirets([action,retourdem]), ( B = true -> Eretourth=Efin ; demconj(N,B,Eretourth,Efin) ) . demdij(N,C,Edij, Efin) :- ( C = (A | B) | (C = A , B=true) ), atom_concat(N,+,N0), gensym(N0,N1), creersousth(N,N1,A,Ecreationsousth), traces(N,action(demdij),(concl(N, C, Edij)), creersousth(N,N1,A,Ecreationsousth), (Ecreationsousth), ['creation du sous-theoreme',N1,'de conclusion',A], ([Edij])), ecrire_tirets([action,demdij]), appliregactiv(N1), !, concl(N1,C1,Edemsousth), ( C1=true -> nouvconcl(N,true,Eretourth), traces(N, action(retourdemdij), (sousthdem), nouvconcl(N,true,Eretourth), (Eretourth), ['la conclusion',A, 'du (sous-)theoreme',N, 'a ete demontree'], ([Edij , Edemsousth]) ), ecrire_tirets([action,retourdemdij]) ; B \=true -> ecrire_tirets([action,retourdemdij]), ecrire1('on eie al disjonction suivante'), demdij(N,B,Edij,Efin) ; ecrire1('la disjonction n\'a pas ete demontree') ) . 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) ; ecrire1([on, n, a, pas, trouve, A, dans, C, pour, le, retirer]) ) . copitem(N,M) :- hyp(N, H,I), assert(hyp(M,H,I/**/)) /* pas de message */, fail. copitem(N,M) :- hyp_traite(N, H,E), assert(hyp_traite(M,H,E),E) , fail. copitem(N,M) :- objet(N, H), assert(objet(M,H)) ,fail. copitem(N,M) :- reglactiv(N, LR), assert(reglactiv(M,LR)), fail. copitem(_, _) . demconclexi(N, ? [X|XX]:C, Eexi, Efin):- obj_cte(N,Ob), ecrire1(['*** on essaie',Ob,'***']), atom_concat(N,+,N0), gensym(N0,N1), remplacer(C,X,Ob,C0), ( XX=[] -> C1=C0 ; C1= (?XX:C0)), creersousth(N,N1,C1,Ecreationsousth), traces(N1, action(demconclexi), concl(N, ? [X]:C, Eexi), [creersousth(N,N1,C1,Ecreationsousth), nouvconcl(N1,C1,Ecreationsousth)], Ecreationsousth, ['on essaie',Ob,'pour la variable existentielle'], [Eexi] ), ecrire_tirets([action,demconclexi]), ecrire1('++++++++++= demontrer'-C1), appliregactiv(N1), ( concl(N1, true, E1) -> nouvconcl(N,true,Efin), traces(N, action(retourdemexi), concl(N1, true, E1), nouvconcl(N,true, Efin), Efin, ['la conclusion du (sous-)theoreme',N, 'a ete demontree (sous-theoreme',N1,')'], [Eexi, E1] ) ; ecrire1('on essaie l\'objet suivant'),fail ). nouvconcl(N,C, E2) :- \+ concl(N, C, _), (etape(E1),var(E2) -> E2 is E1+1, affecter(etape(E2)) ; true), retractall(concl(N,_,_)),assert(concl(N,C,E2/**/)), ecrire1([E2:N,nouvconcl(C)]). ajhyp(N, H, E2) :- (var(E2) -> etape(E1), E2 is E1+1, affecter(etape(E2));true), ( H = (A & B) -> ajhyp(N, A, E2), ajhyp(N,B, E2) ; hyp(N, H,_) -> true ; H =(X,A) -> ( var(I1) -> etape(I), I1 is I+1, affecter(etape(I1)) ; true), assert(hyp(N,H,I1)), creer_objet(N,z,X1), remplacer(A,X,X1,A1), ajhyp(N,A1,I1) ; H = (Y=X), atom(X), atom(Y), avant(X,Y), ajhyp(N,(X=Y),E2) ; H = (..[R, X, Y]) -> (H1 =..[R, X, Y]), ajhyp(N, H1, E2) ; H = (..[F, X]::Y) -> (Y1 =..[F, X]), ajhyp(N, Y1:Y, E2) ; H=seul(A::X,Y)-> ( hyp(N,A::X1,_I) -> ecrire1([remplacer,X,par,X1,dans,Y]), remplacer(Y,X,X1,Y1),ajhyp(N,Y1,E2 ), ecrire1ettrace(N,'', ajhyp(N,Y1,I1),ajhypseul) ; creer_objet(N,z,X1),ajhyp(N,A::X1, E2 ), remplacer(Y,X,X1,Y1),ajhyp(N,Y1, E2 ), ecrire1ettrace(N,'', ajhyp(N,A::X1 & Y1, I1),ajhypseul) )%, ; H = (~ seul(FX::Y,P)) -> ajhyp(N,seul(FX::Y, ~ P ), E2) ; H = (!_: _) -> ( var(E2) -> etape(E0), E2 is E0+1, affecter(etape(E2)) ; true), atom_concat(reghyp__,E2,ReghypE2), atom_concat(ReghypE2,'__',Reghyp), ecrire1([E2:N,'traiter l\'hypothese universelle',H]), creer_nom_regle(Reghyp,Nom), consreg(H, _,Nomfof,N+H,Nom,[],[E2]), Imoins1 is E2-1, ecrire1ettrace(N,hyp(N,'',Imoins1),ajhyp(N,H,I1), I1) ; H = (~ (?XX:A)) -> creer_nom_regle(reghyp,Nom), consreg( (!XX:(~ A)), _, Nomfof, N+H, Nom, [],[]) ; H = (A =>B) -> creer_nom_regle(reghyp,Nom), consreg( H,_,Nomfof,N+H,Nom,[],[]) ; ( var(E2) -> etape(E0), E2 is E0+1, affecter(etape(E2)) ; true), assert(hyp(N, H,E2)), ecrire1([E2:N,ajhyp(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 ; etape(E), ecrire1([E:N, ajouter,objet,X])) ) . ajconcept(P) :- (concept(P) -> true; assert(concept(P))). ajfonction(F,N) :- (fonction(F,N)-> true;assert(fonction(F,N))). consreg :- effacer_regcons,fail. consreg :- definition(Nomfof,A<=> ~ B), A=..[P|L], vars(L), ajconcept(P), atom_concat(non,P,NonP),ajconcept(NonP), NonA =.. [NonP|L], \+ NonA = B, asserta(definition(Nomfof,A <=> ~ NonA)),asserta(definition(Nomfof,NonA <=> B)), creer_nom_regle(P,Nom), assert((regle(_,Nom):- hyp(N,~ A,I), \+ hyp(N,NonA,_), ajhyp(N,NonA,_), traces(N,regle(Nom), hyp(N,~ A,I), ajhyp(N,NonA,E),E, ['a cause de',P,et,NonP], [I] ) )), assert(type(Nom,P)), fail. consreg :- definition(Nomfof, A<=>B), not(var(A)), ( A=(C::_) -> C =..[P|_] ; A=..[_,_,E],not(var(E)),E=..[_|_] -> fail ; A=..[P|_] ), ajconcept(P), creer_nom_regle(P,Nom), (A=(X=Y)-> remplacer(B,Y,X,B1),consreg(B1,N,Nomfof,P,Nom,objet(N,X),[]) ; consreg(A=>B,_,Nomfof,P,Nom,[],[]), (ecrireconsreg -> ecrire1('+++consreg contraposee'/A=>B);true), (B = (_ | _) -> consreg(B=>A,_,Nomfof,P,Nom,[],[]);true) ), fail. consreg :- definition(Nomfof,A=B), not(B=[_,_]), A =.. [F|_], ajconcept(F), creer_nom_regle(F,Nom), elifon4(B::X,B1X), consreg(A::X => B1X,_,Nomfof,F,Nom,[],[]), fail. consreg :- definition(Nomfof,A<=>D), ( A =..[R,X,E],not(var(E)),E=..[F|_] ) , ajconcept(F), creer_nom_regle(F,Nom), ( atom(E) -> consreg((!XX:(A =>D)),_,Nomfof,F,Nom,[],[]) ; XappW =.. [R,X,W],consreg((E::W)=>!XX:(XappW <=>D),_,Nomfof,F,Nom,[],[]) ), fail. consreg :- lemme(Nomfof,E),atom_concat(Nomfof,'_',Nom0), creer_nom_regle(Nom0,Nom1), consreg(E,_,Nomfof,lemme,Nom1,[],[]), fail. consreg. consreg(E,N,Concept,Nom,Cond,An):- ecrire1(reste_consreg_a_6_arg), ecrire1([consreg,'\n','Concept'=Concept, '\n','Nom '=Nom, '\n','N '=N, '\n','Cond '=Cond, '\n','E '=E, '\n','An '=An]), fail. consreg(E,N,Nomfof,Concept,Nom,Cond,Antecedants):- ecrireconsreg, nl, ecrire1([consreg,'\n','Concept'=Concept, '\n','Nomfof '=Nomfof, '\n','Nom '=Nom, '\n','N '=N, '\n','Cond '=Cond, '\n','Antecedants'=Antecedants, '\n','E '=E]), fail. consreg(E,N,Nomfof,Concept,Nom,Cond,Antecedants) :- \+ tempsdepasse_ltb(consreg), ( E = (A | B => C) -> consreg((A=>C)&(B=>C),N,Nomfof,Concept,Nom,Cond,Antecedants) ; E = ((X=Y) => C), (var(X) | var(Y)) -> ( var(X) -> remplacer(Cond,X,Y,Cond1), remplacer(C,X,Y,C1) ; var(Y) -> remplacer(Cond,Y,X,Cond1), remplacer(C,Y,X,C1) ), consreg(C1,N,Nomfof,Concept,Nom,Cond1,Antecedants) ; E = (~ D => B) -> ajoucond(N,Cond,Antecedants, ~ D, Cond1,Antecedants1), consreg(B, N, Nomfof,Concept, Nom, Cond1,Antecedants1), creer_nom_regle(Nom, Nom1), consreg(D | B, N, Nomfof,Concept,Nom1,Cond,Antecedants) ; E = (~ D & A1 =>B) -> ajoucond(N,Cond,Antecedants,~ D,Cond1,Antecedants1), consreg(A1 => B,N,Nomfof,Concept,Nom,Cond1,Antecedants1), creer_nom_regle(Nom, Nom1), consreg(A1 => D | B, N, Nomfof,Concept,Nom1,Cond,Antecedants) ; E = (A1 & A2 => B) -> consreg(A1 => (A2 => B),N,Nomfof,Concept,Nom,Cond,Antecedants) ; E = (A => B), A = (!_:_) -> ajouseqavantobjet(Cond,concl(N,B,I),Cond1), ajoufinseq(Cond1,nouvconcl(N,A,I1),CondAct2), atom_concat(Nom, '_cs', Nom_cs), ajoufinseq(CondAct2, traces(N,regle(Nom_cs), concl(N,B,I), nouvconcl(N,A,I1), I1, 'condition suffisante', [I]), Regle), ajoureg(N, Concept, Nom_cs, Regle) , creer_nom_regle(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), nouvconcl(N,A &(B=>C),II1)), CondAct4), append(Antecedants,[I2,II],An1), ajoufinseq(CondAct4, traces(N,regle(Nom_cs_endernier), Cond+concl(N,C,II)+hyp(N,H,_)+averifier, nouvconcl(N,A & (B=>C),II1), II1, 'condition suffisante', An1 ), Regle2), ajoureg(N, endernier, Nom_cs_endernier, Regle2) ; E = (A=>B) -> ajoucond(N,Cond,Antecedants,A,Cond1,Antecedants1), consreg(B,N,Nomfof,Concept,Nom,Cond1,Antecedants1) ; E = (A<=>B) -> consreg((A=>B)&(B=>A),N,Nomfof,Concept,Nom,Cond,Antecedants) ; E = (A & B) -> creer_nom_regle(Nom, Nom1),consreg(A,N,Nomfof,Concept,Nom1,Cond,Antecedants), creer_nom_regle(Nom1, Nom2),consreg(B,N,Nomfof,Concept,Nom2,Cond,Antecedants) ; E = (![X]:B),(var(X); atom(X)) -> ajoucond(N,Cond,Antecedants,objet(N,X),Cond1,Antecedants1), consreg(B,N,Nomfof,Concept,Nom,Cond1,Antecedants) ; E = (![X|XX]:B),(var(X); atom(X)) -> ajoucond(N,Cond,Antecedants,objet(N,X),Cond1,Antecedants1), consreg(!XX:B,N,Nomfof,Concept,Nom,Cond1,Antecedants) ; E = seul(FX::Y, B) -> ajoucond(N,Cond,Antecedants,FX::Y,Cond1,Antecedants1), consreg(B,N,Nomfof,Concept,Nom,Cond1,Antecedants1), ( seulile(oui),seulile(non)->true ; seulile(non)-> true ; seulile(oui) -> atom_concat(Nom, '_crea_seul', Nom2), creer_nom_regle(Nom2, Nom1), ajouseqavantobjet(Cond, \+ hyp(N,FX::Y,_), Cond3), consreg((?[Y]:((FX::Y) & B)),N,Nomfof,Concept,Nom1,Cond3,Antecedants) ; true ) ; E = (~ (?[X]:A)) -> consreg((![X]:(~ A)),N,Nomfof,Concept,Nom,Cond,Antecedants) ; E = (~ ~ A) -> consreg(A,N,Nomfof,Concept,Nom,Cond,Antecedants) ; E = (~ A), \+(A=(!_:_)) -> ajoucond(N, Cond, Antecedants,A, Cond1,Antecedants1), consreg(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, ajhyp(N,E,I1), CondAct2), Act=ajhyp(N,E,I1), (Cond0=[] -> SiAlorsAct=Act;SiAlorsAct=(si Cond0 alors Act)), copy_term(SiAlorsAct,SiAlorsActCop), ( Concept=(_ + HypUnivImp) ->affecter(zut(HypUnivImp)), zut(HypU), Expli = ['regle locale\n',SiAlorsActCop, '\n(regle construite a partir de l\'hypothese universelle', HypU,')'] ; Concept=lemme -> Expli = [regle,SiAlorsActCop, 'construite a partir de l\'axiome', Nom,'(fof',Nomfof,')'] ; Expli= [regle,SiAlorsActCop, '\nconstruite a partir de la definition de',Concept, '(fof',Nomfof,')'] ), ajoufinseq(CondAct2, traces(N,regle(Nom), Cond0, ajhyp(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, ajhyp(N,T::Y,I1),CondAct3), ajoufinseq(CondAct3, traces(N,regle(Nom), Cond0, ajhyp(N,E,I1),I1, ['a cause de',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, ajhyp(N,T,I1),CondAct3), ajoufinseq(CondAct3, trace(N,regle(Nom), Cond0, ajhyp(N,E,I1),I1, ['a cause de',Concept], Antecedants ), Regle ), ajoureg(N, Concept, Nom, Regle) ; E = (A | B),definition(Nomfof,A <=> ~ A1), A =..[_|L],vars(L), A1 =..[_|_] -> ecrire1('consreg ou1 non Nom/E'=Nom/E), sup_objet(Cond,Cond0), ajoufinseq(Cond, \+ hyp(N,E,_), Cond1) , ajoufinseq(Cond1, ajhyp(N,E,I1), CondAct2), atom_concat(Nom, ounonpourquoi, Nom11), creer_nom_regle(Nom11,Nom1), ajoufinseq(CondAct2, ecrire1ettrace(N,Cond,ajhyp(N,E,I1),Nom1),Regle), ajoureg(N, Concept, Nom1, Regle), ajoufinseq(Cond, A1, Cond3), ajoufinseq(Cond3, traces(N,regle(Nom1), Cond,ajhyp(N,E,I1),I1, ['a cause de',Concept], Antecedants ), Regle2 ), consreg(B,N,Nomfof,Concept,Nom1,Regle2,Antecedants) ; E = (B | A),definition(Nomfof,A <=> ~ A1), A =..[_|L],vars(L), A1 =..[_|_] -> ecrire1('consreg ou2 non Nom/E'=Nom/E), sup_objet(Cond,Cond0), ajoufinseq(Cond, \+ hyp(N,E,_), Cond1) , ajoufinseq(Cond1, ajhyp(N,E,I1), CondAct2), atom_concat(Nom, ounonpourquoi, Nom11), creer_nom_regle(Nom11,Nom1), ajoufinseq(CondAct2, traces(N,regle(Nom1), Cond0,ajhyp(N,E,I1),I1, ['a cause de',Concept], Antecedants ), Regle1 ), ajoureg(N, Concept, Nom1, Regle1), ajouseqavantobjet(Cond, A1, Cond3), ajoufinseq(Cond3, traces(N,regle(Nom1), Cond,ajhyp(N,E,EE),EE, ['a cause de',Concept], Antecedants ), Regle2 ), consreg(B,N,Nomfof,Concept,Nom1,Regle2,Antecedants) ; Cond=Cond0, ajoufinseq(Cond, \+ hyp(N,E,_), Cond1), Act=ajhyp(N,E,I1), %Act_simpli=ajhyp(E), ajoufinseq(Cond1, Act , CondAct2), ( E = (?_:_) -> Priorite = 2, atom_concat(Nom, existe, Nom1) ; E = (_ | _) -> Priorite = 2, atom_concat(Nom, ou, Nom1) ; Nom = Nom1, Priorite = 1), creer_nom_regle(Nom1,Nom2), assert(priorite(Nom2,Priorite)), (Cond0=[] -> SiAlorsAct=Act;SiAlorsAct=(si Cond0 alors Act)), copy_term(SiAlorsAct,SiAlorsActCop), ( Concept=(_ + HypUnivImp) ->affecter(zut(HypUnivImp)), zut(HypU), Expli = ['regle locale2\n',SiAlorsActCop, '\n(regle construite a partir de l\'hypothese universelle',HypU] ; Concept=lemme -> Expli = [regle2,SiAlorsActCop, '\nconstruite a partir de l\'axiome', Nomfof] ; Expli= [regle2,SiAlorsActCop, '\nconstruite a partir de la definition de',Concept, '(fof',Nomfof,')']), ajoufinseq(CondAct2, traces(N,regle(Nom2),Cond0,ajhyp(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,_) :- ecrire1(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 = seul(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)) -> ecrire1('??????????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 = (~ seul(FX::Y,P)) -> ajoucond(N,C,An,seul(FX::Y,~ P),CA,AnA) ; ajouseqavantobjet(C,hyp(N,A,Etape),CA), ajoufin(An,Etape,AnA) ) . ajoureg(N, Arg, Nom, Corps) :- sup_cond_egal(Corps, Corps0), (ecrireconsreg -> nl,ecrire1('apres sup_cond_egal'-Corps0);true), ( Arg=(Nsth+H) -> etape(E),assert(reglehypuniv(Nom,H,E)), ajoureglocale(Nsth,(regle(N,Nom):-Corps0), Nom) ; assert((regle(N,Nom) :- Corps0)), assert(type(Nom,Arg)), (Nom=disjoint -> message(ajouregdisjoint-Corps0) ;true) ). numberth(N) :- atom_concat(0,_,N). sup_cond_egal(Corps,Corps0) :- ( sup_egal(X=Y,Corps, Corps1) -> ( var(X) -> remplacer(Corps1,X,Y,Corps2) ; var(Y) -> remplacer(Corps1,Y,X,Corps2) ), sup_cond_egal(Corps2,Corps0) ; Corps0=Corps ). sup_egal(X=Y,(X=Y,L),L) :- !. sup_egal(X,(Y,L),(Y,L1)) :- sup_egal(X,L,L1),!. sup_egal(X=Y,X=Y,[]) :- ! . ajoureglocale(Arg,R, Nom) :- reglactiv(Arg,LR), R= (regle(_,Nom):-Corps), etape(E), ecrire1([E:Arg,'ajouter la regle active locale']), ecrire(R), ecrire1('a la fin des regles universelles'),ligne, assert(type(Nom,Arg)), regles_univ(LRU),append(LRU,LRNU,LR), ( compareg(Corps,LRNU,L2,R3,L3) -> append([R3,Nom|L2],L3,NLR), ecrire1([et,mettre,R3,avant]),ligne ; NLRNU=[Nom|LRNU] ), append(LRU,NLRNU,NLR), retract(reglactiv(Arg,LR)), assert(reglactiv(Arg,NLR)), assert(R),!. desactiver(N,Nom) :- reglactiv(N,LR),member(Nom,LR),oter(Nom,LR,LR1), retract(reglactiv(N,LR)), assert(reglactiv(N,LR1)), ecrire1([N,supprimer,la,regle,active,Nom]). desactiver(_,_). activreg :- acti_lien, acti_univ, acti_enpremier, acti_ro, acti_et, acti_def1, acti_ilexiste, acti_ou, acti_def2, acti_concl_ilexiste, acti_endernier, ordoreg,! . tempsdepasse_ltb(Pred) :- version(ltb), statistics(cputime,T), tempsfinal(TF), T>TF, nl,write(T-' temps depasse dans '-Pred),nl, resul(Res),tell(Res),write(T), nl,write('SZS status GaveUp for '), probleme(P), write(P),nl, halt. acti_lien :- forall(concept(C),assert(lien(0,C))). acti_univ :- regles_univ(LR), assert(reglactiv(0,LR)). acti_ro :- priorites(sans), reglactiv(0,LR), ecrire1('\nacti_ro sans priorite'), ( bagof(R, P^( lien(0,P),type(R,P)),RR)-> true ; RR= [] ), append(LR, RR, LRR1), ( bagof(R, ( type(R,lemme)),RR1) -> append(LRR1, RR1, LRR) ; LRR = LRR1 ) , retractall(reglactiv(_,_)),assert(reglactiv(0,LRR)), fail. acti_ro :- priorites(avec), reglactiv(0,LR), ( bagof(R, P^( lien(0,P),type(R,P),\+ priorite(R,2),\+ type(R,enpremier),\+ type(R,endernier)),RR)-> true ; RR= [] ), append(LR, RR, LRR1), ( bagof(R,(type(R,lemme),\+ priorite(R,2),\+ type(R,enpremier),\+ type(R,endernier)),RR1) -> append(LRR1, RR1,LRR2) ; LRR2 = LRR1 ) , ( bagof(R, P^( lien(0,P),type(R,P),priorite(R,2)),RR2) -> append(LRR2,RR2,LRR3) ; LRR3 = LRR2 ), ( bagof(R,(type(R,lemme),priorite(R,2)),RR3) -> append(LRR3, RR3,LRR) ; LRR = LRR3 ) , retractall(reglactiv(_,_)),assert(reglactiv(0,LRR)), fail. acti_ro . acti_enpremier :- reglactiv(0,LR), ( bagof(R, ( type(R,enpremier)),RR1) -> append(LR,RR1,LRR) ; LRR=LR ) , retractall(reglactiv(_,_)),assert(reglactiv(0,LRR)), fail. acti_enpremier. acti_endernier :- reglactiv(0,LR), ( bagof(R, ( type(R,endernier)),RR1) -> append(LR,RR1,LRR) ; LRR=LR ) , retractall(reglactiv(_,_)),assert(reglactiv(0,LRR)), fail. acti_endernier. acti_et :- reglactiv(0,LR), regles_et(RET), append(LR,RET,LRR), retractall(reglactiv(_,_)),assert(reglactiv(0,LRR)). acti_ou :- reglactiv(0,LR), regles_ou(ROU), append(LR,ROU,LRR), retractall(reglactiv(_,_)),assert(reglactiv(0,LRR)). acti_def1 :- reglactiv(0,LR), regles_defconcl1(RR), append(LR,RR,LRR), retractall(reglactiv(_,_)),assert(reglactiv(0,LRR)). acti_def2 :- reglactiv(0,LR), regles_defconcl2(RR), append(LR,RR,LRR), retractall(reglactiv(_,_)),assert(reglactiv(0,LRR)). acti_ilexiste :- reglactiv(0,LR),regles_existe(RILE),append(LR,RILE,LRR), retractall(reglactiv(_,_)),assert(reglactiv(0,LRR)). acti_concl_ilexiste :- reglactiv(0,LR), regles_concl_existe(RILE), append(LR,RILE,LRR), retractall(reglactiv(_,_)), assert(reglactiv(0,LRR)). ordoreg. compareg(_,_,_,_,_) :- ecrire1('compareg sert a quoi ?'),fail. hyp_traite(N,H) :- hyp_traite(N,H,_), ecrire1(hyp_traite_a_2_arg_restant-N-H). traitegal(N, X, Y, Ixy) :- \+ tempsdepasse_ltb(traitegal1), hyp(N, H,I), \+ H =(X=Y), remplacer(H,Y,X,H1),\+ H=H1, retract(hyp(N,H,_)), \+ hyp(N, H1,_), ajhyp(N, H1,I1), ecrire1ettrace(N,(hyp(N,X=Y,Ixy),hyp(N,H,I)), ajhyp(N, H1,I1),egal), traces(N,action(traitegal_hyp), (hyp(N,X=Y,Ixy),hyp(N,H,I)), ajhyp(N, H1,I1),I1, ['on remplace',Y,par,X,'dans les hypotheses'], [I,Ixy] ), ecrire1('-------------------------------- traitegal'), fail. traitegal(N, X, Y,_) :- \+ tempsdepasse_ltb(traitegal2), hyp_traite(N, H,_), \+ H =(_=_), remplacer(H,Y,X,H1),\+ H=H1, retract(hyp_traite(N,H)), \+ hyp(N, H1,_), ajhyp_traite(N, H1), fail. traitegal(N,X,Y,Ixy) :- \+ tempsdepasse_ltb(traitegal3), concl(N, X=Y,I), nouvconcl(N, true,I1), ecrire1ettrace(N,(hyp(N,X=Y,Ixy),concl(N, X=Y,I)), nouvconcl(N, true,I1),=), traces(N,action('traitegal_concl='), (hyp(N,X=Y,Ixy),concl(N, X=Y,I)), nouvconcl(N, true,I1),I1, ['on remplace',Y,par,X,'dans la conclusion'], [I,Ixy] ), ecrire1('-------------------------------- traitegal'). traitegal(N,X,Y,Ixy) :- \+ tempsdepasse_ltb(traitegal4), concl(N, C, I), remplacer(C, Y,X,C1), \+ C=C1, nouvconcl(N, C1, I1), ecrire1ettrace(N,(hyp(N,X=Y,Ixy),concl(N, C, I)), nouvconcl(N, C1, I1),egal), traces(N,action(traitegal_concl), (hyp(N,X=Y,Ixy),concl(N, C, I)), nouvconcl(N, C1, I1),I1, ['on remplace',Y,par,X,'dans la conclusion'], [I,Ixy] ), ecrire1('-------------------------------- traitegal'), fail. traitegal(N,X,Y,I) :- \+ tempsdepasse_ltb(traitegal5), clause(regle(L,Nom),Q), \+ Nom = ! , \+ Nom = concl_seul , \+ tempsdepasse_ltb(traitegal5a), reglactiv(N,LR),member(Nom,LR), remplacer(Q, Y,X,Q1), \+ Q=Q1, sup_cond_triviales(Q1,Q2), Q3=Q2, creer_nom_regle(Nom,Nom1),R = (regle(L,Nom1):-Q3), ajoureglocale(N,R,Nom1), ecrire1(ancienneregle/Nom-nouvregle/Nom1), etape(E), traces(N,action(traitegal_regle), regle(Nom),creer_regle(Nom1),E, ['on remplace',Y,par,X,'dans la regle',Nom, 'pour donner la regle',Nom1], [I] ), desactiver(N,Nom), ecrire1('-------------------------------- traitegal'), fail. %%%%%%%%% nov 04 %%%%%%%%% %%% traitegal(N,X,Y,_) :- \+ tempsdepasse_ltb(traitegal6), retract(hyp(N,X=Y,_)), ecrire1([supprimer,hypothese,X=Y]), retract(objet(N,Y)),ecrire1([supprimer,objet,Y]). traitegal(_,_,_,_). 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. elifondef :- tempsdepasse_ltb(elifondef). elifondef :- definition(Nomfof,D), D=(!_:(A=B)), assert(definition1(Nomfof,A=B )), retract(definition(Nomfof,D)), fail. elifondef :- definition(Nomfof,D), D=(!_:(~(A=B))), assert(definition1(Nomfof,~(A=B))), retract(definition(Nomfof,D)), fail. elifondef :- definition(Nomfof,D), D=(!_:(A<=>B)), elifon(B,B1), assert(definition1(Nomfof,A<=>B1)), retract(definition(Nomfof,D)), fail. elifondef :- definition1(Nomfof,D), retract(definition1(Nomfof,D)),assert(definition(Nomfof,D)),fail. elifondef :- lemme(Nom,B),elifon(B,B1), retract(lemme(Nom,B)),assert(lemme1(Nom,B1)), ( avecseulile -> ( element(H=>seul(FXY,C),B1),\+ (seulile(oui)) -> assert(seulile(oui)) ; B1 = seul(FXY,C),\+ (seulile(oui)) -> assert(seulile(oui)) ; element(H=>C1 & seul(FXY,C),B1),\+ (seulile(oui)) -> assert(seulile(oui)) ; element(H=>seul(FXY,C) & C1,B1),\+ (seulile(oui)) -> assert(seulile(oui)) ; element(H<=>seul(FXY,C),B1),\+ (seulile(non)) -> assert(seulile(non)) ) ; true ), fail. elifondef :- lemme1(Nom,B), retract(lemme1(Nom,B)),assert(lemme(Nom,B)), fail. elifondef :- definition(Nomfof,D),D=(!_:De), retract(definition(Nomfof,D)), assert(definition(Nomfof,De)), fail. elifondef . elifon(_,_) :- tempsdepasse_ltb(elifon). elifon(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='.' ) -> elifon(A,A1),elifon(B,B1),E1 =..[P,A1,B1] ; E = (..L) -> elifon(L, L1), E1 = (..L1) ; E =(!XX:P) -> elifon(P,P1), E1 = (!XX:P1) ; E =(?XX:P) -> elifon(P,P1), E1 = (?XX:P1) ; E =seul(_,_) -> elifon2(E,E1) ; E =(_::_) -> E=E1%, ; E = (~ A) -> elifon(A, A1), E1 = (~ A1) ; E = (A=B), varatom(A), \+ varatom(B) -> elifon3((B::A),E1) ; E = (A=B), varatom(B), \+ varatom(A) -> elifon3((A::B),E1) ; E =..[P|_] -> elifon1(E,E1) ), ! . elifon2(E,E5) :- E = seul(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 ; remplacer(Args,Arg,Z,Args1), FX1 =.. [F|Args1], elifon2(seul(FX1::Y,E1),E3), E4=seul(Arg::Z,E3),elifon2(E4,E5) ), !. elifon2(E,E). elifon1(E,E4) :- (E=(_::_) -> E4=E;true), E =.. [P|Args], \+ P = seul, member(Arg,Args), \+var(Arg), \+ objet(_,Arg), ( (atom(Arg);number(Arg)) -> ajobjet(-1,Arg),fail ; remplacer(Args,Arg,Y,Args1), E1 =.. [P|Args1], elifon(E1,E2),elifon1(E2,E22),E3=seul(Arg::Y,E22), elifon2(E3,E4) ), !. elifon1(E,E). elifon4(FY::X,(Z,E1 & E2)) :- FY =.. [F|Args], member(Arg,Args), \+ atom(Arg), \+var(Arg), \+number(Arg), remplacer(Args,Arg,Z,Args1), FY1 =.. [F|Args1], elifon4(FY1::X, E1), elifon4(Arg::Z,E2), !. elifon4(E,E). elifon3(FX::Y,E) :- FX =.. [F|Args], member(Arg,Args), \+var(Arg), \+ objet(_,Arg), ( (atom(Arg);number(Arg)) -> ajobjet(-1,Arg),fail ; remplacer(Args,Arg,Z,Args1), FY1 =.. [F|Args1], elifon3(FY1::Y,FY1Y), elifon2(seul(Arg::Z,FY1Y),E) ), !. elifon3(E,E). traiter(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)) ) , creer_objet(N,z,X1), ajobjet(N,X1), remplacer(P,X,X1,P1), ecrire1ettrace(N,hyp(N,(?[X];P),I) , (ajobj(N,X1,I1),traiter(N,P1,I1)),traitement_ilexiste), traces(N,action(traiter_exi), (?[X|XX]:P),traiter(N,P1,I1),I1, traiter_exi, [] ), ( XX=[] -> traiter(N, P1, I,I1) ; traiter(N,(? XX:P1),I1) ) . traiter(N,H,I,I1) :- ajhyp(N, H,I1), ecrire1ettrace(N,hyp(N,'',I),ajhyp(N, H,I1),traiter-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([sousth(_,_), hyp(_,_,_), hyp_traite(_,_,_), ou_applique(_), concl(_,_,_), lien(_,_), objet(_,_), fonction(_,_), reglactiv(_,_), tracedem(_,_,_,_,_,_,_), conjecture(_,_), fof(_,_,_), include(_), probleme(_), definition(_Nomfof,_), lemme(_,_), priorite(_,_), fichier(_), concept(_), reglehypuniv(_,_,_), etape(_), fof_traitee(_,_,_), seulile(_), version(_) ]), assert(probleme(pas_encore_de_probleme)), assert(conjecture(pas_de_conjecture, false)), assert(seulile(niouininon)), 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((regle(_,R):- _)),retract(type(R,_)),fail. effacer_regcons :- effacer(type(_,_)). listeth :- liste([hyp, concl, objet]). listetout :- liste([hyp, hyp_traite, concl, /*objet,concept,fonction,*/ reglactiv,conjecture, fof ]). liste([Item|Items]) :- (listing(Item);true), liste(Items). liste([]). creer_objet(N,X,XX) :- gensym(X,XX), ajobjet(N,XX). creer_objets_et_remplacer(N,[X|XX],CX,C1,OO) :- creer_objets_et_remplacer(N,[X|XX],CX,C1,[],OO). %, creer_objets_et_remplacer(N,[X|XX],CX,C1,OO1,OO2) :- gensym(z, Z), ajobjet(N, Z), ligne,tab(3), remplacer(CX,X,Z,CZ), creer_objets_et_remplacer(N,XX, CZ,C1,[Z|OO1],OO2). creer_objets_et_remplacer(_N,[],C,C,OO,OO). creer_nom_regle(R,RR) :- ( type(R,_) -> suc(R,R1),creer_nom_regle(R1,RR) ; RR = R). remplacer(E, X, Y, E1) :- ( E == X -> E1 = Y ; (var(E) ; atom(E)) -> E1 = E ; E = [] -> E1 = [] ; E = [A|L] -> remplacer(A, X, Y, A1), remplacer(L, X, Y, L1), E1 = [A1|L1] ; E =..[F|A] -> remplacer(A, X, Y, A1), E1 =..[F|A1] ). hypou(A | B => C, (A => C) & BC) :- hypou(B => C, BC),!. hypou(T,T). ou_et(A & B,C) :- ou_et(A,A1), ou_et(B,B1),assoc(A1 & B1,C),!. ou_et(A | (B & C),F) :- ou_et((A | B) & (A | C),F),!. ou_et((A & B) | C, F) :- ou_et((A | C) & (B | C),F),!. ou_et(A | B,F):- ou_et(A,A1),ou_et(B,B1),not((A=A1,B=B1)), ou_et(A1 | B1, F),!. ou_et(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). ou_non(A | ~ B, A, B) :- ! . ou_non(A | B, A | Aplus, Amoins) :- ou_non(B, Aplus,Amoins). elt_ou(A,A | _) :- !. elt_ou(A,_ | A) :- !. elt_ou(X, _ | B) :- elt_ou(X,B),!. elt_ou_bis(N, A | _) :- elt_ou_bis(N, A),!. elt_ou_bis(N, A) :- A = seul(FX::Y,P), hyp(N,FX::Y,_), hyp(N,P,_), ecrire1(elt_ou_bis-'FX::Y'/(FX::Y)-'P'/P), !. elt_ou_bis(N, A) :- A = seul(FX::Y,Z=T), hyp(N,FX::Y,_), Y=Z, Y=T, ecrire1(elt_ou_bis-'FX::Y'/(FX::Y)-'Y'/Y-'Z'/Z-'T'/T), !. elt_ou_bis(N, _ | B) :- elt_ou_bis(N, B), ecrire1(elt_ou_bis_), !. ecrire1(L):- ligne, ecrire(L). ecrire_tirets(E) :- ligne, ecrire([---------------------------------------------------------]), ecrire(E). ecrire(_) :- version(casc),!. ecrire(E) :- (var(E) -> write(E) ;E = [X|L] -> ecrire(X), tab(1), ecrire(L) ;E=[] -> true ;ecrireAA(E) ). ecrireAA(T) :- numbervars(T,0,_,[singletons(true)]), write_term(T,[numbervars(true),max_depth(9)]), fail. ecrireAA(_). ecrireV(E) :- (var(E) -> write(E) ; (element(!,E);element(?,E);element(seul,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,ecrire1(M),appendd(F). message(Fich,M) :- tellling(F), appendd(Fich), probleme(Probleme), ecrire1(Probleme),ecrire1(M),appendd(F). traces(N,Nom,Cond,A,E,Expli,Antecedants) :- (Cond=[] -> true;ecrire1(['\n*** car',Cond])), ecrire1(['arcs',Antecedants-E]), ecrire1(Expli), assert(tracedem(N,Nom,Cond,A,E,Expli,Antecedants)). ecrire1ettrace(_,_,_,_):- ecrire1(ecrire1ettrace). limitertemps(TL) :- affecter(tempslimite(TL)). tptp :- ecrire1(' MENU TPTP\n'), ecrire1(['Pour demontrer un theoreme de la base TPTP,', 'appeler tptp avec comme arguments :', '\n un chemin ou un fichier ou un nom de probleme TPTP ', '\n ou un domaine et deux numeros i et j', '\n puis eventuellement un temps limite. ']), ecrire1(['Les parametres doivent etre ', 'des chaines ou des nombres Prolog valides.']), ecrire1('Ne pas oublier le point a la fin de l''appel.\n'), ecrire1( 'La preuve detaillee se trouvera dans le fichier res_'), ecrire1(' suivie par la trace constituee des seules etapes utiles'), ecrire1('Pour avoir la seule trace utile, utiliser la commande casc'), ecrire1(['\nExemples :', '\n tptp(''tptp/Problems/SET/SET027+4.p'').', '\n tptp(fichier_du_repertoire_courant).', '\n tptp(''copie_de_SET027+4.p'').', '\n tptp(''SET027+4.p'').', '\n tptp(''SET'',27,4).']), tempslimite(TL), ecrire1(['\nLe temps limite par defaut est',TL,'secondes.']), ecrire1(['Pour le modifier taper', '\n limitertemps().', '\nou le donner comme argument supplementaire', '(il sera alors modifie).']), ecrire1(['Pour le connaitre taper', '\n tempslimite(TL).']), ecrire1(['\nExemples :', '\n tptp(''tptp/Problems/SET/SET741+4.p'',25).', '\n tptp(fichier_du_repertoire_courant,40).', '\n tptp(''SET741+4.p'',25).', '\n tptp(''SET'',741,4,25).']). m :- [muscadet-frco]. t :- test. t1 :- abimpab. abimpab :- effacertout, tell(res_abimpab), demontrer(a & b => a & b). abimpac :- effacertout, demontrer(a & b => a & c). abimpcb :- effacertout, demontrer(a & b => c & b). aimpab :- effacertout, demontrer(a => a & b). pab :- effacertout, demontrer(p(a) & p(b) & q(b)=> ? [X]: (p(X) & q(X))). t2 :- aimpboua. aimpboua :- effacertout, tell(res_aimpboua), demontrer(a => b|a). test :- tptp('SET',2,4). tt :- tptp('SET',27,4). t3 :- effacertout, listetout,tptp(setegal). t3n :- effacertout, listetout,tptp(setegalnon). 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) :- limitertemps(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) :- ecrire1(['pas de fichier ni de probleme',CHouNOM]). tptp(X,Temps) :- ( number(Temps) -> T is Temps*2, limitertemps(T ), tptp(X) ; ecrire1([Temps,'n''est pas un nombre']) ). tptp(Nom,apartirde,I) :- name(Nom,[_,_,_,N,U,M|_]), name(NUM,[N,U,M]), ( NUM < I -> ecrire1([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) ; ecrire1([I,ou,J,'n''est pas un nombre']) ). tptp(Nom,apartirde,I,Temps) :- ( number(Temps)-> limitertemps(Temps),tptp(Nom,apartirde,I) ; ecrire1([Temps,'n''est pas un nombre']) ). tptp(DOM,I,J,Temps) :- (number(Temps)->limitertemps(Temps),tptp(DOM,I,J) ;ecrire1([Temps,'n''est pas un nombre']) ). tptp3(FICH,_,_) :- not(exists_file(FICH)), ecrire1(['pas de fichier ',FICH]),!. tptp3(FICH,REG,RES) :- message('---------------------------------------------------'), tempspasse(TP), affecter(probleme(FICH)), lire(FICH), charger_axioms, travail1, telll(REG), listingg(regle), l(type),l(priorite),l(definition),l(lemme), conjecture(Nom,TH), told,ecrire1('TH'=TH), telll(RES), ecrire1(FICH), ecrire1(Nom), demontrer(TH), statistics(cputime,Tapresdem),Tdem is Tapresdem-TP, appendd(RES), write('('),write(Nom),write(')'), messagetemps(Tdem), appendd(RES), etape(NH), ecrire1([en,NH,etapes]), statistics(cputime,Tavantutile), (concl(0,true,_) -> ligne, tracedemutile, statistics(cputime,Tapresutile), Tutile is Tapresutile-Tavantutile, ecrire1([tracedemutile,en,Tutile,seconds]), concat_atom(['tracedemutile en ',Tutile,' seconds'],TU), message(TU) ; Tapresutile = Tavantutile), ligne,ligne, toldd, affecter(tempspasse(Tapresutile))%, . messagetemps(Tdem) :- ecrire(' en '),ecrire(Tdem),ecrire(' seconds'), ecrire1(========================================), ecrire(========================================), toldd, told, ecrire(' en '),ecrire(Tdem), ecrire(' 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(lemme(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) -> remplacer(C,A,B,C1), assert(definition(Nomfof,!XX:C1)) ; true ), (Formule=(!_:(_=>(! XX :(A=B)))) -> assert(lemme(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,_,_], ecrire('Formule'=Formule), atom(Apply),atom(R) -> assert(lemme(Nomfof,Formule)), assert(definition(Nomfof,FT)) ; assert(lemme(Nomfof,Formule)) ), ( Formule=(!_:FT), FT=(A =>_),A=..[P,X|_],var(X)-> ajconcept(P) ; true ) ; ecrire1(type_de_fof_non_connu-FormuleTPTP) ), retract(fof(Nomfof,Nature,FormuleTPTP)), assert(fof_traitee(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 ; ecrire1('Variable d''environnement TPTP non definie') ). charger_axioms. casc :- ecrire1(' MENU TPTPU\n'), ecrire1(['Pour demontrer un theoreme de la base TPTP,', 'appeler casc avec comme arguments ', 'un chemin absolu ou relatif vers un probleme TPTP.' ]), ecrire1('Ne pas oublier le point a la fin de l''appel.\n'), ecrire1( 'La preuve utile sera sur la sortie standard (ontologie SZS).'), ecrire1('Pour avoir la recherche detaillee, utiliser la commande tptp.'), ecrire1(['\nExemples :', '\n casc(''/home/dominique/TPTP/TPTP-v3.5.0/Problems/SET/SET027+4.p'').', '\n casc(''tptp/Problems/SET/SET027+4.p'').', '\n casc(fichier_du_repertoire_courant).' ]), ecrire1(['\nIl n''y a pas de limite de temps.']). casc(FICH) :- effacer([version(_)]),assert(version(casc)), affecter(tempslimite(10000)), file_base_name(FICH,Probleme), affecter(probleme(Probleme)), lire(FICH), charger_axioms, travail1, conjecture(Nom,TH), message(['theoreme ',Nom]), demontrer(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(tempslimitepourladem=T1), affecter(tempslimite(T1)), file_base_name(Pb,Probleme), affecter(probleme(Probleme)), nl, write(probleme=Probleme), (exists_file(Pb) -> true; write('pas de fichier'-Pb)), lire(Pb), charger_axioms, travail1, conjecture(Nom,TH), message(['theoreme ',Nom]), demontrer(TH), statistics(cputime,Tapresdem), Tempstotaldem is Tapresdem-Tavanteffacertout, nl,write(tempstotaldem=Tempstotaldem),nl, tell(Res), (exists_file(Res)-> true;write('pas de fichier'-Res)), write(Tempstotaldem), nl, (concl(0, true,_) -> (conjecture(pas_de_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 :- ecrire1(' menu th'), ecrire1('Pour demontrer un theoreme dont l''enonce et les donnees (definitions et lemmes se trouvent dans un fichier f, appeler th(f).'), ecrire1('Le theoreme (unique) et les donnees doivent être ecrites de la facon suivante:'), ecrire1(' theoreme().'), ecrire1(' definition().'), ecrire1(' lemme().'), ecrire1('Ne pas oublier les points (termes Prolog).'), ecrire1('Exemple de fichier:'), ecrire1(' theoreme(![A,B,C]:(inc(A,B) & inc(B,C) => inc(A,C))).'), ecrire1(' definition(inc(A,B) <=> ! [X]:(X app A => X app B)).'). th(Fth) :- [Fth], forall((definition(A<=>B), functor(A,P,_)),assert(definition(P,A<=>B))), elifondef,consreg,theoreme(Th),demontrer(Th), affecter(conjecture('','')), affecter(probleme(probleme)), tracedemutile . regles_et([concl_et]). regles_univ( [!, elifon, concl_exi_all, stop_hyp_concl, stop1a,stop_hyp_false,concl_ou_stop3,concl_ou_stop3bis, hyp_contradiction, egal,egaldef, hyp_ou1,hyp_ou23,hyp_ou4,hyp_ou5, concl_non,hypnon,hypnonnon,hypnonimp,hypimp, concl_non_ou, concl_ou_non, hypequ, hypnonequ, concl_ou_et, =>,<=>, concl_seul,..,..1, concl_ilec1, concl_ilec2, concl_ilec3,concl_ilec4, concl_ilec5, concl_ilec1a,concl_ilec1b, concl_ilec_seul, concl_et_trivial_1,concl_et_trivial_2, concl_stop_trivial,concl_stop_trivial_ou, concl2pts ] ) . regles_defconcl1([def_concl_pred,defconcl1a,defconcl1b,defconcl1bb]). regles_defconcl2([defconcl2,defconcl2app,defconcl2elt, defconcl2a,defconcl2b,defconcl3]). regles_existe([ilexiste]). regles_ou([hyp_ou_cte, hyp_ou]). regles_concl_existe([concl_exi,creer_un_objet_image]). regle(N, elifon) :- concl(N, C, I), elifon( C, C1), nouvconcl(N, C1,I1),!, traces(N,regle(elifon), concl(N, C, I), nouvconcl(N, C1, I1), I1, ['elimination des symboles fonctionnels dans la conclusion', '\nfor example, p(f(X)) is replaced by only(f(X)::Y, p(Y)'], [I]). regle(N,stop_hyp_concl ):- concl(N,C,IC), ground(C), hyp(N,C,I/**/), nouvconcl(N,true,NouvelleEtape), traces(N, regle(stop_hyp_concl), (hyp(N,C,I),concl(N,C,IC)), nouvconcl(N,true,NouvelleEtape), (NouvelleEtape), ['la conclusion',C,'a demontrer est une hypothese'], ([IC,I]) ). regle(N,stop1a):- concl(N,C,IC), ( C=(?_:_);C=(!_:_);C=(_ | _);C=(_<=>_) ;C=seul(_::_,_) ), hyp(N,H,I), H =@= C, nouvconcl(N,true,I1), traces(N,regle(stop1a), (concl(N,C,IC),hyp(N,H,I)), nouvconcl(N,true,I1), I1, ['la conclusion',C,'a demontrer est une hypothese'], [IC,I] ), ecrire1ettrace(N,(concl(N,C,IC),hyp(N,H,I)), nouvconcl(N,true,I1),stop1a). regle(N,stop_hyp_false):- hyp(N,false,I), nouvconcl(N,true,I1), traces(N,regle(stop_hyp_false), hyp(N,false,I),nouvconcl(N,true,I1), I1, ['on a trouve une contradiction'], [I]). regle(N,concl_ou_stop3):-concl(N,A | B,I), hyp(N,H,II),elt_ou(H,A | B), nouvconcl(N,true,I1), traces(N,regle(concl_ou_stop3), (concl(N,A | B,I),hyp(N,H,II)), nouvconcl(N,true,I1),I1, 'un des elements de la conclusion disjonctive est une hypothese', [I,II] ). regle(N,concl_ou_stop3bis):-concl(N,A | B,I), elt_ou_bis(N,A | B), nouvconcl(N,true,I1), ecrire1ettrace(N,concl(N,A | B,I), nouvconcl(N,true,I1),concl_ou_stop3bis), traces(N,regle(concl_ou_stop3bis), concl(N,A | B,I), nouvconcl(N,true,I1),I1, concl_ou_stop3bis, [I]). regle(N,hyp_contradiction):- hyp(N,A,I), hyp(N,~ A,II), nouvconcl(N,true,I1), traces(N,regle(hyp_contradiction), (hyp(N,A,I), hyp(N,~ A,II)), nouvconcl(N,true,I1),I1, ['on a une contradiction'], [I,II] ). regle(N, egal) :- hyp(N, X=Y,I), A=X, B=Y, ecrire1([remplacer,B,par,A,propager, et, supprimer,B]), traitegal(N,A,B,I). regle(N, egaldef) :- hyp(N,E::X,I), atom(X), hyp(N,E::Y,J), atom(Y), \+ X == Y, ajhyp(N, X = Y, I1), ecrire1ettrace(N,(hyp(N,E:X,I), hyp(N,E:Y,J), \+ X == Y), ajhyp(N, X=Y, I1),egaldef), traces(N,regle(egadef), (hyp(N,E::X,I), hyp(N,E::Y,J), J), ajhyp(N, X=Y, I1),I1, [X,et,Y,'ont la meme definition'], [I,J] ). regle(N, hyp_ou1) :- hyp(N,A | A,I), \+ hyp_traite(N, A | A,_), ajhyp(N,A,E),assert(hyp_traite(N, A | A,E)), traces(N,regle(hyp_ou1),hyp(N,A | A,I), ajhyp(N,A,E),E, '\n*** car a | a = a',[I]). regle(N, hyp_ou23) :- hyp(N,A | B,I), elt_ou(X=X, A | B), \+ hyp_traite(N, A | B,_), assert(hyp_traite(N, A | B,I)). regle(N, hyp_ou4) :- hyp(N,A | B,I), \+ hyp_traite(N, A | B,_),hyp(N,A,_), assert(hyp_traite(N, A | B,I)). regle(N, hyp_ou5) :- hyp(N,A | B,I), \+ hyp_traite(N, A | B,_),hyp(N,B,_), assert(hyp_traite(N, A | B,I)). regle(N, concl_non) :- concl(N,~ A,I), ajhyp(N,A,I1), nouvconcl(N,false,I1), ecrire1ettrace(N,concl(N,~ A,I), (ajhyp(N,A,I1), nouvconcl(N,false,I1)), non), traces(N,regle(concl_non), concl(N,~ A,I), (ajhyp(N,A,I1), nouvconcl(N,false,I1)),I1, ['on suppose',A,'et on cherche une contradiction'], [I] ). regle(N, hypnonnon) :- hyp(N,~ ~ A,I), ajhyp(N, A, J), ecrire1ettrace(N, hyp(N,~ ~ A,I), ajhyp(N, A, J), hypnonnon), traces(N, regle(hypnonnon), hyp(N,~ ~ A,I), ajhyp(N, A, J),J, '\n*** car ~ ~ a = a', [I,J] ). regle(N, hypnonimp) :- hyp(N,~(A=>B),I),\+ hyp(N,A ,_), ajhyp(N,(A & ~ B),J), ecrire1ettrace(N,hyp(N,~(A=>B),I), ajhyp(N,(A & ~ B),J), hypnonimp), traces(N,regle(hypnonimp), hyp(N,~(A=>B),I), ajhyp(N,(A & ~ B),J), J, '\n*** car ~(a=>b) = (a&~b)', [I] ). regle(N, hypnonequ) :- hyp(N,~(A<=>B),_), \+ hyp(N,(A & ~ B) | (~ A & B),_), ajhyp(N,(A & ~ B) | (~ A & B),_). regle(N, hypequ) :- hyp(N,A <=> B,_),\+ hyp(N,(A & B) | (~ B & ~ A),_), ajhyp(N, (A & B) | (~ B & ~ A),_). regle(N, hypnon) :- hyp(N,~ A,I), concl(N,false,IC), nouvconcl(N,A,I1), traces(N,regle(hypnon), (hyp(N,~ A,I), concl(N,false,IC)), nouvconcl(N,A,I1),I1, ['on suppose',A,'et on cherche une contradiction'], [I,IC] ). regle(N, concl_non_ou) :- concl(N,~ A | B,I),ajhyp(N,A,I1),nouvconcl(N,B,I1), traces(N,regle(concl_non_ou), concl(N,~ A | B,I),(ajhyp(N,A,I1), nouvconcl(N,B,I1)),I1, ['on supppose',A,'et on doit montrer',B], [I] ). regle(N, concl_ou_non) :- concl(N,A | B,I), ou_non(A | B,Aplus,Amoins), ajhyp(N,Amoins,I1), nouvconcl(N,Aplus,I1), traces(N,regle(concl_ou_non), concl(N,A | B,I), (ajhyp(N,Amoins,I1), nouvconcl(N,Aplus),I1), I1, ['on suppose',Amoins, 'on retire',~ Amoins,'de la conclusion'], [I] ). regle(N,concl_ou_et) :- concl(N,A | B,I),ou_et(A | B,C),nouvconcl(N,C,I1), traces(N,regle(concl_ou_et), concl(N,A | B,I),nouvconcl(N,C,I1),I1, 'distributivite de | par rapport a &', [I] ). regle(N,=>) :- concl(N, A => B, IC), ajhyp(N, A, NouvelleEtape), nouvconcl(N,B,NouvelleEtape), traces(N, regle(=>), (concl(N, A => B, IC)), [ajhyp(N, A, NouvelleEtape), nouvconcl(N,B,NouvelleEtape)], (NouvelleEtape), 'pour demontrer H=>C, on suppose H et on doit demontrer C', ([IC]) ). regle(N,<=>) :- concl(N , A <=> B, E1), nouvconcl(N,(A => B) & (B => A), E2), traces(N,regle(<=>), concl(N, A <=> B, E1), nouvconcl(N,(A => B) & (B => A)), E2, ('on remplace A<=>B par (A=>B)&(B=>A)'), [E1]). regle(N, !) :- concl(N,(! XX : C), IC), etape(E), NouvelleEtape is E+1,affecter(etape(NouvelleEtape)), creer_objets_et_remplacer(N,XX,C,C1,Objets), nouvconcl(N, C1,NouvelleEtape), traces(N, regle(!), concl((0,! XX : C), IC), [creer_objets(Objets), nouvconcl(N, C1,NouvelleEtape)], (NouvelleEtape), 'on instancie la(les) variable(s) universelle(s) de la conclusion', [IC] ). regle(N, concl_seul) :- concl(N,seul(A::X,B),I), ( hyp(N,A::Y,II) -> ecrire1([remplacer,X,par,Y]), remplacer(B,X,Y,B1), nouvconcl(N,B1,I1), traces(N,regle(concl_seul), (concl(N,seul(A::X,B),I), hyp(N,A::Y,II)), nouvconcl(N,B1,I1), I1, X-est_remplace_par-Y-dans-B, [I,II]) ; var(X) -> creer_objet(N,z,X1), ajobjet(N, X1),ajhyp(N,A::X1,I1), remplacer(B,X,X1,B1), nouvconcl(N,B1,I1), traces(N,regle(concl_seul), concl(N,seul(A::X,B),I), (ajhyp(N,A::X1,I1),nouvconcl(N,B1,I1)), I1, ['creation de l\'objet',X1,'et de sa definition'], [I]) ; ecrire1([regle,seul,cas, non,prevu]) ). regle(N, ..) :- concl(N, ..[R, X, Y], I), C=..[R, X, Y], nouvconcl(N, C, I1), traces(N,regle(..), concl(N, ..[R, X, Y], I), nouvconcl(N, C, I1),I1, '\n*** car ..[r,a,b] = r(a,b)', [I] ). regle(N, ..1) :- concl(N, ..[F, X]::Y,I), Z=..[F, X], nouvconcl(N, Z::Y,I1), traces(N,regle(..1), concl(N, ..[F, X]::Y,I), nouvconcl(N, Z::Y,I1),I1, '\*** car ..[f,x] = f(x)', [I] ). regle(N,concl_exi_all) :- concl(N,(?[X]:(![Y]:(A=>C))),E), ajhyp(N,(![X]:(?[Y]:(A&(~C)))),E1), nouvconcl(N,false,E1), message(concl_exi_all), traces(N,regle(concl_exi_all), concl(N,(?[X]:(![Y]:(A=>C))),E), (ajhyp(N,(![X]:(?[Y]:(A&(~C)))),E1), nouvconcl(N,false,E1)),E1, 'raisonnement par l\'absurde', [E] ). regle(N, concl_ilec1) :- concl(N,(?[X]:C),I), (atom(X);var(X)),hyp(N,C,II), ground(C), nouvconcl(N, true, I1), remplacer((?[X]: C),X,_XX,CC), ecrire1ettrace(N,(concl(N, CC,I), hyp(N,C,II)), nouvconcl(N, true, I1),concl_ilec1), traces(N,regle(concl_ilec1), (concl(N, CC,I), hyp(N,C,II)), nouvconcl(N, true, I1),I1, ['l\'objet',X,'verifie la conclusion'], [I,II] ). regle(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), nouvconcl(N,true,I1), remplacer((?[X]:(B & C)),X,_XX,CC), traces(N, regle(concl_ilec2), ( concl(N, CC,I),hyp(N,B,II), hyp(N,C,III)), nouvconcl(N,true,I1), I1, ['l\'objet',X,'verifie la conclusion'], [I,II,III] ). regle(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), nouvconcl(N,true,I1), remplacer((?[X]: B | C),X,_XX,CC), ecrire1ettrace(N,(concl(N, CC,I), hyp(N,BouC,II)), nouvconcl(N,true,I1),concl_ilec3). regle(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), nouvconcl(N, true, I1), remplacer((?[X]: B => C),X,_XX,CC), ecrire1ettrace(N,(concl(N, CC,I),hyp(N,NBouC,II)), nouvconcl(N, true, I1),concl_ilec4). regle(N, concl_ilec5) :- concl(N, (?XX: (~ C)),I), nouvconcl(N,false,I1),ajhyp(N, (!XX:C),I1), ecrire1ettrace(N,concl(N, (?[X]:( ~ C)),I), (nouvconcl(N,false,I1),ajhyp(N, qqs(X,C),I1)), concl_ilec5). regle(N,concl_exi) :- ecrire1(concl_exi), concl(N, ? XX:C, Eexi), ecrire1(regle-concl_exi-XX-C), demconclexi(N,? XX:C, Eexi,EEE), ecrire1(regle-concl_exi-etape-EEE). regle(N, creer_un_objet_image) :- objet(N,X), fonction(F,1), FX =.. [F,X], \+ hyp(N,_::X,_), \+ hyp(N,(?_:(FX::Y)),_), ajhyp(N,(?[Y]:(FX::Y)),I1), traces(N,regle(creer_un_objet_image), [objet(N,X), fonction(F,1)], ajhyp(N,(?[Y]:(FX::Y)),I1),I1, creer_un_objet_image, [] ), ecrire1ettrace(N,creation, ajhyp(N,(?_:(FX::Y)),I1), creer_un_objet_image). regle(N, concl_et_trivial_1) :- concl(N, A & B, I), hyp(N, A, II), ecrire1([A, est, true]),nouvconcl(N, B, I1), ecrire1ettrace(N,(concl(N, A & B, I),hyp(N, A, II)), nouvconcl(N, B, I1), concl_et_trivial_1), traces(N,regle(concl_et_trivial_1), (concl(N, A & B, I),hyp(N, A, II)), nouvconcl(N, B, I1),I1, 'un des elements de la conclusion conjonctive est une hypothese', [I,II] ). regle(N, concl_et_trivial_2) :- concl(N, A & B,I), hyp(N, B, II), ecrire1([B, est, true]),nouvconcl(N, A, I1), ecrire1ettrace(N,(concl(N, A & B,I), hyp(N, B, II)), nouvconcl(N, A, I1), concl_et_trivial_2), traces(N,regle(concl_et_trivial_2), (concl(N, A & B,I), hyp(N, B, II)), nouvconcl(N, A, I1), I1, 'un des elements de la conclusion conjonctive est une hypothese', [I,II] ). regle(N, concl_stop_trivial) :- concl(N, A = A, I), nouvconcl(N,true, I1), ecrire1ettrace(N,concl(N, A = A, I), nouvconcl(N,true, I1), concl_stop_trivial), traces(N,regle(concl_stop_trivial), concl(N, A = A, I), nouvconcl(N,true, I1),I1, 'conclusion triviale', [I] ). regle(N, concl_stop_trivial_ou) :- concl(N, A | B, I), elt_ou(X=X,A | B), nouvconcl(N,true, I1), ecrire1ettrace(N,concl(N, A | B, I), nouvconcl(N,true, I1), concl_stop_trivial_ou), traces(N,regle(concl_stop_trivial_ou), concl(N, A | B, I), nouvconcl(N,true, I1),I1, 'un des elements de la conclusion disjonctive est triviale', [I] ). regle(N, concl_et) :- concl(N, A & B, Eavant ), demconj(N, A & B, Eavant, _Eapres), (concl(N, true, _) -> Expli=['tous les elements de la conclusion conjonctive du theoreme',N, 'ont ete demontres'] ; Expli=['tous les elements de la conclusion conjonctive du theoreme',N, 'n\'ont pas ete demontres'] )%, . regle(N, concl_ou ) :- concl(N, A | B, Eavant ), demdij(N, A | B, Eavant, _Eapres), (concl(N, true, EE),message(etapefinale-EE) -> Expli=['un des elements de la conclusion disjonctive du theoreme',N, 'a ete demontre'] ; Expli=['aucun element de la conclusion disjonctive du theoreme',N, 'n\'a ete demontre'] )%, . regle(N, def_concl_pred) :- concl(N, C, I), definition(Nomfof,C <=> D), ecrire1([N, 'definition de la conclusion']), nouvconcl(N, D, I1), traces(N, regle(def_concl_pred), concl(N, C, I), nouvconcl(N, D, I1), I1, ['on remplace la conclusion ',C,' par sa definition(fof',Nomfof,')'], [I] ). regle(N, defconcl1a) :- concl(N, C | A, I), definition(Nomfof,C <=> D), ecrire1([N, 'definition de la conclusion']), nouvconcl(N, D | A, I1), ecrire1ettrace(N,concl(N, A | C, I), nouvconcl(N, D | A, I1), defconcl1a), traces(N,regle(defconcl1a), concl(N, A | C, I), nouvconcl(N, A | D, I1),I1, [definition,Nomfof], [I] ). regle(N, defconcl1b) :- concl(N, A | C, I), definition(Nomfof,C <=> D), ecrire1([N, 'definition de la conclusion']), nouvconcl(N, A | D, I1), ecrire1ettrace(N,concl(N, A | C, I), nouvconcl(N, A | D, I1), defconcl1b), traces(N,regle(defconcl1b), concl(N, A | C, I), nouvconcl(N, A | D, I1),I1, [definition,Nomfof], [I]). regle(N, defconcl1bb) :- concl(N, A | seul(Y::X,seul(Z::T,C)), I), definition(Nomfof,C <=> ~ D), ecrire1([N, 'definition de la conclusion']), nouvconcl(N, A | ~ seul(Y::X,seul(Z::T,D)), I1), ecrire1ettrace(N,concl(N, A | seul(Y::X,seul(Z::T,C)), I), nouvconcl(N, A | ~ seul(Y::X,seul(Z::T,D)), I1), defconcl1bb), traces(N,regle(defconcl1bb), concl(N, A | seul(Y::X,seul(Z::T,C)), I), nouvconcl(N, A | ~ seul(Y::X,seul(Z::T,D)), I1),I1, [definition,Nomfof], [I] ). regle(N, concl2pts) :- concl(N, FX::Y, I), nouvconcl(N, seul(FX::Z, Z=Y), I1), traces(N,regle(concl2pts), concl(N, FX::Y, I), nouvconcl(N, seul(FX::Z, Z=Y), I1),I1, ' FX::Y is rewriten only(FX::Z, Z=Y)', [I] ) . regle(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 , remplacer(P, X, A, P1), ecrire1(['definition de la conclusion']), nouvconcl(N, P1, I1), ecrire1ettrace(N,(concl(N, C, I), hyp(N, D:B, II)), nouvconcl(N, P1, I1), defconcl2elt) , traces(N,regle(defconcl2elt), (concl(N, C, I), hyp(N, D::B, II)), nouvconcl(N, P1, I1),I1, [definition,Nomfof], [I,II] ) . regle(N, ilexiste) :- hyp(N, (?XX:P),I), \+ hyp_traite(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)) ) , etape(E), I1 is E+1, affecter(etape(I1)), creer_objets_et_remplacer(N,XX,P,P1,Objets), ajhyp(N,P1,I1), ajhyp_traite(N,(?XX:P),I), traces(N,regle(ilexiste), hyp(N,(?XX:P),I), [creer_objets(Objets), ajhyp(N,P1,I1)], I1, 'traitement de l\'hypothese existentielle', [I] ) . regle(N, hyp_ou) :- hyp(N, (A | B),I), \+ hyp_traite(N, (A | B),_), \+ (ou_applique(N)), concl(N, C, II), ecrire1([N,traitement,de,l,hypothese,disjonctivee,(A | B)]), hypou(A | B => C, T), nouvconcl(N,T, I1), traces(N,regle(hyp_ou), (hyp(N, A | B,I),concl(N, C, II)), nouvconcl(N,T, I1), I1, ['on doit montrer la conclusion dans les deux cas'], [I,II]), ajhyp_traite(N, (A | B),I1), assert(ou_applique(N)) . regle(N, hyp_ou_cte) :- hyp(N, A | B,I), \+ hyp_traite(N, A | B,_), \+ (ou_applique(N)), A=(A1=A2), B=(B1=B2), atom(A1), atom(A2), atom(B1), atom(B2), concl(N, C, II), ecrire1([N,traitement,de,l,hypothese,disjonctive,(A | B)]), hypou(A | B => C, T), nouvconcl(N,T, I1), traces(N,regle(hyp_ou_cte), (hyp(N, A | B,I),concl(N, C, II)), nouvconcl(N,T, I1),I1, ['on doit montrer la conclusion dans les deux cas'], [I,II] ), ajhyp_traite(N, A | B,I1), assert(ou_applique(N)) . orphelin(L) :- tracedem(_,_,_,_,_,_,L),var(L),!. orphelin(E) :- tracedem(_,_,_,_,_,_,L),member(E,L), (var(E)-> ecrire('il reste une variable dans tracedem'-L) ; E =\= 1), \+ tracedem(_,_,_,_,E,_,[_|_]). tracedemutile :- ecrire1('graphe : '), forall(tracedem(_,_,_,_,Etape,_,Antecedants), ecrire([Antecedants-Etape,''])), ( concl(0,true,Efin) -> bagof(B-A,C^D^E^F^G^tracedem(C,D,E,F,B,G,A),L1), etape(Efin), ( reachable(Efin,L1,L11), sort(L11,VT) -> nl,write('etapes utiles':L11), ecrire1('\n*****************\n* demonstration *\n*****************\n'), retractall(version(casc)), probleme(P), ecrire1('SZS output start proof for '), write(P), ecrire1('\n* * * * * * * * * * * * * * * * * * * * * * * *'), ecrire1('in the following, N is the number of a (sub)theorem'), ecrire1(' E is the current step'), ecrire1('hyp(N,H,E) means that H is an hypothesis of (sub)theorem N'), ecrire1('concl(N,C,E) means that C is the conclusion of (sub)theorem N'), ecrire1('obj_cte(N,C) means that C is a created object or a given constant'), ecrire1('addhyp(N,H,E) means add H as a new hypothesis for N'), ecrire1('newconcl(N,C,E) means that the new conclusion of N is C'), ecrire1(' (C replaces the precedent conclusion)'), ecrire1('a subtheorem N0-i or N0+i is a subtheorem of the (sub)theorem N0'), ecrire1(' N0 is proved if all N0-i have been proved (&-node)'), ecrire1(' or if one N0+i have been proved (|-node)'), ecrire1('the initial theorem is numbered 0'), nl, ecrire1('* * * theorem to be proved'), conjecture(_,TH), ecrire1(TH), ecrire1('\n* * * proof :'), ecrire1('\n* * * * * * theoreme 0 * * * * * *'), tracedemutile(VT), ecrire1('le theoreme initial 0 est donc demontre'), (conjecture(pas_de_conjecture,_) -> ecrire(' (pas de conjecture)') ;true), ecrire1('* * * * * * * * * * * * * * * * * * * * * * * *\n'), ecrire1('SZS output end proof for '), write(P),nl ; true ) ; ecrire1('theoreme initial non demontre') ). tracedemutile([U|LU]) :- tracedem(_N,Nom,Cond,Act,(U),Expli,_Antecedants), ecriretrace(Act), (Cond=[] -> true ;ecrire1(['\n*** car',Cond])), ecrire1('\n*** explication : '),ecrire(Expli), ecrire_tirets(Nom), tracedemutile(LU). tracedemutile([]). ecriretrace([Act|AA]) :- ecriretrace(Act), ecriretrace(AA),!. ecriretrace([]). ecriretrace(ajhyp(N,A & B,E)) :- ecriretrace(ajhyp(N,A,E)), tab(1), ecriretrace(ajhyp(N,B,E)),!. ecriretrace(ajhyp(N,seul(FX::Y,A),E)) :- hyp(N,FX::Obj,Eobj), remplacer(A,Y,Obj,A1), (E=Eobj -> ecriretrace(ajhyp(N,FX::Obj,E)),nl,tab(5) ; true), ecriretrace(ajhyp(N,A1,E)),!. ecriretrace(creersousth(N,N1,_A,_E)) :- ecrire1(['\n* * * * * * creation * * * * * * sous-theoreme', N1,'* * * * *']), ecrire1(['toutes les hypotheses du (sous-)theoreme',N, 'sont hypotheses du sous-theoreme',N1]). ecriretrace(creer_objets(OO)) :- ecrire1(['creer objet(s)',OO]). ecriretrace(E) :- ecrire1(['***',E]).