Preuve automatique dans le calcul propositionnel et les logiques trivalentes

Preuve automatique dans le calcul propositionnel et les logiques trivalentes J.A. Alonso, E. Briales, A. Riscos Universit´e de S´eville Introduction Nous pr´esentons une application des bases de Gr¨obner (bases standard) d’id´eaux de polynˆomes la v´erification des tautologies dans le Calcul Propositionnel et dans trois types de logiques trivalentes. L’id´ee base est de transformer les formules en polynˆomes, et de trouver l’´equivalent alg`ebrique de la d´eduction: nous verons des th´eor`emes faisant la liaison entre d´eduction et crit`eres de r´eduction alg`ebrique ([2], [3], [4]). A.- Bases de Gr¨obner dans k[X1, . . . , Xn] Soit k[X1, . . . , Xn] l’ensemble des polynˆomes sur X1, . . . , Xn, et avec les coefficients dans un corps k. Tout polynˆome ppeut s’´ecrire p=c1.t1+· · · +cm.tmo`u cisont les coefficients, et tison les monˆomes ordonn´es: t1>· · · > tmpar l’ordre lexicographique. On notera L(p) = c1.t1. Un ensemble fini de polynˆomes, F⊆k[X1, . . . , Xn] permet d´efinir une r´elation de r´eduction −→Fpar: p−→Fqssi il existe r∈Fet un monˆome atels que (i) a.L(r) est un monˆome de p (ii) q=p−a.r Si Fest clair, on notera −→Fsimplement par −→;∗ −→ est la clˆoture r´eflexive et transitive de −→. On notera par I(F) l’id´eal engendr´e par F. On utilisera la charact´erisation suivante: Fest una base de Gr¨obner ssi I(F) = {p:p∗ −→ 0}ssi pour tout p∃!q,−→-irr´eductible, tel que p∗ −→ q. Par exemple, pour mpremier, l’ensemble Fm={Xm 1−X1, . . . , Xm n−Xn} est toujours une base de Gr¨obner dans l’anneau Zm[X1, . . . , Xn]. B.- Tautologies dans le Calcul Propositionnel Soit P(X1, . . . , Xn) l’ensemble des propositions construites avec les connecteurs usuels ¬(non), ∨(ou), ∧(et), →(si ... alors ...), ↔(ssi) et les variables X1,...,Xn. Dans Z2on d´efinit les op´erations ¬0,∨0,∧0,→0,↔0par les tableaux a¬0a 0 1 1 0 a∨0b a∧0b a→0b a↔0b b0 1 0 1 0 1 0 1 a 0 0 1 0 0 1 1 1 0 1 1 1 0 1 0 1 0 1 ou, de fa¸con ´equivalente ¬0a=a+ 1 a∨0b=a.b +a+b a∧0b=a.b a→0b=a.b +a+ 1 a↔0b=a+b+ 1 Le sens logique de 1 sera “vrai” et de 0 sera “faux”. Les op´erations ont et´e d´efinies suivant le th´eor`eme de Stone [6]. On notera les propositions par P,Q. D´efinition B.1. Une r´ealisation est une application v:{X1, . . . , Xn} → Z2 Toute r´ealisation peut s’´etendre, de fa¸con unique, une application v0:P(X1, . . . , Xn)→Z2 telle que v0(Xi) = v(Xi),1≤i≤n v0(P∧Q) = v0(P)∧0v0(Q) v0(¬P) = ¬0v0(P) v0(P∨Q) = v0(P)∨0v0(Q) v0(P∧Q) = v0(P)∧0v0(Q) v0(P→Q) = v0(P)→0v0(Q) v0(P↔Q) = v0(P)↔0v0(Q) comme on peut d´eduire facilement des lois de formation des propositions. 2 D´efinition B.2. Pest une tautologie, |=P, ssi v0(P) = 1 pour toute r´ealisation v. D´efinition B.3. On d´efinit, r´ecursivement, une application B:P(X1, . . . , Xn)→Z2[X1, . . . , Xn] par B(P) =                    Xi, si Pest Xiet 1≤i≤n; B(Q)+1,si Pest ¬Q; B(Q)B(R) + B(Q) + B(R),si Pest Q∨R; B(Q)B(R),si Pest Q∧R; B(Q)B(R) + B(Q)+1,si Pest Q→R; B(Q) + B(R) + 1,si Pest Q↔R; A nouveau, les lois des formation des propositions nous garantissent la bonne d´efinition. Lemme B.4. Pour toute r´ealisation v, il existe un homomorphisme unique v∗:Z2[X1, . . . , Xn]→Z2 tel que v∗(Xi) = v(Xi),1≤i≤n. La preuve se fait en consid´erant maintenant la structure des polynˆomes. En plus, on peut tester facilement la commutativit´e du diagramme: P(X1, . . . , Xn)B −−−−→ Z2[X1, . . . , Xn] v0  y v∗  y Z2 id −−−−→ Z2 On arrive au r´esultat fondamental de cette section. On consid`ere l’ensemble F= F2={X2 1+X1, . . . , X2 n+Xn}. On a: Th´eor`eme B.5. |=Pssi B(P)∗ −→ 1[et Pest contradictoire ssi B(P)∗ −→ 0]. La preuve repose sur les lemmes Lemme B.6. Si p∗ −→ q, alors v∗(p) = v∗(q), pour toute r´ealisation v. Lemme B.7. p∗ −→ 0ssi v∗(p) = 0 pour toute r´ealisation v. qui sont des r´esultats strictement alg`ebriques. Comme nous avons annonc´e, le th´eor`eme B.5 met en r´elation un aspect exclusivement logique avec un aspect exclusivement alg`ebrique. 3 Exemples. P1= ((x→ ¬y)→ ¬y)B(P1)∗ −→ (xy +y+ 1) P2= (x∨ ¬x)B(P2)∗ −→ (1) P3= (((x→ ¬x)→x)→x)B(P3)∗ −→ (1) P4= ((x→y)∨(y→x)) B(P4)∗ −→ (1) P5= (x→(y→x)) B(P5)∗ −→ (1) P6= (x∧(x→y)→y)B(P6)∗ −→ (1) P7= ((¬¬x→x)→x∨ ¬x)B(P7)∗ −→ (1) P8= (x∧ ¬x)B(P8)∗ −→ (0) C.- Tautologies dans les Logiques Trivalentes On va maintenant d´ecrire le mˆeme processus pour les syst`emes de ÃLucasiewicz, G¨odel et Kleene, de logique trivalente. On d´efinit trois ensembles d’op´erations sur Z3(qui ont ses ´equivalents polynomiales, comme nous verons apr`es): a¬0 La 0 1 1 0 2 2 a∨0 Lb a∧0 Lb a→0 Lb a↔0 Lb b0 1 2 0 1 2 0 1 2 0 1 2 a 0 0 1 2 0 0 0 1 1 1 1 0 2 1 1 1 1 0 1 2 0 1 2 0 1 2 2 2 1 2 0 2 2 2 1 1 2 2 1 a¬0 Ga 0 1 1 0 2 0 a∨0 Gb a∧0 Gb a→0 Gb a↔0 Gb b0 1 2 0 1 2 0 1 2 0 1 2 a 0 0 1 2 0 0 0 1 1 1 1 0 0 1 1 1 1 0 1 2 0 1 2 0 1 2 2 2 1 2 0 2 2 0 1 1 0 2 1 a¬0 Ka 0 1 1 0 2 2 a∨0 Kb a∧0 Kb a→0 Kb a↔0 Kb b0 1 2 0 1 2 0 1 2 0 1 2 a 0 0 1 2 0 0 0 1 1 1 1 0 2 1 1 1 1 0 1 2 1 0 2 0 1 2 2 2 1 2 0 2 2 2 1 2 2 2 2 Maintenant, une r´ealisation est une application v:{X1, . . . , Xn} → Z3, 4 et peut s’´etendre, de fa¸con unique, `a une application vT:P(X1, . . . , Xn)→Z3 telle que vT(R) =                    v(Xi),si Rest Xiet 1 ≤i≤n; ¬TvT(P),si Rest ¬P; vT(P)∨TvT(Q),si Rest P∨Q; vT(P)∧TvT(Q),si Rest P∧Q; vT(P)→TvT(Q),si Rest P→Q; vT(P)↔TvT(Q),si Rest P↔Q o`u T=L,Gou K. De mˆeme, on dira que Pest une T-tautologie, |=TP, ssi vT(P) = 1 pour toute r´ealisation v. On d´efinit, tout comme `a B, les trois fonctions L, G, K :P(X1, . . . , Xn)→Z3[X1, . . . , Xn] r´ecursivement par: L(Xi) = Xi(1 ≤i≤n) L(¬P) = 2p+ 1 L(P∨Q) = 2p2.q2+p2.q +p.q2+p.q +p+q L(P∧Q) = p2.q2+ 2p2.q + 2p.q2+ 2p.q L(P→Q) = p2.q2+ 2p2.q + 2p.q2+ 2p.q + 2p+ 1 L(P↔Q) = 2p2.q2+p2.q +p.q2+p.q + 2p+ 2q+ 1 G(Xi) = Xi(1 ≤i≤n) G(¬P) = 2p2+ 1 G(P∨Q) = 2p2.q2+p2.q +p.q2+p.q +p+q G(P∧P) = p2.q2+ 2p2.q + 2p.q2+ 2p.q G(P→Q) = 2p2.q2+ 2p2.q +p.q2+ 2p2+ 2pq + 1 G(P↔Q) = p2.q2+ 2p2+p.q + 2q2+ 1 K(Xi) = Xi(1 ≤i≤n) K(¬P) = 2p+ 1 K(P∨Q) = 2p2.q2+p2.q +p.q2+p.q +p+q K(P∧Q) = p2.q2+ 2p2.q + 2p.q2+ 2p.q K(P→Q) = 2p2.q2+ 2p2+p.q2+ 2p.q +p+ 1 K(P↔Q) = 2p.q + 2p+ 2q+ 1 5 Pour chaque r´ealisation v, il existe un homomorphisme unique v∗:Z3[X1, . . . , Xn]→Z3 tel que v∗(Xi) = v(Xi), 1 ≤i≤n. En plus, on obtient la commutativit´e du diagramme: P(X1, . . . , Xn)T −−−−→ Z3[X1, . . . , Xn] vT  y v∗  y Z3 id −−−−→ Z3 Si on prend maintenant l’ensemble F=F3={X3 1+ 2X1, . . . , X3 n+ 2Xn}on a le Th´eor`eme C.1. |=TPssi T(P)∗ −→ 1. qui nous permet de programmer facilement la v´erification automatique des tautologies dans les trois syst`emes consid´er´es. Dans le diagramme suivant on voit la situation r´elative des tautologies. Les exemples P1`a P7, dej`a vus, ont la position qu’on indique. B L I G P1P2P3P4P5P6P7 I= Intuitionisme. Notez que, dans le syst`eme de Kleene, il n’y a pas de tautologies. Pourquoi ces trois types de logique trivalente? Le syst`eme de ÃLucasiewicz fut le premier historiquement; le sens logique du “2”est celui d’ˆetre “pas d´efinible”; le syst`eme nous permet la d´efinition d’op´erateurs modales, dont nous parlerons `a la fin. Il faut signaler que les op´erateurs modales ne sont pas d´efinibles dans le Calcul Propositionnel. Dans le syst`eme de G¨odel le sens logique du “2” n’a pas d’importance. G¨odel prouva que l’Intuitionisme n’est pas d´efinible par des tableaux, et il introduit son syst`eme parce que c’est une bonne aproximation (en fait, il y a des syst`emes d’axiomes pour l’Intuitionisme, de fa¸con telle qu’en ajoutant un nouveau axiome, on obtient les axiomes de G¨odel). Malheureusement les tautologies intuitionistes sont contenues dans les G- Tautologies, donc notre automatisme alg`ebrique sert plutˆot `a prouver des non-th´eor`emes. Dans le syst`eme de Kleene, le sens logique du “2” est celui d’ˆetre “pas encore d´efini” ou “inconnu”. Comme on a dej`a dit, il n’y a pas de K-Tautologies, mais notre proc´essus permet de tester aisement des formules avec les mˆemes valeurs de verit´e. Exemple. Q1= (x→y) Q2= (¬x∨y) K(Q1)∗ −→ (1 + 2x+xy2+x2y+ 2x2y2) 6 K(Q2)∗ −→ (1 + 2x+xy2+x2y+ 2x2y2) tandis que L(Q1)∗ −→ (1 + 2x+ 2xy + 2xy2+ 2x2y+x2y2) L(Q2)∗ −→ (1 + 2x+xy2+x2y+ 2x2y2) et G(Q1)∗ −→ (1 + 2xy +xy2+ 2x2+ 2x2y+ 2x2ye2) G(Q2)∗ −→ (1 + 2x2+x2y) La m´ethode d´ecrite peut s’appliquer `a tous les types de logique trivalente (ex. Bochvar), et mˆeme `a des logiques polivalentes (avec un nombre premier de valeurs), de fa¸con toute naturelle. D.- D´eduction dans le Calcul Propositionnel D´efinition D.1. Qest une cons´equence tautologique de (ou, on peut d´eduire Q`a partir de) P1, . . . , Pm,{P1, . . . , Pm} |=Q, ssi pour toute r´ealisation v, si v0(P1) = · · · =v0(Pm) = 1, alors v0(Q) = 1. Dans le Calcul Propositionnel, on a la charact´erisation ´equivalente: {P1, . . . , Pm} |=Q⇐⇒ |=P1∧ · · · ∧ Pm→Q qui va nous permettre d’utiliser les r´esultats de la section A. Malheureusement cette charact´erisation n’est pas valable dans les logiques non-classiques. En effet, on consid´ere dans P(X1, . . . , Xn) la r´elation d’´equivalence P≃Qssi v0(P) = v0(Q) pour toute r´ealisation v. L’ensemble des classes d’´equivalence, muni de l’extension naturelle des op´erations ¬,∨,∧ c’est une alg`ebre bool´eenne <P∗(X1, . . . , Xn),¬,∨,∧>nomm´ee alg`ebre de Lindenbaum- Tarski. Le point c’est que si B(X1, . . . , Xn) est l’anneau bool´een associ´e par le th´eor`eme de Stone, on a le Th´eor`eme D.2. L’application θ:B(X1, . . . , Xn)→Z2[X1, . . . , Xn]/I(F2) d´efinie par θ(P) = B(P)est un isomorphisme d’anneaux. Notez que Pest une classe de propositions ´equivalentes par la r´elation ≃, et que B(P) est une classe de polynˆomes ´equivalents par la r´elation induite par l’id´eal I(F2). Ce th´eor`eme, et aussi sa preuve, sont exclusivement techniques. Le r´esultat important c’est le Th´eor`eme D.3. Les conditions suivantes sont ´equivalentes: (i) {P1, . . . , Pm} |=Q (ii) θ(Q) + 1 ∈(θ(P1) + 1, . . . , θ(Pm) + 1) (iii) B(Q) + 1 ∈(B(P1)+1, . . . , B(Pm) + 1, X2 1+X1, . . . , X2 n+Xn) o`u 1r´epresente la classe des tautologies; par exemple, on peut ´ecrire 1 = X1∨ ¬X1. La preuve repose sur les lemmes 7 Lemme D.4. p1···pm.(q+ 1) = 0 ssi q+ 1 ∈(p1· · · pm+ 1) Lemme D.5. (p1· · · pm+ 1) = (p1+ 1, . . . , pm+ 1) qui sont des r´esultats faciles sur les classes de polynˆomes. Le majeur int´erˆet du th´eor`eme D.3 c’est l’´equivalence (i)⇐⇒ (iii); en effet, si on calcule une base standard pour l’id´eal, la preuve automatique des cons´equences est presque triviale. Voici l’algorithme: AX ={P1, . . . , Pm} F:= BG{p1+ 1, . . . , pm+ 1, X2 1+X1, . . . , X2 n+Xn} Q h:= FN(q+ 1) h= 0 AX |=Q AX 6|=Q Exemple 1. Pour l’ensemble AX1={¬e→(¬a∧ ¬b∧(c∨d)), a ∧(¬b∨ ¬c)→d, ¬b→ ¬a, c ↔ ¬d} on obtient F1={ae +a, be +b, ab +a, c +d+ 1, a2+a, b2+b, d2+d, e2+e} Si Q1.1=¬e→ ¬a∧ ¬bet Q1.2=a→(b↔c) on a h1.1= 0 et h1.2=ad respectivement. Pour le calcul de la base de Gr¨obner, nous avons d´evelopp´e un algorithme du type Buchberger [1] pour le cas sp´ecial Z2, avec un crit´ere de r´eduction des paires critiques, dˆu `a Chazarain [2]. Cette m´ethode pr´esente, face `a la m´ethode habituelle de R´esolution de Robinson, les avantages suivantes: •Nous pouvous travailler avec des formules quelconques, tandis que la r´esolution a besoin de formules en forme de clauses. 8 •Le proc´essus de r´esolution est formellement ´egal (c.`a.d. ´egalement complexe) que le calcul d’une base de Gr¨obner. Notre algorithme, en faisant les calculs une seule fois, “compile” les axiomes; le changement de proposition Qn’oblige pas `a refaire les calculs; la r´esolution doit refaire tout le proc´essus chaque fois qu’on change la formule Q. •Notre m´ethode permet de tester tr`es aisement l’´equivalence d’ensembles d’axiomes: il suffit de voir qu’on obtient la mˆeme base. Par exemple, si AX2={a→b, c ∨d, b →e, ¬(c∧d)} alors F2={ae +a, a2+a, ab +a, b2+b, be +b, d2+d, c +d+ 1, e2+e} donc, l’ensemble AX1est ´equivalent `a l’ensemble AX2. •De mˆeme, on peut tester l’inconsistance d’un ensemble d’axiomes. Par exemple, si AX3={b→a∧d, ¬c∨b, a → ¬d, c ∧d}, alors F3={1}: l’id´eal est l’anneau tout entier, donc AX3est inconsistante E.- Logique Modale Pour finir, on dira quelques mots sur logique modale. Dans le syst`eme de ÃLucasiewicz, on peut d´efinir deux nouveaux connecteurs: P:“P est possible” P:“P est n´ecessaire”. On consid`ere alors l’ensemble des propositions P0(X1, . . . , Xn) avec les connecteurs ¬,,,∨,∧,→,↔. Le point c’est que si on d´efinit sur Z3les ´operations L,Lpar aLaLa 0 1 0 1 0 1 2 1 0 on ´etend vLpar vL(P) =LvL(P); vL(P) =LvL(P) et Lpar L(P) = L(P)2; L(P) = 2L(P)2+ 2L(P) on arrive `a 9