%% Copyright 2008 Crip5 Dominique Pastre %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Muscadet version 4.0a %% %% 05/16/11 %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% muscadet-en is the English Prolog version of MUSCADET %% call by the Unix script musca-en %%%%%%%%%%%%%%%%%% %% declarations %% %%%%%%%%%%%%%%%%%% :-dynamic hyp/3. :-dynamic hyp_traite/3. :-dynamic hyp_traite/2. :-dynamic ou_applique/1. :-dynamic concl/3. :-dynamic lien/2. :-dynamic subth/2. :-dynamic objet/2. :-dynamic rulactiv/2. :-dynamic rule/2. :-dynamic concept/1. :-dynamic fonction/2. :-dynamic type/2. :-dynamic avecseulile/0. :-dynamic definition/2. :-dynamic definition/1. :-dynamic definition1/2. %1. :-dynamic lemme/2. :-dynamic lemme1/2. :-dynamic version/1. :-dynamic ecrireconsreg/0. :-dynamic timelimit/1. :-dynamic tempspasse/1. :-dynamic temps_debut/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 step/1. :- dynamic nbhypexi/1. :- dynamic display/1. :- dynamic lang/1. :- dynamic chemin/1. :- dynamic res/1. :- dynamic theoreme/1. :- dynamic th/1. :- dynamic theoreme/2. :- dynamic theorem/2. :- dynamic include/1. priorites(avec). probleme(pas_encore_de_probleme). version(th). timelimit(740). tempspasse(0). temps_debut(0). conjecture(false,false). seulile(niouininon). avecseulile. lang(en). fr :- assign(lang(fr)). en :- assign(lang(en)). display(pr). :-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(400,fx,/). :- op(600,fx,si). :- op(610,xfx,alors). :- op(600,fx,if). :- op(610,xfx,then). c :- consreg. l(P) :- listing(P). ll(P) :- listingg(P). rule(Nom) :- clause(rule(_,Nom ),Q), ecrire1(Q). %%%%%%%%%%%%%%%%%%%%%%%%%% %% inference engine %% %%%%%%%%%%%%%%%%%%%%%%%%%% applyrulactiv(N) :- repeat, ( concl(N, true, _) -> demontre(N) ; concl(N, _/timeout, _) -> !, nondemontre(N) ; rulactiv(N,LR) -> ( applyrul(N,LR)-> fail ;! ) ) . applyrul(N,_) :- tempsdepasse(N,applireg),!,nondemontre(N),fail. applyrul(N,[R|RR]) :- (rule(N,R ) -> acrire_tirets(tr,fr([regle,R])/en([rule,R])) ; applyrul(N,RR) ) . applyrul(N,[]) :- nondemontre(N), fail. tempsdepasse(N,Marqueur) :- statistics(cputime,T),!, tempspasse(TP),timelimit(TL), TT is TP+TL , T>TT, ( concl(N,C, _) -> newconcl(N,C/timeout, _) ; true ), concat_atom(['temps limite depasse N=',N,' dans ',Marqueur, '\ntheoreme 0 non demontre en ',T,' secondes\n'],Messagefr), concat_atom(['time over N=', N,' dans ',Marqueur, '\ntheorem 0 not proved in ',T,' seconds\n'],Messageen), acrire1(tr,fr(Messagefr)/en(Messageen)),nl, message(fr(Messagefr)/en(Messageen)), !, break . demontre(N) :- acrire1(tr,fr([theoreme,N,demontre])/en([theorem,N,proved])), ( N=0 -> ( version(tptp),conjecture(false,_) -> message(fr('pas de conjecture, probleme montre insatisfaisable') /en('no conjecture, problem proved unsatisfiable')) ; message(fr('theoreme 0 demontre')/en('theorem 0 proved')) ), ( display(tr) -> true ; version(casc) -> true ; ecrire1(fr('theoreme 0 demontre ')/en('theorem 0 proved ')) ), probleme(P), temps_debut(TD), statistics(cputime,Tapresdem),Tdem is Tapresdem-TD, ( version(tptp), conjecture(NomConj,_) -> Nom=NomConj ; version(th),(theoreme(NomTh,_);theorem(NomTh,_)) -> Nom=NomTh ), concat_atom(['(',Nom,')'],Texte), (version(casc) ->true ; Nom='' -> true ; ecrire(Texte) ), (version(casc)->true;messagetemps(Tdem)), ligne(szs), (display(szs) -> ( conjecture(false,_) -> ecrire1('SZS status Unsatisfiable for ') ; ecrire1('SZS status Theorem for ') ), probleme(P),ecrire(P) ; true ), ligne(szs), ( display(szs)-> ecrire1('SZS output start proof for '), write(P) ; true ), ( display(pr) -> ligne, statistics(cputime,Tavantutile), tracedemutile, ( version(casc) -> true ; statistics(cputime,Tapresutile), Tutile is Tapresutile-Tavantutile, acrire1(tr,fr('preuve extraite')/en('extracted proof')), message(fr('preuve extraite')/en('extracted proof')), messagetemps(tr,Tutile) ), ( display(szs) -> ecrire1('SZS output end proof for '), write(P) ; true ) ; true ) ; true ) . nondemontre(N) :- acrire1(tr,[theoreme,N,non,demontre]), ( N=0 -> message('theoreme non demontre'), ( display(_) -> true; ecrire1([theoreme,non,demontre])), ( display(szs) -> nl,nl, write('SZS status GaveUp for '), probleme(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) ). elt_seq(X,(X,_)). elt_seq(X,(_,S)) :- elt_seq(X,S). elt_seq(X,X) :- \+ X=(_,_). der_seq(D,(_,S)):- der_seq(D,S),!. der_seq(X,X). seq_der((S1,S2,S3),(S1,SS),Der) :- seq_der((S2,S3),SS,Der),!. seq_der((S1,S2),S1,S2):-!. seq_der(S,S,S) :- message([S, 'n''a qu''un element']). arbre(E,Indent) :- E=..[Op,A,B],(Op=ou;Op=et),nl,indent(Indent), write(Op),I is Indent+1,arbre(A,I),arbre(B,I),!. arbre([],_) . arbre(E,Indent) :- nl,indent(Indent),write(E). indent(N) :- write(' '),(N>0 -> N1 is N-1, indent(N1);true). arg_exp(A,E) :- E =..[_,X|[L]], ( A=X ; A=L ; arg_exp(A,L) ). 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_ct(_,_) -> ajoufinseq(S,A,SA) ; S=(obj_ct(_,_),L) -> SA = (A,S) ; S = (X,L) -> ajouseqavantobjet(L,A,L1), SA = (X,L1) ; S = [] -> SA = A ; S = obj_ct(_,_) -> SA = (A,S) ; SA = (S,A) ) . obj_ct(N,X) :- objet(N,X) ; objet(-1,X). assign(X) :- X =.. [P,_],Y=..[P,_],retractall(Y),assert(X),!. assign(X) :- X =.. [P,_,_],Y=..[P,_,_],retractall(Y),assert(X),!. assign(X) :- X =.. [P,A,_,_],Y=..[P,A,_,_],retractall(Y),assert(X),!. nbhypexi(0). incrementer_nbhypexi(N1) :- nbhypexi(N), N1 is N+1, assign(nbhypexi(N1)). step_action(E1) :- ( var(E1),step(E) -> E1 is E+1,assign(step(E1)) ; true). tartip(X1,X2) :- name(X1,L1),compareg1ter(L1,L2),name(X2,L2). 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) ; acrire1(tr,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). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% super-actions %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% travail1 :- (ecrireconsreg -> telll(traceconsreg);true), verifdef,elifundef, consreg, typesdonnees, told. typesdonnees :- clause(rule(_,Nom),_), \+ type(Nom,_), assert(type(Nom,donnee)),fail. typesdonnees. demontr(_Theoreme) :- tempsdepasse(0, 'temps depasse avant meme d attaquer le theoreme'). demontr(Theoreme) :- ( version(casc) -> true ; shell('echo `hostname`\. > zzzmachine;echo >> zzzmachine'), see(zzzmachine),read(HostName),seen, ecrire1(machine:HostName) ), ( version(casc) -> true ; ecrire1('****************************************'), ecrire('****************************************'), ecrire1([fr('theoreme a demontrer')/en('theorem to be proved')]), ecrire1([Theoreme]), ecrire_tirets('') ), assign(step(0)), newconcl(0, Theoreme, E), traces(0, action(ini), [], newconcl(0 , Theoreme, E), E,fr('theoreme initial')/en('initial theorem'),[] ), acrire_tirets(tr,[action,ini]), \+ tempsdepasse(0, 'temps depasse avant meme d activer les regles'), activrul, \+ tempsdepasse(0, 'temps depasse apres l activation des regles'), applyrulactiv(0 ), ! . creersubth(N,N1,A,E) :- assert(subth(N,N1)), ligne(tr),acrire1(tr,[************************************************]), acrire(tr,[fr(sous-theoreme)/en(subtheorem), N1,*****]), newconcl(N1,A,E), copitem(N,N1). proconj(_N,_C,_Econj) :- message(z_demconj, normalement_y_a_plus). proconj(N,C,Econj, Efin) :- ( C = (A & B) -> true ; (C=A,B=true) ), atom_concat(N,-,N0), gensym(N0,N1), creersubth(N,N1,A,Ecreationsousth), (B=true -> Cond=[], Expli_fr='demonstration du dernier element de la conjonction', Expli_en='proof of the last element of the conjunction' ; Cond=concl(N, C, Econj), Expli_fr='pour demontrer une conjonction, on demontre successivement tous les elements de la conjonction', Expli_en='to prove a conjunction, prove all the elements of the conjunction' ), traces(N1,action(fr(demconj)/en(proconj)), Cond, [creersubth(N,N1,A,Ecreationsousth), newconcl(N1,A,Ecreationsousth)], (Ecreationsousth), fr(Expli_fr)/en(Expli_en), ([Econj]) ), acrire_tirets(tr,[action,fr(demconj)/en(proconj)]), applyrulactiv(N1), !, concl(N1,true,Edemsousth), newconcl(N,B,Eretourth), traces(N,action(fr(retourdem)/en(returnpro)), concl(N1,true,Edemsousth), newconcl(N,B,Eretourth), (Eretourth), [fr('la conclusion')/en('the conclusion'), A, fr('du (sous-)theoreme')/en('of (sub)theorem'), N, fr('a ete demontree ( sous-theoreme') /en('has been proved ( subtheorem/'), N1,')' ], ([Econj , Ecreationsousth,Edemsousth]) ), acrire_tirets(tr,[action,fr(retourdem)/en(returnpro)]), ( B = true -> Eretourth=Efin ; proconj(N,B,Eretourth,Efin)) . demdij(N,C,Edij, Efin) :- ( C = (A | B) | (C = A , B=true) ), atom_concat(N,+,N0), gensym(N0,N1), creersubth(N,N1,A,Ecreationsousth), traces(N,action(fr(demdij)/en(propij)),(concl(N, C, Edij)), creersubth(N,N1,A,Ecreationsousth), (Ecreationsousth), [fr('creation du sous-theoreme')/en('creation of subtheorem'), N1, fr('de conclusion')/en('with conclusion'), A], ([Edij])), acrire_tirets(tr,[action,demdij]), applyrulactiv(N1), !, concl(N1,C1,Edemsousth), ( C1=true -> newconcl(N,true,Eretourth), traces(N, action(fr(retourdemdij)/en(returnpropij)), (sousthdem), newconcl(N,true,Eretourth), (Eretourth), [fr('la conclusion')/en('the conclusion'), A, fr('du (sous-)theoreme')/en('of (sub)theorem'), N, fr('a ete demontree')/en('has been proved')], ([Edij , Edemsousth]) ), acrire_tirets(tr,[action,fr(retourdemdij)/en(returnpropij)]) ; B \=true -> acrire_tirets(tr,[action,retourdemdij]), acrire1(tr,'on eie al disjonction suivante'), demdij(N,B,Edij,Efin) ; acrire1(tr,'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) ; acrire1(tr,[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), assert(hyp_traite(M,H)) , fail. copitem(N,M) :- objet(N, H), assert(objet(M,H)) ,fail. copitem(N,M) :- rulactiv(N, LR), assert(rulactiv(M,LR)), fail. copitem(_, _) . proconclexi(N, ? [X|XX]:C, Eexi, Efin):- obj_ct(N,Ob), acrire1(tr,fr(['*** on essaie',Ob,'***']) /en(['***',Ob,'is tried','***']) ), atom_concat(N,+,N0), gensym(N0,N1), remplacer(C,X,Ob,C0), ( XX=[] -> C1=C0 ; C1= (?XX:C0)), creersubth(N,N1,C1,Ecreationsousth), traces(N1, action(fr(demconclexi)/en(proconclexi)), concl(N, ? [X]:C, Eexi), [creersubth(N,N1,C1,Ecreationsousth), newconcl(N1,C1,Ecreationsousth)], Ecreationsousth, fr(['on essaie',Ob,'pour la variable existentielle']) /en([Ob,'is tried for the existential variable']), [Eexi] ), acrire_tirets(tr,[action,fr(demconclexi)/en(proconclexi)]), applyrulactiv(N1), ( concl(N1, true, E1) -> newconcl(N,true,Efin), traces(N, action(fr(retourdemexi)/en(returnproexi)), concl(N1, true, E1), newconcl(N,true, Efin), Efin, [fr('la conclusion du (sous-)theoreme') /en('the conclusion of subtheorem'), N, fr('a ete demontree (sous-theoreme') /en('has been proved (subtheorem'), N1,')'], [Eexi, E1] ) ; acrire1(tr,fr('on essaie l\'objet suivant') /en('the following object is tried') ), fail ). newconcl(N,C, E2) :- \+ concl(N, C, _), step_action(E2), (C = (..[R, X, Y])-> (C1 =..[R, X, Y]);C1=C), assign(concl(N,C1,E2)), acrire1(tr,[E2:N,newconcl(C1)]). addhyp(N, H, E2) :- step_action(E2), ( H = (A & B) -> addhyp(N, A, E2), addhyp(N,B, E2) ; hyp(N, H,_) -> true ; H = (X = X) -> true ; H =(X,A) -> ( var(I1) -> step(I), I1 is I+1, assign(step(I1)) ; true), assert(hyp(N,H,I1)), create_objet(N,z,X1), remplacer(A,X,X1,A1), addhyp(N,A1,I1) ; H = (Y=X), atom(X), atom(Y), before(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),message(z_a_voir,Y-Y1) ; H=seul(A::X,Y)-> ( hyp(N,A::X1,_I) -> acrire1(tr,[remplacer,X,par,X1,dans,Y]) ; create_objet(N,z,X1),addhyp(N,A::X1, E2) ), remplacer(Y,X,X1,Y1),addhyp(N,Y1,E2) ; H = (~ seul(FX::Y,P)) -> addhyp(N,seul(FX::Y, ~ P ), E2) ; H = (!_: _) -> ( var(E2) -> step(E0), E2 is E0+1, assign(step(E2)) ; true), atom_concat(r_hyp__,E2,ReghypE2), atom_concat(ReghypE2,'__',Reghyp), acrire1(tr,[E2:N,fr('traiter l\'hypothese universelle') /en('treat the universal hypothesis'), H]), create_name_rule(Reghyp,Nom), buildrules(H, _,Nomfof,N+H,Nom,[],[E2]) ; H = (~ (?XX:A)) -> create_name_rule(r_hyp,Nom), buildrules( (!XX:(~ A)), _, Nomfof, N+H, Nom, [],[]) ; H = (A =>B) -> create_name_rule(r_hyp,Nom), buildrules( H,_,Nomfof,N+H,Nom,[],[]) ; ( var(E2) -> step(E0), E2 is E0+1, assign(step(E2)) ; true ), assert(hyp(N, H,E2)), acrire1(tr,[E2:N,addhyp(H)]), (H=p(X) -> ajobjet(N,X) ; H=q(X) -> ajobjet(N,X) ; true ) ) . before(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), acrire1(tr,[E:N, fr('ajouter objet')/en('add object'),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)), create_name_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, [fr('a cause de')/en(because),P,et,NonP], [I] ) )), assert(type(Nom,P)), fail. consreg :- definition(Nomfof, A<=>B), not(var(A)), (ecrireconsreg-> ecrire1(definition(A<=>B));true), ( A=(C::_) -> C =..[P|_] ; A=..[_,_,E],not(var(E)),E=..[_|_] -> fail ; A=..[P|_] ), (ecrireconsreg-> ecrire1(definitionapres(A<=>B));true), ajconcept(P), create_name_rule(P,Nom), (A=(X=Y)-> remplacer(B,Y,X,B1),buildrules(B1,N,Nomfof,P,Nom,objet(N,X),[]) ; buildrules(A=>B,_,Nomfof,P,Nom,[],[]), (ecrireconsreg -> ecrire1('+++consreg contraposee'/A=>B);true), (B = (_ | _) -> buildrules(B=>A,_,Nomfof,P,Nom,[],[]);true) ), fail. consreg :- definition(Nomfof,A=B), not(B=[_,_]), A =.. [F|_], ajconcept(F), create_name_rule(F,Nom), elifun4(B::X,B1X), buildrules(A::X => B1X,_,Nomfof,F,Nom,[],[]), fail. consreg :- definition(Nomfof,A<=>D), (ecrireconsreg -> ecrire1(definitionelt(A<=D));true), ( A =..[R,X,E],not(var(E)),E=..[F|_] ) , ajconcept(F), create_name_rule(F,Nom), ( atom(E) -> (ecrireconsreg -> ecrire1(definitioneltapres1(![X]:(A =>D)));true), buildrules((![X]:(A =>D)),_,Nomfof,F,Nom,[],[]) ; XappW =.. [R,X,W], (ecrireconsreg -> ecrire1(definitioneltapres2((E::W)=>![X]:(XappW <=>D)));true), buildrules((E::W)=>![X]:(XappW <=>D),_,Nomfof,F,Nom,[],[]) ), fail. consreg :- lemme(Nomfof,E),atom_concat(Nomfof,'_',Nom0), create_name_rule(Nom0,Nom1), buildrules(E,_,Nomfof,lemme,Nom1,[],[]), fail. consreg. buildrules(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. buildrules(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. buildrules(N,_,_,_,_,_,_) :- tempsdepasse(N,'temps epuise avant la fin de la construction des regles'). buildrules(E,N,Nomfof,Concept,Nom,Cond,Antecedants) :- \+ tempsdepasse_ltb(consreg), ( 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) -> remplacer(Cond,X,Y,Cond1), remplacer(C,X,Y,C1) ; var(Y) -> remplacer(Cond,Y,X,Cond1), remplacer(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_name_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_name_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, [fr('condition suffisante (regle : ') /en('sufficient condition (rule : '), Nom,'(fof',Nomfof,')' ], [I]), Regle), ajoureg(N, Concept, Nom_cs, Regle) , create_name_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, 'condition suffisante', 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_name_rule(Nom, Nom1),buildrules(A,N,Nomfof,Concept,Nom1,Cond,Antecedants), create_name_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 = seul(FX::Y, B) -> ajoucond(N,Cond,Antecedants,FX::Y,Cond1,Antecedants1), buildrules(B,N,Nomfof,Concept,Nom,Cond1,Antecedants1), ( seulile(oui),seulile(non)->true ; seulile(non)-> true ; seulile(oui) -> atom_concat(Nom, '_crea_seul', Nom2), create_name_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 = (_=_) -> Cond=Cond0, ajoufinseq(Cond, \+ E, Cond1), ajoufinseq(Cond1, addhyp(N,E,I1), CondAct2), Act=addhyp(N,E,I1), ( Cond0=[] -> SiAlorsAct=Act ; ( lang(fr) -> SiAlorsAct = (si Cond0 alors Act) ; lang(en) -> SiAlorsAct = (if Cond0 then Act) ; SiAlorsAct = '...' ) ), copy_term(SiAlorsAct,SiAlorsActCop), ( Concept=(_ + HypUnivImp) ->assign(zut(HypUnivImp)), zut(HypU), Expli = [fr('la regle')/en('the rule'),Nom,:, SiAlorsActCop, fr('\nest une regle locale construite a partir de l\'hypothese universelle') /en('\nis a local rule built from the universal hypothesis'), HypU] ; Concept=lemme -> Expli = [fr(regle)/en(rule),SiAlorsActCop, fr('construite a partir de l\'axiome') /en('built from the axiom'), Nom,'(fof',Nomfof,')'] ; Expli= [fr(regle)/en(rule),SiAlorsActCop, fr('\nconstruite a partir de la definition de') /en('\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, [fr('a cause de')/en(because),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, [fr('a cause de')/en(because),Concept], Antecedants ), Regle ), ajoureg(N, Concept, Nom, Regle) ; E = (A | B),definition(Nomfof,A <=> ~ A1), A =..[_|L],vars(L), A1 =..[_|_] -> acrire1(tr,'consreg ou1 non Nom/E'=Nom/E), sup_objet(Cond,Cond0), ajoufinseq(Cond, \+ hyp(N,E,_), Cond1) , ajoufinseq(Cond1, addhyp(N,E,I1), CondAct2), atom_concat(Nom, ounonpourquoi, Nom11), create_name_rule(Nom11,Nom1), ecrire1(12731273127312731273),message(12731273127312731273), ajoufinseq(CondAct2, ecrire1ettrace(1273,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, [fr('a cause de')/en(because),Concept], Antecedants ), Regle2 ), buildrules(B,N,Nomfof,Concept,Nom1,Regle2,Antecedants) ; E = (B | A),definition(Nomfof,A <=> ~ A1), A =..[_|L],vars(L), A1 =..[_|_] -> acrire1(tr,'consreg ou2 non Nom/E'=Nom/E), sup_objet(Cond,Cond0), ajoufinseq(Cond, \+ hyp(N,E,_), Cond1) , ajoufinseq(Cond1, addhyp(N,E,I1), CondAct2), atom_concat(Nom, ounonpourquoi, Nom11), create_name_rule(Nom11,Nom1), ajoufinseq(CondAct2, traces(N,rule(Nom1), Cond0,addhyp(N,E,I1),I1, [fr('a cause de')/en(because),Concept], Antecedants ), Regle1 ), ajoureg(N, Concept, Nom1, Regle1), ajouseqavantobjet(Cond, A1, Cond3), ajoufinseq(Cond3, traces(N,rule(Nom1), Cond,addhyp(N,E,EE),EE, [fr('a cause de')/en(because),Concept], Antecedants ), Regle2 ), buildrules(B,N,Nomfof,Concept,Nom1,Regle2,Antecedants) ; \+tempsdepasse(-1,'consreg par defaut'), Cond=Cond0, ajoufinseq(Cond, \+ hyp(N,E,_), Cond1), Act=addhyp(N,E,I1), ajoufinseq(Cond1, Act , CondAct2), ( E = (?_:_) -> Priorite = 2, atom_concat(Nom, exist, Nom1) ; E = (_ | _) -> Priorite = 2, atom_concat(Nom, ou, Nom1) ; Nom = Nom1, Priorite = 1), create_name_rule(Nom1,Nom2), assert(priorite(Nom2,Priorite)), (Cond0=[] -> SiAlorsAct=Act ; ( lang(fr) -> SiAlorsAct = (si Cond0 alors Act) ; lang(en) -> SiAlorsAct = (if Cond0 then Act) ; SiAlorsAct = '...' ) ), copy_term(SiAlorsAct,SiAlorsActCop), ( Concept=(_ + HypUnivImp) ->assign(zut(HypUnivImp)), zut(HypU), Expli = [fr('la regle')/en('the rule'),Nom2,:, SiAlorsActCop, fr('\nest une regle locale construite a partir de l\'hypothese universelle') /en('\nis a local rule built from the universal hypothesis'), HypU] ; Concept=lemme -> Expli = [fr(regle2)/en(rule),SiAlorsActCop, fr('\nconstruite a partir de l\'axiome') /en('\nbuilt from the axiom'), Nomfof] ; Expli= [fr(regle2)/en(rule),SiAlorsActCop, fr('\nconstruite a partir de la definition de') /en('\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), \+ tempsdepasse(-1,avant_ajoureg), ajoureg(N, Concept , Nom2, Regle) ). sup_objet((X,L),L1) :- (X = obj_ct(_,_)|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_ct(_,_)|X=objet(_,_)), !. sup_objet(X,X). ajoucond(_,C,A,_) :- acrire1(tr,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)) -> acrire1(tr,'??????????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_ct(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,Step),CA), ajoufin(An,Step,AnA) ) . ajoureg(N, Arg, Nom, Corps) :- sup_cond_equal(Corps, Corps0), (ecrireconsreg -> nl,ecrire1('apres sup_cond_equal'-Corps0);true), ( Arg=(Nsth+H) -> step(E),assert(reglehypuniv(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) -> remplacer(Corps1,X,Y,Corps2) ; var(Y) -> remplacer(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), acrire1(tr,[E:Arg, fr('ajouter la regle active locale') /en('add the local rule')]), ecrire_simpl_R(tr,R), acrire1(tr,fr('a la fin des regles universelles') /en('at the end of universal rules')), ligne(tr), assert(type(Nom,Arg)), regles_univ(LRU),append(LRU,LRNU,LR), ( compareg(Corps,LRNU,L2,R3,L3) -> append([R3,Nom|L2],L3,NLR), acrire1(tr,[et,mettre,R3,avant]),ligne(tr) ; 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)), acrire1(tr,[N,fr('supprimer la regle active')/en('remove active rule'), Nom]). desactiver(_,_). activrul :- acti_link, acti_univ, acti_enpremier, acti_ro, acti_et, acti_def1, acti_exist, acti_ou, acti_def2, acti_concl_exist, 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. tempsdepasse_ltb(Pred) :- (atom_concat(traitile,_,Pred)-> ecrire1(pred);true), tempsdepasse(-1,Pred). acti_link :- forall(concept(C),assert(lien(0,C))). acti_univ :- regles_univ(LR), assert(rulactiv(0,LR)). acti_ro :- priorites(sans), rulactiv(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(rulactiv(_,_)),assert(rulactiv(0,LRR)), fail. acti_ro :- priorites(avec), rulactiv(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(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_et :- rulactiv(0,LR), regles_et(RET), append(LR,RET,LRR), retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)). acti_ou :- rulactiv(0,LR), regles_ou(ROU), append(LR,ROU,LRR), retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)). acti_def1 :- rulactiv(0,LR), regles_defconcl1(RR), append(LR,RR,LRR), retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)). acti_def2 :- rulactiv(0,LR), regles_defconcl2(RR), append(LR,RR,LRR), retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)). acti_exist :- rulactiv(0,LR),regles_exist(RILE),append(LR,RILE,LRR), retractall(rulactiv(_,_)),assert(rulactiv(0,LRR)). acti_concl_exist :- rulactiv(0,LR), regles_concl_exist(RILE), append(LR,RILE,LRR), retractall(rulactiv(_,_)), assert(rulactiv(0,LRR)). ordoreg. compareg(_,_,_,_,_) :- fail. compareg1ter([I1,I2,X,X|L],[I3,I6,I4,I5|L]) :- I3 is I1+1, I4 is I2-1, I5 is I4-1, I6 is I5-1. hyp_traite(N,H,E) :- message(z_hyp_traite_a_3_arg,N+H+E), hyp_traite(N,H). traitequal(N,X,Y,Ixy) :- \+ tempsdepasse(N,traitequal), acrire1(tr,traitequal-N-X-Y-Ixy),fail. traitequal(N, X, Y, Ixy) :- \+ tempsdepasse_ltb(traitequal1), hyp(N, H,I), \+ H =(X=Y), remplacer(H,Y,X,H1),\+ H=H1, retract(hyp(N,H,_)), \+ hyp(N, H1,_), addhyp(N, H1,I1), traces(N,fr('action(traitequal_hyp)')/en('treatequal_hyp'), (hyp(N,X=Y,Ixy),hyp(N,H,I)), addhyp(N, H1,I1),I1, fr(['on remplace',Y,par,X,'dans les hypotheses']) /en([Y,'is replaced by',X,'in the hypotheses']), [I,Ixy] ), acrire1(tr,fr('-------------------------------- action traitequal_hyp') /en('-------------------------------- action treatequal_hyp')), fail. traitequal(N, X, Y,_) :- \+ tempsdepasse_ltb(traitequal2), hyp_traite(N, H), \+ H =(_=_), remplacer(H,Y,X,H1),\+ H=H1, retract(hyp_traite(N,H)), \+ hyp(N, H1, _), acrire1(tr,'et apres'), ajhyp_traite(N, H1), fail. traitequal(N,X,Y,Ixy) :- \+ tempsdepasse_ltb(traitequal3), concl(N, X=Y,I), newconcl(N, true,I1), traces(N,action(fr('traitequal_concl=')/en('treatequal_concl=')), (hyp(N,X=Y,Ixy),concl(N, X=Y,I)), newconcl(N, true,I1),I1, fr(['on remplace',Y,par,X,'dans la conclusion']) /en([Y,'is replaced by',X,'in the conclusion']), [I,Ixy] ), acrire1(tr,fr('-------------------------------- traitequal_concl=') /en('-------------------------------- treatequal_concl=')). traitequal(N,X,Y,Ixy) :- \+ tempsdepasse_ltb(traitequal4), concl(N, C, I), remplacer(C, Y,X,C1), \+ C=C1, newconcl(N, C1, I1), traces(N,action(fr(traitequal_concl)/en(treatequal_concl)), (hyp(N,X=Y,Ixy),concl(N, C, I)), newconcl(N, C1, I1),I1, fr(['on remplace',Y,par,X,'dans la conclusion']) /en([Y,'is replaced by',X,'in the conclusion']), [I,Ixy] ), acrire1(tr,fr('-------------------------------- traitequal_concl') /en('-------------------------------- treatequal_concl')), fail. traitequal(N,X,Y,I) :- \+ tempsdepasse_ltb(traitequal5), clause(rule(L,Nom),Q), \+ Nom = ! , \+ Nom = concl_only , \+ tempsdepasse_ltb(traitequal5a), rulactiv(N,LR),member(Nom,LR), concat_atom(['trop de regles a tester pour le remplacement de ', Y,' par ',X],Message), \+ tempsdepasse(N,Message), remplacer(Q, Y,X,Q1), \+ Q=Q1, sup_cond_triviales(Q1,Q2), Q3=Q2, create_name_rule(Nom,Nom1),R = (rule(L,Nom1):-Q3), ajoureglocale(N,R,Nom1), step(E), traces(N,action(fr(traitequal_regle)/en(treatequal_rule)), fr(rule(Nom))/en(rule(Nom)),create_rule(Nom1),E, [Y,fr('est remplace')/en('is replaced by'),X, fr('dans la regle')/en('in the rule'),Nom, fr('pour donner la regle')/en('to give the rule'),Nom1], [I] ), desactiver(N,Nom), acrire1(tr,fr('-------------------------------- traitequal_regle') /en('-------------------------------- treatequal_rule') ), fail. %%%%%%%%% nov 04 %%%%%%%%% %%% traitequal(N,X,Y,_) :- \+ tempsdepasse_ltb(traitequal6), retract(hyp(N,X=Y,_)), acrire1(tr,[fr('supprimer hypothese')/en('remove hypothesis'), X=Y]), retract(objet(N,Y)), acrire1(tr,[fr('supprimer objet')/en('remove object'),Y]). traitequal(_,_,_,_). 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 :- tempsdepasse_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)), A=..[P|_], ( B=..[P|_] -> true ; B=(~B2), B2=..[P|_]-> true ; true %message(z_elidondef_lesautresdefinitions,D) ), elifun(B,B1), assert(definition1(Nomfof,A<=>B1)), (ecrireconsreg-> ecrire1(definition(D)-definition1(A<=>B1));true), retract(definition(Nomfof,D)), fail. elifundef :- definition1(Nomfof,D), retract(definition1(Nomfof,D)),assert(definition(Nomfof,D)),fail. elifundef :- lemme(Nom,B),elifun(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. elifundef :- lemme1(Nom,B), retract(lemme1(Nom,B)),assert(lemme(Nom,B)), fail. elifundef :- definition(Nomfof,D),D=(!_:De), retract(definition(Nomfof,D)), assert(definition(Nomfof,De)), fail. elifundef . elifun(_,_) :- tempsdepasse_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 =seul(_,_) -> 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 = 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], elifun2(seul(FX1::Y,E1),E3), E4=seul(Arg::Z,E3),elifun2(E4,E5) ), !. elifun2(E,E). elifun1(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], elifun(E1,E2),elifun1(E2,E22),E3=seul(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), remplacer(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 ; remplacer(Args,Arg,Z,Args1), FY1 =.. [F|Args1], elifun3(FY1::Y,FY1Y), elifun2(seul(Arg::Z,FY1Y),E) ), !. elifun3(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)) ) , create_objet(N,z,X1), ajobjet(N,X1), remplacer(P,X,X1,P1), 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) :- addhyp(N, H,I1). eg(P,P1) :- ( P = P1 ; P1 = (F1::Y) , P = (F::Y), F1=..L,F = (..L), message([eg,oui,ce,cas,se,produit]),read(_) ) . deleteth :- effacer([subth(_,_), theoreme(_), chemin(_), hyp(_,_,_), hyp_traite(_,_), ou_applique(_), concl(_,_,_), lien(_,_), objet(_,_), fonction(_,_), rulactiv(_,_), tracedem(_,_,_,_,_,_,_), conjecture(_,_), fof(_,_,_), include(_), priorite(_,_), fichier(_), reglehypuniv(_,_,_), step(_), fof_traitee(_,_,_), res(_), seulile(_) ]), assert(conjecture(false, false)), assert(seulile(niouininon)), assign(probleme(pas_encore_de_probleme)), reset_gensym, told. deleteall :- effacer([ definition(_),definition(_Nomfof,_), lemme(_,_), priorite(_,_), concept(_), step(_), fof_traitee(_,_,_), seulile(_) ]), assert(seulile(niouininon)), effacer_regcons, 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_traite, concl, /*objet,concept,fonction,*/ reglactiv,conjecture, fof ]). liste([Item|Items]) :- listing(Item), liste(Items). liste([]). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% actions elementaires %% elementary actions %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% create_objet(N,X,XX) :- gensym(X,XX), ajobjet(N,XX). create_objects_and_replace(N,[X|XX],CX,C1,OO) :- create_objects_and_replace(N,[X|XX],CX,C1,[],OO). create_objects_and_replace(N,[X|XX],CX,C1,OO1,OO2) :- gensym(z, Z), ajobjet(N, Z), ligne(tr),tab(3), remplacer(CX,X,Z,CZ), create_objects_and_replace(N,XX, CZ,C1,[Z|OO1],OO2). create_objects_and_replace(_N,[],C,C,OO,OO). create_name_rule(R,RR) :- ( type(R,_) -> suc(R,R1),create_name_rule(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(_,_) :- tempsdepasse(_,ou_et). 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(_,_) :- tempsdepasse(_,assoc). 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,_), acrire1(tr,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, acrire1(tr,elt_ou_bis-'FX::Y'/(FX::Y)-'Y'/Y-'Z'/Z-'T'/T), !. elt_ou_bis(N, _ | B) :- elt_ou_bis(N, B), acrire1(tr,elt_ou_bis_), !. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% ecritures %% dispaly %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ecrire1(L):- ligne, ecrire(L). acrire_tirets(Option,E) :- (display(Option) -> ecrire_tirets(E);true). ecrire_tirets(E) :- ligne, ecrire([-------------------------------------------------------]), ecrire(E). acrire(Option,E) :- (display(Option) -> ecrire(E);true). acrire1(Option,E) :- (display(Option) -> ecrire1(E);true). ecrire(E) :- var(E) , write('_'). ecrire(fr(FR)/en(EN)):- ( lang(fr) -> ( lang(en) -> ecrire(FR/EN) ; ecrire(FR) ) ; lang(en) -> ecrire(EN) ), !. 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 :- nl. ligne(Option) :- (display(Option) -> nl;true). message(M) :- ( version(casc) -> true ; 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;acrire1(tr,[fr('car')/en('because'),Cond])), acrire1(tr,[cond:Antecedants, action:E]), acrire1(tr,'expl : '), acrire(tr,Expli), assert(tracedem(N,Nom,Cond,A,E,Expli,Antecedants)). ecrire1ettrace(A,B,C,D):- ecrire1(ecrire1ettrace-A-B-C-D). modifytimelimit(TL) :- assign(timelimit(TL)). tptp :- ( lang(fr) -> shell('cat tptp-commandes') ; lang(en) -> shell('cat tptp-commands') ; nl,write('definir un langage/define a language') ). m :- [muscadet-perso]. t1 :- abimpab. abimpab :- deleteall, tell(res_abimpab), demontrer(a & b => a & b). abimpac :- deleteall, demontrer(a & b => a & c). abimpcb :- deleteall, demontrer(a & b => c & b). aimpab :- deleteall, demontrer(a => a & b). pab :- deleteall, demontrer(p(a) & p(b) & q(b)=> ? [X]: (p(X) & q(X))). t2 :- aimpboua. aimpboua :- deleteall, tell(res_aimpboua), demontrer(a => b|a). t :- test. testtr :- tptp('SET002+4.p',tr). test :- tptp('SET002+4.p'). ttt :- tptp('SET027+4.p'). tt :- tptp('SET012+4.p'). ta :- tptp('ALG020+1.p'). tag :- tptp('AGT017+1.p'). tc :- testcasc. testcasc :- casc('/home/dominique/TPTP/TPTP-v4.0.1/Problems/SET/SET002+4.p'). testcascsyn :- casc('Problems/SYN/SYN075+1.p'). tcom :- tptp('COM018+1.p',tr+szs). tcs :- testcascsyn. p :- demontrer(p). petp :- demontrer(p & p). pimpp :- demontrer(p => p). agt :- tptp('AGT001+1.p'). 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'). csr(I,J,T) :- tptp('CSR',I,J,T). csr(I,J) :- tptp('CSR',I,J). geo(I) :- tptp('GEO',I,1). g :- grp(1,6). gra(I) :- tptp('GRA',I,1). grp(I,J) :- tptp('GRP',I,J). 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) :- modifytimelimit(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) :- deleteall,tptp('SYN',I,1). syn :- deleteall, syn(973). tptp([A|AA]) :- ( atom(A),exists_file(A) -> file_base_name(A,NomPb), assign(chemin(A)),assign(probleme(NomPb)), tptp(AA) ; atom(A),sub_atom(A,0,3,_,DOM), getenv('TPTP',TPTPdir), concat_atom([TPTPdir,'/Problems/',DOM,'/',A],CHEMIN), exists_file(CHEMIN) -> assign(chemin(CHEMIN)),assign(probleme(A)), tptp(AA) ; number(A) -> A2 is A*8,modifytimelimit(A2), tptp(AA) ; A=(+B) -> ( display(B) -> true ; assert(display(B))), tptp(AA) ; A=(-B) -> retractall(display(B)), tptp(AA) ; (A=fr|A=en) -> assign(lang(A)), tptp(AA) ; ecrire1([fr('donnee incorrecte')/en('data error'),A]),nl ),!. tptp([]) :- assign(version(tptp)), statistics(cputime,Tdebut), assign(temps_debut(Tdebut)), deleteall, (chemin(Ch) -> ( version(casc) -> RES=user, REG=res ; write('---------------------------------------------------'), ligne(tr), acrire1(tr,fr(chemin=Ch)/en(path=Ch)), probleme(NomPb), acrire1(tr,fr(probleme=NomPb)/en(problem=NomPb)), atom_concat(res_,NomPb,RES), (lang(en) -> atom_concat(rul_,NomPb,REG);atom_concat(reg_,NomPb,REG)) ), assign(res(RES)), assign(reg(REG)), lire(Ch), charger_axioms, \+ tempsdepasse(-1,apres_charger_axioms), travail1, \+ tempsdepasse(-1, 'apres travail1'), ( display(tr) -> tell(REG), listingg(regle), l(type),l(priorite),l(definition),l(lemme), told ; true ), conjecture(NomConj,TH), telll(RES), acrire1(tr,Ch), acrire1(tr,NomConj), demontr(TH), ( version(casc) -> true ; statistics(cputime,Tfintptp), assign(tempspasse(Tfintptp)) ), nl,toldd, ! ; ecrire1(fr('pas de fichier ni chemin ni probleme') /en('no file or path or problem')) ). tptp(A) :- atom(A), tptp([A]). tptp(A,B) :- tptp([A,B]). tptp(A,B,C) :- tptp([A,B,C]). tptp(A,B,C,D) :- tptp([A,B,C,D]). tptp(A,B,C,D,E) :- tptp([A,B,C,D,E]). tptp(A,B,C,D,E,F) :- tptp([A,B,C,D,E,F]). tptptest :- tptp([-name, 'SET002+4.p', -print, tr+pr+szs]). messagetemps(Tdem) :- concat_atom([' en ',Tdem,' secondes'],Textefr), concat_atom([' in ',Tdem,' seconds'],Texteen), (lang(en) -> write(user,Texteen);write(user,Textefr)), ecrire(fr(Textefr)/en(Texteen)), ecrire1(========================================), ecrire(========================================), message('---------------------------------------------------'). messagetemps(Option, Tdem) :- concat_atom([' en ',Tdem,' secondes'],Textefr), concat_atom([' in ',Tdem,' seconds'],Texteen), (lang(en) -> write(user,Texteen);write(user,Textefr)), acrire(Option,fr(Textefr)/en(Texteen)), acrire1(Option,========================================), acrire(Option,========================================), message('---------------------------------------------------'). trad(_,_) :- tempsdepasse(-1,trad). 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), \+ tempsdepasse(-1,lire_fof), (Nature = conjecture -> effacer([conjecture(_,_)]), assert(conjecture(Nomfof,Formule)) ;(Nature=axiom;Nature=hypothesis;Nature=lemma;Nature=definition ; Nature=assumption) -> (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<=>B),A=..[_,X|_],var(X) -> (A=..[P|_], B=(~B1), B1=..[P|_] -> assert(lemme(Nomfof,Formule)) ; 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 '/ Nature /' non connu dans la formule '/ FormuleTPTP) ), retract(fof(Nomfof,Nature,FormuleTPTP)), assert(fof_traitee(Nomfof,Nature,FormuleTPTP)), fail. lire(_). charger_axioms :- include(Axioms), \+ tempsdepasse(-1,charger_axioms), (getenv('TPTP',TPTPDirectory) -> atom_concat(TPTPDirectory,'/',Directory), atom_concat(Directory,Axioms,Axioms1), exists_file(Axioms1), lire(Axioms1), fail ; ecrire1(fr('variable d''environnement TPTP non definie') /en('envitonment variable TPTP not defined')) ). 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) :- assert(version(casc)), tptp([path,FICH,+pr,-tr,+szs]). casc_ltb(Pb,Res,T1) :- assert(resul(Res)), statistics(cputime,Tavantdeleteall), Tfinal is Tavantdeleteall + T1, assert(tempsfinal(Tfinal)), assert(version(casc)), assert(version(ltb)), nl,write(tempslimitepourladem=T1), assign(timelimit(T1)), file_base_name(Pb,Probleme), assign(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]), demontr(TH), statistics(cputime,Tapresdem), Tempstotaldem is Tapresdem-Tavantdeleteall, nl,write(tempstotaldem=Tempstotaldem),nl, tell(Res), (exists_file(Res)-> true;write('pas de fichier'-Res)), write(Tempstotaldem), nl, (concl(0, true,_) -> (conjecture(false,_) -> write('SZS status Unsatisfiable for ') ; write('SZS status Theorem for ') ) ; write('SZS status GaveUp for ') ), write(Probleme), nl, told . %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% appel th (donnees et theoremes) %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% th :- ( lang(fr) -> shell('cat th-commandes') ; lang(en) -> shell('cat th-commands') ; nl,write('definir un langage/define a language') ). th([A|AA]) :- ( atom(A), exists_file(A) -> assign(chemin(A)),th(AA) ; number(A) -> modifytimelimit(A), th(AA) ; A=(+B) -> ( display(B) -> true ; assert(display(B))), th(AA) ; A=(-B) -> retractall(display(B)), th(AA) ; (A=fr|A=en) -> assign(lang(A)), th(AA) ; ecrire1([fr('donnee incorrecte')/en('data error'),A, fr('(ni atome, ni option)')/en('(neither atom, neither option)')]), nl ),!. th([]) :- assign(version(th)), chemin(Ch), [Ch], file_base_name(Ch,FichCh),atom_concat(reg_,FichCh,REG), forall( include(Donnees),[Donnees]), ( (theoreme(_,_);theorem(_,_)) -> travail1th, ( display(tr) -> tell(REG), listingg(regle),told;true), forall( (theoreme(Nom,T);theorem(Nom,T)), ( deleteth, assign(probleme(Nom)),assert(theoreme(T)), probleme(P),message(['theoreme a demontrer (',P,')','\n',T]), atom_concat(res_,Nom,RES), assign(res(RES)), telll(RES), demontrerth(T), told ) ), nl ; ecrire1('pas de theoremes, on lit juste des definitions') ) . th(A) :- th([A]). th(A,B) :- th([A,B]). th(A,B,C) :- th([A,B,C]). th(A,B,C,D) :- th([A,B,C,D]). th(A,B,C,D,E) :- th([A,B,C,D,E]). th(A,B,C,D,E,F) :- th([A,B,C,D,E,F]). th2 :- th(exemple2). th21 :- th(exemple21). th22 :- th(exemple22). thex :- th(exemple_th,res(zzres)). thexres :- th(exemple_th,res(zres)). tth0 :- tell(faits0),listing,told. tth1 :- tell(faits1),listing,told. tth2 :- tell(faits2),listing,told. tth3 :- tell(faits3),listing,told. tth :- tell(faits0),listing,told, thexres, tell(faits1),listing,told, deleteth, tell(faits2),listing,told, deleteall, tell(faits3),listing,told. travail1th :- forall((definition(Y=A), \+ var(A), functor(Y,P,_), A=[X,PX], +++(APP), XappY =.. [APP,X,Y]), assert(definition(P, XappY <=> PX))), forall((definition(A<=>B), functor(A,P,_)), assert(definition(P,A<=>B))), forall((definition(!_:(A<=>B)), functor(A,P,_)), assert(definition(P,A<=>B))), elifundef, consreg. demontrerth(Th) :- res(RES), telll(RES), demontr(Th) . demontrer(Th) :- travail1th, assign(theoreme(Th)), assign(theoreme('',Th)),assign(res(user)), assign(probleme(probleme)), demontrerth(Th). demontrer1(Th) :- \+ theoreme(Th), assign(theoreme(Th)), assign(res(user)), demontrerth(Th). def(Def) :- assert(definition(Def)). test_def_part :- assert(definition(parties(E)=[X,inc(X,E)])). tdp :- test_def_part. %%%%%%%%%%%%%%%%%%%%%%%%%%% %% regles %% %%%%%%%%%%%%%%%%%%%%%%%%%%% regles_et([concl_and]). regles_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,hyp_notnot,hypnotimp,hypimp, concl_not_ou, concl_or_not, hypequ, hypnotequ, concl_or_and, =>,<=>, concl_only,..,..1, concl_exi1, concl_exi2, concl_exi3,concl_exi4, concl_exi5, concl_exi1a,concl_exi1b, concl_exi_seul, concl_and_trivial_1,concl_and_trivial_2, concl_stop_trivial,concl_stop_trivial_or, concl2pts ] ) . regles_defconcl1([def_concl_pred,defconcl1a,defconcl1b,defconcl1bb]). regles_defconcl2([defconcl2,defconcl2app,defconcl_rel, defconcl2a,defconcl2b,defconcl3]). regles_exist([hyp_exi]). regles_ou([hyp_or_cte, hyp_or]). regles_concl_exist([concl_exi,concl_exi_et_non,create_an_image_object]). rule(N, elifun) :- concl(N, C, I), elifun( C, C1), newconcl(N, C1,I1),!, traces(N,elifun, concl(N, C, I), newconcl(N, C1, I1), I1, [fr('elimination des symboles fonctionnels dans la conclusion') /en('elimination of the functional symbols of the conclusion'), fr('\npar exemple, p(f(X)) est remplace par seul(f(X)::Y, p(Y))') /en('\nfor example, p(f(X)) is replaced by only(f(X)::Y, p(Y))')], [I]). rule(N,stop_hyp_concl ):- concl(N,C,Step1), ground(C), hyp(N,C,Step2/**/), newconcl(N,true,NewStep), traces(N, rule(stop_hyp_concl), (hyp(N,C,Step2),concl(N,C,Step1)), newconcl(N,true,NewStep), (NewStep), fr(['la conclusion',C,'a demontrer est une hypothese']) /en(['the conclusion',C,'to be proved is a hypothesis']), ([Step1,Step2]) ). rule(N,stop1a):- concl(N,C,IC), ( C=(?_:_);C=(!_:_);C=(_ | _);C=(_<=>_) ;C=seul(_::_,_) ), 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, fr(['la conclusion',C,'a demontrer est une hypothese']) /en(['the conclusion',C,'to be proved is a hypothesis']), [IC,I] ). 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, fr('on a trouve une contradiction') /en('a contradiction has been found'), [I]). rule(N,concl_or_stop3) :- concl(N,A | B,I), hyp(N,H,II),elt_ou(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, fr('un des elements de la conclusion disjonctive est une hypothese') /en('one element of the disjunctive conclusion of theorem'), [I,II] ). rule(N,concl_or_stop3bis) :- concl(N,A | B,I), elt_ou_bis(N,A | B), newconcl(N,true,I1), 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, fr('on a une contradiction') /en('there is a contradiction'), [I,II] ). rule(N, equal) :- hyp(N, X=Y,I), A=X, B=Y, acrire1(tr,fr([remplacer,B,par,A,'propager et supprimer',B]) /en([replace,B,by,A,'propagate and remove',B])), \+ tempsdepasse(N,regle_equal_avant_traitequal), traitequal(N,A,B,I), \+ tempsdepasse(N,regle_equal_apres_traitequal) . rule(N, equaldef) :- hyp(N,E::X,I), atom(X), hyp(N,E::Y,J), atom(Y), \+ X == Y, addhyp(N, X = Y, I1), traces(N,rule(egadef), (hyp(N,E::X,I), hyp(N,E::Y,J), J), addhyp(N, X=Y, I1),I1, fr([X,et,Y,'ont la meme definition']) /en([X,and,Y,'have the same definition']), [I,J] ). rule(N, hyp_or1) :- hyp(N,A | A,I), \+ hyp_traite(N, A | A), addhyp(N,A,E),assert(hyp_traite(N, A | A)), traces(N,rule(hyp_or1),hyp(N,A | A,I), addhyp(N,A,E),E, 'E|E = E',[I]). rule(N, hyp_or23) :- hyp(N,A | B,_), \+ hyp_traite(N, A | B), elt_ou(X=X, A | B), assert(hyp_traite(N, A | B)) . rule(N, hyp_or4) :- hyp(N,A | B,_), \+ hyp_traite(N, A | B),hyp(N,A,_), assert(hyp_traite(N, A | B)). rule(N, hyp_or5) :- hyp(N,A | B,_), \+ hyp_traite(N, A | B),hyp(N,B,_), assert(hyp_traite(N, A | B)). rule(N, concl_not) :- concl(N,~ A,I), addhyp(N,A,I1), newconcl(N,false,I1), traces(N,rule(concl_not), concl(N,~ A,I), (addhyp(N,A,I1), newconcl(N,false,I1)),I1, fr(['on suppose',A,'et on cherche une contradiction']) /en(['assume',A,'and search for a contradiction']), [I] ). rule(N, hyp_notnot) :- hyp(N,~ ~ A,I), addhyp(N, A, J), traces(N, rule(hyp_notnot), hyp(N,~ ~ A,I), addhyp(N, A, J),J, fr('\n*** car ~ ~ a = a') /en('\n*** because ~ ~ a = a'), [I,J] ). rule(N, hypnotimp) :- hyp(N,~(A=>B),I),\+ hyp(N,A ,_), addhyp(N,(A & ~ B),J), traces(N,rule(hypnotimp), hyp(N,~(A=>B),I), addhyp(N,(A & ~ B),J), J, fr('\n*** car ~(a=>b) = (a&~b)') /en('\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, fr(['on suppose',A,'et on cherche une contradiction']) /en(['assume',A,'and search for a contradiction']), [I,IC] ). rule(N, concl_not_ou) :- concl(N,~ A | B,I),addhyp(N,A,I1),newconcl(N,B,I1), traces(N,rule(concl_not_ou), concl(N,~ A | B,I),(addhyp(N,A,I1), newconcl(N,B,I1)),I1, fr(['on suppose',A,'et on doit montrer',B]) /en(['assume',A,'and prove',B]), [I] ). rule(N, concl_or_not) :- concl(N,A | B,I), ou_non(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, fr(['on suppose',Amoins, 'on retire',~ Amoins,'de la conclusion']) /en(['assume',Amoins, 'remove',~ Amoins,'from the conclusion']), [I] ). rule(N,concl_or_and) :- concl(N,A | B,I),ou_et(A | B,C),newconcl(N,C,I1), traces(N,rule(concl_or_and), concl(N,A | B,I),newconcl(N,C,I1),I1, fr('distributivite de | par rapport a &') /en('distributivity of | upon &'), [I] ). rule(N, =>) :- concl(N, A => B, Step), addhyp(N, A, NewStep), newconcl(N,B,NewStep), traces(N, rule(=>), (concl(N, A => B, Step)), [addhyp(N, A, NewStep), newconcl(N,B,NewStep)], (NewStep), fr('pour demontrer H=>C, on suppose H et on doit demontrer C') /en('to prove H=>C, assume H and prove C'), ([Step]) ). 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, fr('on remplace A<=>B par (A=>B)&(B=>A)') /en('A<=>B is replaced by (A=>B)&(B=>A)'), [E1]). rule(N, !) :- concl(N,(! XX : C), Step), step_action(NewStep), create_objects_and_replace(N,XX,C,C1,Objets), newconcl(N, C1,NewStep), traces(N, rule(!), concl((0,! XX : C), Step), [create_objets(Objets), newconcl(N, C1,NewStep)], (NewStep), fr('on instancie la(les) variable(s) universelle(s) de la conclusion')/ en('the universal variable(s) of the conclusion is(are) instantiated'), [Step] ). rule(N, concl_only) :- concl(N,seul(A::X,B),I), ( hyp(N,A::X1,II) -> acrire1(tr,fr([remplacer,X,par,X1])/en([replace,X,by,X1])), traces(N,rule(concl_only), (concl(N,seul(A::X,B),I), hyp(N,A::X1,II)), newconcl(N,B1,I1), I1, fr([X,'est remplace par',X1,dans,B]) /en([X,'is replaced by',X1,in,B]), [I,II]) ; var(X) -> create_objet(N,z,X1), ajobjet(N, X1),addhyp(N,A::X1,I1), traces(N,rule(concl_only), concl(N,seul(A::X,B),I), (addhyp(N,A::X1,I1),newconcl(N,B1,I1)), I1, fr(['creation de l\'objet',X1,'et de sa definition']) /en(['creation of object',X1,'and of its definition']), [I]) ; acrire1(tr,[regle,seul,cas, non,prevu]) ), remplacer(B,X,X1,B1), newconcl(N,B1,I1) . 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, fr('\n*** car ..[r,a,b] = r(a,b)') /en('\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, fr('\*** car ..[f,x] = f(x)') /en('\*** 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, fr('raisonnement par l\'absurde') /en('proof by contradiction'), [E] ). rule(N, concl_exi1) :- concl(N,(?[X]:C),I), (atom(X);var(X)),hyp(N,C,II), ground(C), newconcl(N, true, I1), remplacer((?[X]: C),X,_XX,CC), traces(N,rule(concl_exi1), (concl(N, CC,I), hyp(N,C,II)), newconcl(N, true, I1),I1, ['l\'objet',X,'verifie la conclusion'], [I,II] ). rule(N, concl_exi2) :- 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), remplacer((?[X]:(B & C)),X,_XX,CC), traces(N, rule(concl_exi2), ( concl(N, CC,I),hyp(N,B,II), hyp(N,C,III)), newconcl(N,true,I1), I1, fr(['l\'objet',X,'verifie la conclusion']) /en(['the object',X,'satisfies the conclusion']), [I,II,III] ). rule(N, concl_exi3) :- 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), remplacer((?[X]: B | C),X,_XX,CC), traces(N,rule(concl_exi3), (concl(N,CC,I),hyp(N,BouC,II)), newconcl(N,true,I1), I1, fr(['on a un element qui verifie la conclusion']) /en(['there is an element which satisfies the conclusion']), [I,II] ). rule(N, concl_exi4) :- 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), remplacer((?[X]: B => C),X,_XX,CC), traces(N, rule(concl_exi4), (concl(N, CC,I),hyp(N,NBouC,II)), newconcl(N, true, I1),I1, fr(['on a un element qui verifie la conclusion']) /en(['there is an element which satisfies the conclusion']), [I,II] ). rule(N, concl_exi5) :- concl(N, (?XX: (~ C)),I), newconcl(N,false,I1),addhyp(N, (!XX:C),I1), traces(N,rule(concl_exi5), concl(N, (?XX:( ~ C)),I), (newconcl(N,false,I1),addhyp(N,(!XX:C),I1)), I1, fr(['pour demontrer ?[..]: ~A,', 'on suppose A et on cherche une contradiction']) /en(['to prove ?[..]: ~A,', 'assume A and search for a contradiction']), [I] ). rule(N,concl_exi) :- concl(N, ? XX:C, Eexi), proconclexi(N,? XX:C, Eexi,_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, fr('creer un objet image')/en('create an image object'), [] ). rule(N,concl_and_trivial_1):- concl(N, A & B, I), hyp(N, A, II), acrire1(tr,[A, fr(est)/en(is), true]),newconcl(N, B, I1), traces(N,rule(concl_and_trivial_1), (concl(N, A & B, I),hyp(N, A, II)), newconcl(N, B, I1),I1, fr('un des elements de la conclusion conjonctive est une hypothese') /en('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), acrire1(tr,[B, fr(est)/en(is), true]),newconcl(N, A, I1), traces(N,rule(concl_and_trivial_2), (concl(N, A & B,I), hyp(N, B, II)), newconcl(N, A, I1), I1, fr('un des elements de la conclusion conjonctive est une hypothese') /en('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), traces(N,rule(concl_stop_trivial), concl(N, A = A, I), newconcl(N,true, I1),I1, fr('conclusion triviale') /en('trivial conclusion'), [I] ). rule(N, concl_stop_trivial_or) :- concl(N, A | B, I), elt_ou(X=X,A | B), newconcl(N,true, I1), traces(N,rule(concl_stop_trivial_or), concl(N, A | B, I), newconcl(N,true, I1),I1, fr('un des elements de la conclusion disjonctive est triviale') /en('one of the elements of the disjunctive conclusion is trivial'), [I] ). rule(N, concl_and) :- concl(N, A & B, E ), proconj(N, A & B, E, Efin), (concl(N, true, Efin) -> 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'] ) . rule(N, concl_or) :- concl(N, A | B, Eavant ), demdij(N, A | B, Eavant, _Eapres), (concl(N, true, EE),message(etapefinale-EE) -> Expli=[fr('un des elements de la conclusion disjonctive du theoreme') /en('one element of the disjunctive conclusion of theorem'), N, fr('a ete demontre')/ent('has been proved') ] ; Expli=['aucun element de la conclusion disjonctive du theoreme',N, 'n\'a ete demontre'] ) . rule(N, def_concl_pred) :- concl(N, C, Step), definition(Nomfof,C <=> D), acrire1(tr,[N, fr('definition_de_la_conclusion') /en('definition_of_the_conclusion')]), newconcl(N, D, NewStep), traces(N, rule(def_concl_pred), concl(N, C, Step), newconcl(N, D, NewStep), NewStep, fr(['on remplace la conclusion ',C,' par sa definition(fof',Nomfof,')']) /en(['the conclusion ',C,'is replaced by its definition(fof',Nomfof,')']), [Step] ). rule(N, defconcl1a) :- concl(N, C | A, I), definition(Nomfof,C <=> D), acrire1(tr,[N, fr('definition de la conclusion') /en('definition of the conclusion')]), newconcl(N, D | A, I1), 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), acrire1(tr,[N, fr('definition de la conclusion') /en('definition of the conclusion')]), newconcl(N, A | D, I1), traces(N,rule(defconcl1b), concl(N, A | C, I), newconcl(N, A | D, I1),I1, [definition,Nomfof], [I]). rule(N, defconcl1bb) :- concl(N, A | seul(Y::X,seul(Z::T,C)), I), definition(Nomfof,C <=> ~ D), acrire1(tr,[N, fr('definition de la conclusion') /en('definition of the conclusion')]), newconcl(N, A | ~ seul(Y::X,seul(Z::T,D)), I1), traces(N,rule(defconcl1bb), concl(N, A | seul(Y::X,seul(Z::T,C)), I), newconcl(N, A | ~ seul(Y::X,seul(Z::T,D)), I1),I1, [definition,Nomfof], [I] ). rule(N, concl2pts) :- concl(N, FX::Y, I), newconcl(N, seul(FX::Z, Z=Y), I1), traces(N,rule(concl2pts), concl(N, FX::Y, I), newconcl(N, seul(FX::Z, Z=Y), I1),I1, fr(' FX::Y est reecrit seul only(FX::Z, Z=Y)') /en(' FX::Y is rewriten only(FX::Z, Z=Y)'), [I] ) . rule(N, defconcl_rel) :- 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), acrire1(tr,[N, fr('definition de la conclusion') /en('definition of the conclusion')]), newconcl(N, P1, I1), traces(N,rule(defconcl_rel), (concl(N, C, I), hyp(N, D::B, II)), newconcl(N, P1, I1),I1, [definition,Nomfof], [I,II] ) . rule(N, hyp_exi) :- hyp(N, (?XX:P),I), \+ hyp_traite(N, (?XX:P)), ( 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, assign(step(I1)), create_objects_and_replace(N,XX,P,P1,Objets), addhyp(N,P1,I1), ajhyp_traite(N,(?XX:P)), incrementer_nbhypexi(NBhypexi), traces(N,rule(hyp_exi), hyp(N,(?XX:P),I), [create_objets(Objets), addhyp(N,P1,I1)], I1, fr('traitement de l\'hypothese existentielle nbhypexi'=NBhypexi) /en('treatment of the existential hypothesis'), [I] ), ( NBhypexi > 300 -> acrire1(tr,fr(['on a traite',NBhypexi,'hypotheses existentielles']) /en([NBhypexi,'have been treated'])), acrire1(tr,fr('on desactive la regle hyp_exi') /en('rule hyp_exi is desactivated')), desactiver(N,hyp_exi) ;true ) . rule(N, hyp_or) :- hyp(N, (A | B),I), \+ hyp_traite(N, (A | B)), \+ (ou_applique(N)), concl(N, C, II), acrire1(tr,fr([N,'traitement de l''hypothese disjonctive',(A | B)]) /en([N,'treatment of the disjunctive hypothesis',(A | B)])), hypou(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, [fr('on doit montrer la conclusion dans les deux cas') /en('the conclusion must be proved in both cases')], [I,II] ), ajhyp_traite(N, (A | B)), assert(ou_applique(N)) . rule(N, hyp_or_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), acrire1(tr,fr([N,'traitement de l''hypothese disjonctive',(A | B)]) /en(['treatment of the disjunctive hypothesis',(A | B)])), hypou(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, [fr('on doit montrer la conclusion dans les deux cas') /en('the conclusion must be proved in both cases')], [I,II] ) , ajhyp_traite(N, A | B), assert(ou_applique(N)) . orphelin(L) :- tracedem(_,_,_,_,_,_,L),var(L),!. orphelin(E) :- tracedem(_,_,_,_,_,_,L),member(E,L), (var(E)-> acrire(tr,'il reste une variable dans tracedem'-L) ; E =\= 1), \+ tracedem(_,_,_,_,E,_,[_|_]). tracedemutile :- ( 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) -> length(VT, LongueurVT), ( LongueurVT>1000 -> acrire1(tr,fr(['trace trop longue (',LongueurVT,'etapes utiles)']) /en(['trace too long (',LongueurVT,'useful steps)'])) ; (version(casc)-> true ;acrire1(tr,'orphelins : '), forall(orphelin(Orph),acrire(tr,['',Orph])), acrire1(pr,['\n*************************************\n*', fr('etapes utiles de la demonstration') /en(' useful steps of the proof '), '*\n*************************************\n' ]) ), acrire1(pr,'\n* * * * * * * * * * * * * * * * * * * * * * * *'), ( lang(en) -> acrire1(pr,'in the following, N is the number of a (sub)theorem'), acrire1(pr,' E is the current step'), acrire1(pr,' or the step when a hypothesis or conclusion has been added or modified'), acrire1(pr, 'hyp(N,H,E) means that H is an hypothesis of (sub)theorem N'), acrire1(pr, 'concl(N,C,E) means that C is the conclusion of (sub)theorem N'), acrire1(pr, 'obj_ct(N,C) means that C is a created object or a given constant'), acrire1(pr,'addhyp(N,H,E) means add H as a new hypothesis for N'), acrire1(pr,'newconcl(N,C,E) means that the new conclusion of N is C'), acrire1(pr,' (C replaces the precedent conclusion)'), acrire1(pr, 'a subtheorem N-i or N+i is a subtheorem of the (sub)theorem N'), acrire1(pr,' N is proved if all N-i have been proved (&-node)'), acrire1(pr,' or if one N+i have been proved (|-node)'), acrire1(pr,'the initial theorem is numbered 0') ; lang(fr) -> acrire1(pr, 'dans ce qui suit, N est le numero d''un (sous-)theoreme'), acrire1(pr,' E est l''etape courante'), acrire1(pr,' ou l''etape ou une hypothese ou conclusion a ete ajoutee ou modifiee'), acrire1(pr, 'hyp(N,H,E) signifie que H est une hypothese du (sous-)theoreme N'), acrire1(pr, ['concl(N,C,E) signifie que', 'C est la conclusion du (sous-)theoreme N']), acrire1(pr,['obj_ct(N,C) signifie que', 'C est un objet cree ou une constante donnee']), acrire1(pr,['addhyp(N,H,E) signifie', 'ajouter H comme nouvelle hypothese pour N']), acrire1(pr, 'newconcl(N,C,E) signifie que la nouvelle conclusion de N est C'), acrire1(pr,' (C remplace la conclusion precedente)'), acrire1(pr,['un sous-theoreme N-i ou N+i est', 'un sous-theoreme du (sous-)theoreme N']), acrire1(pr, ' N est demontre si tous les N-i ont ete demontres (noeud-&)'), acrire1(pr,' ou si un N+i a ete demontre (noeud-|)'), acrire1(pr,'le theoreme initial a pour numero 0') ; true ), ligne(pr), acrire1(pr,fr('* * * theoreme a demontrer') /en('* * * theorem to be proved')), ( version(tptp),conjecture(_,TH) -> acrire1(pr,TH) ; theoreme(TAD), acrire1(pr,TAD) ), acrire1(pr,fr('\n* * * demonstration :')/en('\n* * * proof :')), acrire1(pr,fr('\n* * * * * * theoreme 0 * * * * * *') /en('\n* * * * * * theoreme 0 * * * * * *')), tracedemutile(VT), acrire1(pr,fr('le theoreme initial 0 est donc demontre') /en('then the initial theorem is proved')), ( version(tptp),conjecture(false,_) -> acrire(pr,fr(' (pas de conjecture)')/en(' (no conjecture)')) ; true ), acrire1(pr,'* * * * * * * * * * * * * * * * * * * * * * * *\n') ) ; acrire1(tr,[fr('on ne peut pas atteindre la racine de la trace,') /en('the root of the trace is not reachable'), fr('il doit manquer une etape dans tracedem')/en('')]), acrire1(tr,fr('mais le theoreme initial 0 est bien demontre\n') /en('but the initial theorem is proved')) ) ; acrire1(tr,fr('theoreme initial non demontre') /en('initial theorem not proved')) ). tracedemutile([U|LU]) :- tracedem(_N,Nom,Cond,Act,(U),Expli,_Antecedants), ecriretrace(Act), ( Cond=[] -> true ; acrire1(pr,[fr('*** car')/en('*** because'),Cond]) ), acrire1(pr,['***',fr('explication :')/en('explanation :')]), acrire(pr,Expli), ( Nom=rule(R) -> Nom_a_ecrire=[fr(regle)/en(rule),R] ; Nom=action(A) -> Nom_a_ecrire=[action,A] ; Nom_a_ecrire=Nom ), acrire_tirets(pr,Nom_a_ecrire), tracedemutile(LU). tracedemutile([]). ecriretrace([Act|AA]) :- ecriretrace(Act), ecriretrace(AA),!. ecriretrace([]). ecriretrace(addhyp(N,A & B,E)) :- ecriretrace(addhyp(N,A,E)), tab(1), ecriretrace(addhyp(N,B,E)),!. ecriretrace(addhyp(N,..R,E)) :- H=..R, %acrire1(pr,addhyp(N,H,E)). ecriretrace(addhyp(N,H,E)). ecriretrace(addhyp(N,seul(FX::Y,A),E)) :- hyp(N,FX::Obj,Eobj), remplacer(A,Y,Obj,A1), (E=Eobj -> acrire1(pr,[fr('*** creer objet')/en('create object'),Obj]), ecriretrace(addhyp(N,FX::Obj,E)),nl,tab(5) ; true), ecriretrace(addhyp(N,A1,E)),!. ecriretrace(addhyp(N,~seul(FX::Y,A),E)) :- hyp(N,FX::Obj,Eobj), remplacer(A,Y,Obj,A1), (E=Eobj -> acrire1(pr,[fr('*** creer objet')/en('create object'),Obj]), ecriretrace(addhyp(N,FX::Obj,E)),nl,tab(5) ; true), ecriretrace(addhyp(N,~A1,E)),!. ecriretrace(newconcl(N,..R,E)) :- C=..R, ecriretrace(newconcl(N,C,E)). ecriretrace(creersubth(N,N1,_A,_E)) :- acrire1(pr,[fr('\n* * * * * * creation * * * * * * sous-theoreme') /en('\n* * * * * * creation * * * * * * sub-theoreme'), N1,'* * * * *' ]), acrire1(pr,[fr('toutes les hypotheses du (sous-)theoreme') /en('all the hypotheses of (sub)theorem'), N, fr('sont hypotheses du sous-theoreme') /en('are hypotheses of subtheorem'), N1]). ecriretrace(create_objets(OO)) :- acrire1(pr,[fr('creer objet(s)')/en('create object(s)'),OO]). ecriretrace(E) :- acrire1(pr,['***',E]). ecrire_simpl_R(Option,(rule(_,Nom):- Q)) :- seq_der(Q,_Qmoinstraces,Traces), Traces=traces(_,_,Cond,Act,_,_R,_Ex), ( lang(fr) -> acrire1(Option,['+++',regle,Nom,:,(si Cond alors Act)]) ; lang(en) -> acrire1(Option,['+++',rule,Nom,:,(if Cond then Act)]) ; acrire1(Option,'+++') ). zut(I,N) :- I