th4 appartenir au meme element d'une partition est une relation d'equivalence -qqs(A, qqs(B, partition(A, B)=>qqs(C, qqs(D app B, qqs(E app B, ..[C, D, E]<=>ilexiste(F app A, D app F et E app F)))=>equiv(B, C)))). ******************************************************************************** theoreme a demontrer -qqs(A, qqs(B, partition(A, B)=>qqs(C, qqs(D app B, qqs(E app B, ..[C, D, E]<=>ilexiste(F app A, D app F et E app F)))=>equiv(B, C)))). 0 nouvelle conclusion -qqs(A, qqs(B, partition(A, B)=>qqs(C, qqs(D app B, qqs(E app B, ..[C, D, E]<=>ilexiste(F app A, D app F et E app F)))=>equiv(B, C)))). 0 ajouter lien equiv 0 ajouter lien partition 0 ajouter lien inc regles actives:elifon stop1 stop2 stop3 stop4 egal egaldef ou1 ou23 ou4 ou5 non hypnon hypnonnon hypnonimp hypimp non_ou_1 non_ou_2 hypequ hypnonequ concl_ou_et => <=> qqs1 qqs2 seul .. ..1 ilec1 ilec2 ilec3 ilec4 ilec5 ilec1a ilec1b et_trivial_1 et_trivial_2 stop_trivial stop_trivial_ou conclet equiv equiv1 equiv2 partition partition1 partition2 inc et defconcl1 defconcl1a defconcl1b defconcl1bb ilexiste ou defconcl2 defconcl2app defconcl2elt defconcl2a defconcl2b defconcl3 0 ajouter objet x 0 nouvelle conclusion -qqs(A, partition(x, A)=>qqs(B, qqs(C app A, qqs(D app A, ..[B, C, D]<=>ilexiste(E app x, C app E et D app E)))=>equiv(A, B))). --------------------------------------------------------- regle qqs1 0 ajouter objet x1 0 nouvelle conclusion - (partition(x, x1)=>qqs(A, qqs(B app x1, qqs(C app x1, ..[A, B, C]<=>ilexiste(D app x, B app D et C app D)))=>equiv(x1, A))). --------------------------------------------------------- regle qqs1 0 ajouter hypothese partition(x, x1) 0 nouvelle conclusion -qqs(A, qqs(B app x1, qqs(C app x1, ..[A, B, C]<=>ilexiste(D app x, B app D et C app D)))=>equiv(x1, A)). --------------------------------------------------------- regle => 0 ajouter objet x2 0 nouvelle conclusion - (qqs(A app x1, qqs(B app x1, ..[x2, A, B]<=>ilexiste(C app x, A app C et B app C)))=>equiv(x1, x2)). --------------------------------------------------------- regle qqs1 0 ajouter la regle active locale - (regle(A, reghyp):-hyp(A, B app x1), hyp(A, C app x1), D=..[x2, B, C], hyp(A, D), \+hyp(A, ilexiste(E app x, B app E et C app E)), ajhyp(A, ilexiste(E app x, B app E et C app E))). a la fin des regles universelles 0 ajouter la regle active locale - (regle(A, reghyp1):-hyp(A, B app x1), hyp(A, C app x1), hyp(A, D app x), hyp(A, B app D), hyp(A, C app D), E=..[x2, B, C], \+hyp(A, E), ajhyp(A, E)). a la fin des regles universelles 0 nouvelle conclusion equiv(x1, x2) --------------------------------------------------------- regle => 0 definition de la conclusion 0 nouvelle conclusion -qqs(A app x1, ..[x2, A, A])et qqs(A app x1, qqs(B app x1, ..[x2, A, B]=> ..[x2, B, A]))et qqs(A app x1, qqs(B app x1, qqs(C app x1, ..[x2, A, B]et..[x2, B, C]=> ..[x2, A, C]))). --------------------------------------------------------- regle defconcl1 ************************************************ sous-theoreme 1 ***** 1 nouvelle conclusion -qqs(A app x1, ..[x2, A, A]). ----------------------------------------------- creation du sous-theoreme 1 1 ajouter objet x3 1 ajouter hypothese x3 app x1 1 nouvelle conclusion ..[x2, x3, x3] --------------------------------------------------------- regle qqs2 1 nouvelle conclusion x2(x3, x3) --------------------------------------------------------- regle .. 1 ajouter hypothese -ilexiste(A app x, x3 app A). --------------------------------------------------------- regle partition1 1 ajouter objet x4 1 ajouter hypothese x4 app x 1 ajouter hypothese x3 app x4 1 ajouter hypothese-traitee -ilexiste(A app x, x3 app A). --------------------------------------------------------- regle ilexiste 1 ajouter hypothese x2(x3, x3) --------------------------------------------------------- regle reghyp1 1 nouvelle conclusion vrai --------------------------------------------------------- regle stop1 theoreme 1 demontre 0 nouvelle conclusion -qqs(A app x1, qqs(B app x1, ..[x2, A, B]=> ..[x2, B, A]))et qqs(A app x1, qqs(B app x1, qqs(C app x1, ..[x2, A, B]et..[x2, B, C]=> ..[x2, A, C]))). ************************************************ sous-theoreme 2 ***** 2 nouvelle conclusion -qqs(A app x1, qqs(B app x1, ..[x2, A, B]=> ..[x2, B, A])). ----------------------------------------------- creation du sous-theoreme 2 2 ajouter objet x5 2 ajouter hypothese x5 app x1 2 nouvelle conclusion -qqs(A app x1, ..[x2, x5, A]=> ..[x2, A, x5]). --------------------------------------------------------- regle qqs2 2 ajouter objet x6 2 ajouter hypothese x6 app x1 2 nouvelle conclusion ..[x2, x5, x6]=> ..[x2, x6, x5] --------------------------------------------------------- regle qqs2 2 ajouter hypothese x2(x5, x6) 2 nouvelle conclusion ..[x2, x6, x5] --------------------------------------------------------- regle => 2 nouvelle conclusion x2(x6, x5) --------------------------------------------------------- regle .. 2 ajouter hypothese -ilexiste(A app x, x5 app A et x6 app A). --------------------------------------------------------- regle reghyp 2 ajouter hypothese -ilexiste(A app x, x5 app A). --------------------------------------------------------- regle partition1 2 ajouter hypothese -ilexiste(A app x, x6 app A). --------------------------------------------------------- regle partition1 2 ajouter objet x7 2 ajouter hypothese x7 app x 2 ajouter hypothese x5 app x7 2 ajouter hypothese x6 app x7 2 ajouter hypothese-traitee -ilexiste(A app x, x5 app A et x6 app A). --------------------------------------------------------- regle ilexiste 2 ajouter hypothese x2(x5, x5) --------------------------------------------------------- regle reghyp1 2 ajouter hypothese x2(x6, x5) --------------------------------------------------------- regle reghyp1 2 nouvelle conclusion vrai --------------------------------------------------------- regle stop1 theoreme 2 demontre 0 nouvelle conclusion -qqs(A app x1, qqs(B app x1, qqs(C app x1, ..[x2, A, B]et..[x2, B, C]=> ..[x2, A, C]))). ************************************************ sous-theoreme 3 ***** 3 nouvelle conclusion -qqs(A app x1, qqs(B app x1, qqs(C app x1, ..[x2, A, B]et..[x2, B, C]=> ..[x2, A, C]))). ----------------------------------------------- creation du sous-theoreme 3 3 ajouter objet x8 3 ajouter hypothese x8 app x1 3 nouvelle conclusion -qqs(A app x1, qqs(B app x1, ..[x2, x8, A]et..[x2, A, B]=> ..[x2, x8, B])). --------------------------------------------------------- regle qqs2 3 ajouter objet x9 3 ajouter hypothese x9 app x1 3 nouvelle conclusion -qqs(A app x1, ..[x2, x8, x9]et..[x2, x9, A]=> ..[x2, x8, A]). --------------------------------------------------------- regle qqs2 3 ajouter objet x10 3 ajouter hypothese x10 app x1 3 nouvelle conclusion ..[x2, x8, x9]et..[x2, x9, x10]=> ..[x2, x8, x10] --------------------------------------------------------- regle qqs2 3 ajouter hypothese x2(x8, x9) 3 ajouter hypothese x2(x9, x10) 3 nouvelle conclusion ..[x2, x8, x10] --------------------------------------------------------- regle => 3 nouvelle conclusion x2(x8, x10) --------------------------------------------------------- regle .. 3 ajouter hypothese -ilexiste(A app x, x8 app A et x9 app A). --------------------------------------------------------- regle reghyp 3 ajouter hypothese -ilexiste(A app x, x9 app A et x10 app A). --------------------------------------------------------- regle reghyp 3 ajouter hypothese -ilexiste(A app x, x8 app A). --------------------------------------------------------- regle partition1 3 ajouter hypothese -ilexiste(A app x, x9 app A). --------------------------------------------------------- regle partition1 3 ajouter hypothese -ilexiste(A app x, x10 app A). --------------------------------------------------------- regle partition1 3 ajouter objet x11 3 ajouter hypothese x11 app x 3 ajouter hypothese x8 app x11 3 ajouter hypothese x9 app x11 3 ajouter hypothese-traitee -ilexiste(A app x, x8 app A et x9 app A). --------------------------------------------------------- regle ilexiste 3 ajouter hypothese x2(x8, x8) --------------------------------------------------------- regle reghyp1 3 ajouter hypothese x2(x9, x8) --------------------------------------------------------- regle reghyp1 3 ajouter hypothese x2(x9, x9) --------------------------------------------------------- regle reghyp1 3 ajouter hypothese -ilexiste(A app x, x8 app A et x8 app A). --------------------------------------------------------- regle reghyp 3 ajouter hypothese -ilexiste(A app x, x9 app A et x8 app A). --------------------------------------------------------- regle reghyp 3 ajouter hypothese -ilexiste(A app x, x9 app A et x9 app A). --------------------------------------------------------- regle reghyp 3 ajouter hypothese x11 inc x1 --------------------------------------------------------- regle partition 3 ajouter objet x12 3 ajouter hypothese x12 app x 3 ajouter hypothese x9 app x12 3 ajouter hypothese x10 app x12 3 ajouter hypothese-traitee -ilexiste(A app x, x9 app A et x10 app A). --------------------------------------------------------- regle ilexiste 3 ajouter hypothese x2(x10, x9) --------------------------------------------------------- regle reghyp1 3 ajouter hypothese x2(x10, x10) --------------------------------------------------------- regle reghyp1 3 ajouter hypothese -ilexiste(A app x, x10 app A et x9 app A). --------------------------------------------------------- regle reghyp 3 ajouter hypothese -ilexiste(A app x, x10 app A et x10 app A). --------------------------------------------------------- regle reghyp 3 ajouter hypothese x12 inc x1 --------------------------------------------------------- regle partition 3 ajouter hypothese x11=x12 --------------------------------------------------------- regle partition2 remplacer x12 par x11 propager et supprimer x12 3 ajouter hypothese x10 app x11 supprimer hypothese x11=x12 supprimer objet x12 --------------------------------------------------------- regle egal 3 ajouter hypothese x2(x8, x10) --------------------------------------------------------- regle reghyp1 3 nouvelle conclusion vrai --------------------------------------------------------- regle stop1 theoreme 3 demontre 0 nouvelle conclusion vrai --------------------------------------------------------- regle et theoreme 0 demontre en 1.04 seconds ================================================================================