Lógicas polivalentes y bases de Gröbner

L´ OGICAS POLIVALENTES Y BASES DE GR¨ OBNER Jos´e Antonio Alonso Jim´enez Emilio Briales Morales Departamento de Algebra Facultad de Matem´aticas Universidad de Sevilla The aim of this paper is to describe the application of the Gr¨obner bases to automated theorem proving in Many–Valued Logic INTRODUCCI´ ON El objetivo de la comunicaci´on es presentar una aplicaci´on de las bases de Gr¨obner a la demostraci´on autom´atica en l´ogicas proposicionales polivalentes. La estructura de la comunicaci´on es la siguiente: En la secci´on 1, recordamos conceptos sint´acticos y sem´anticos de las l´ogicas polivalentes. A continuaci´on, reducimos el problema de la validez en l´ogicas polivalentes al de pertenencia a un ideal (secci´on 2) y al de c´alculo de una base de Gr¨obner (secci´on 3). Finalmente, en la secci´on 4 damos algoritmos para resolver los anteriores problemas. 1 L´ OGICAS POLIVALENTES 1.1 Notaciones. En lo que sigue: (1) n,sson dos n´umeros enteros positivos. (2) {X1, . . . , Xn}es un conjunto cuyos elementos se interpretar´an como variables proposicionales. (3) {f1, . . . , fs}es un conjunto, disjunto con {X1, . . . , Xn}, cuyos elementos se interpretar´an como conectivas. (4) Para cada j∈ {1, . . . , s},δ(j) es un n´umero entero positivo que se interpretar´a como la aridad de la conectiva fj. 1.2 Definici´on. El conjunto P(X1, . . . , Xn) de las proposiciones en las variables X1, . . . , Xn y las conectivas f1, . . . , fsse define recursivamente por: (1) Para todo i∈ {1, . . . , n},Xi∈P(X1, . . . , Xn). (2) Si j∈ {1, . . . , s}yA1, . . . , Aδ(j)∈P(X1, . . . , Xn), entonces fj(A1, . . . , Aδ(j))∈ P(X1, . . . , Xn). 1.3 Notaciones. En lo que sigue: (1) Usaremos las letras A,B(posiblemente con sub´ındices) como variables para proposiciones. (2) pes un n´umero primo. (3) Zpes el cuerpo de los enteros m´odulo p, cuyos elementos se interpretar´an como valores de verdad. En particular, 0 se interpretar´a como falso y 1 como verdadero. (4) Para cada j∈ {1, . . . , s},Hjes una aplicaci´on de Zδ(j) pen Zpque se interpretar´a como la tabla de verdad de la conectiva fj. 1.4 Ejemplo. En el sistema trivalente de Lukasiewicz, L3,p= 3; 2 se interpreta como indeterminado; las conectivas son f1=¬(negaci´on), f2=♦(posibilidad), f3= ÃL (necesidad), f4=∨(disyunci´on), f5=∧(conjunci´on), f6=→(implicaci´on) y f7=↔(equivalencia); las aridades son δ(1) = δ(2) = δ(3) = 1, δ(4) = · · · =δ(7) = 2; y las tablas de verdad son las funciones Hidefinidas por a H1(a)H2(a)H3(a) 0 1 0 0 1 0 1 1 2 2 1 0 a b H4(a, b)H5(a, b)H6(a, b)H7(a, b) 0 0 0 0 1 1 0 1 1 0 1 0 0 2 2 0 1 2 1 0 1 0 0 0 1 1 1 1 1 1 1 2 1 2 2 2 2 0 2 0 2 2 2 1 1 2 1 2 2 2 2 2 1 1 1.5 Definiciones. (1) Una valoraci´on es una aplicaci´on v:{X1, . . . , Xn} → Zp. (2) Para cada valoraci´on vse define ˆv:P(X1, . . . , Xn)→Zprecursivamente por: ˆv(A) = ½v(A),si A∈ {X1, . . . , Xn}; Hj(ˆv(A1), . . . , ˆv(Aδ(j))),si Aes fj(A1, . . . , Aδ(j)). (3) Aes una tautolog´ıa,|=A, si para toda valoraci´on v, ˆv(A) = 1. (4) Aes una consecuencia tautol´ogica de {B1, . . . , Bm},{B1, . . . , Bm} |=A, si para toda valoraci´on v, ˆv(B1) = · · · = ˆv(Bm) = 1 =⇒ˆv(A) = 1. 1.6 Ejemplos. En L3se tiene: (1) |=X↔ ¬¬X. (2) X∨ ¬Xy (♦X∧(X→Y)) → ♦Yno son tautolog´ıas. (3) {♦X, X →Y} |=♦Y. 1.7 Nota. El objetivo del presente trabajo consiste en resolver mediante algoritmos algebraicos los siguientes problemas: •Problema 1 Dada una proposici´on A, decidir si |=A. •Problema 2 Dada una proposici´on A0y un conjunto finito de proposiciones {A1, . . . , Am}, decidir si {A1, . . . , Am} |=A0. 2 2 TAUTOLOGIAS E IDEALES 2.1 Notaci´on. En lo que sigue: (1) Zp[X1, . . . , Xn] es el anillo de polinomios en las indeterminadas X1, . . . , Xny con coeficientes en Zp. (2) Usaremos las letras p,q,r(posiblemente con sub´ındices) como variables para polinomios. (3) Usaremos las letras F,G(posiblemente con sub´ındices) como variables para conjuntos de polinomios distintos de cero. 2.2 Definici´on. Para cada valoraci´on v,v∗:Zp[X1, . . . , Xn]→Zpes el ´unico homomorfismo tal que v∗(Xi) = v(Xi), para todo i∈ {1, . . . , n}. 2.3 Definici´on. (1) Para cada conectiva fjse define la aplicaci´on θj:Zp[X1, . . . , Xn]δ(j)→Zp[X1, . . . , Xn] por θj(q1, . . . , qδ(j)) = X 0≤i1≤p−1 ··············· 0≤iδ(j)≤p−1 Hj(i1, . . . , iδ(j))Li1(q1). . . Liδ(j)(qδ(j)), donde L0(q) = 1 −qp−1yLi(q) = L0(q−i) para i∈ {1, . . . , p −1}. (2) La aplicaci´on θ:P(X1, . . . , Xn)→Zp[X1, . . . , Xn] est´a definida por: θ(A) = ½A, si A∈ {X1, . . . , Xn}; θj(θ(A1), . . . , θ(Aδ(j))),si Aes fj(A1, . . . , Aδ(j)). 2.4 Ejemplo. En L3, θ1(q) = 2q+ 1, θ2(q) = q2, θ3(q) = 2q2+ 2, θ4(q1, q2)= 2q2 1q2 2+q2 1q2+q1q2 2+q1q2+q1+q2, θ5(q1, q2)= q2 1q2 2+ 2q2 1q2+ 2q1q2 2+ 2q1q2, θ6(q1, q2)= q2 1q2 2+ 2q2 1q2+ 2q1q2 2+ 2q1q2+ 2q1+ 1, θ7(q1, q2)= 2q2 1q2 2+q2 1q2+q1q2 2+q1q2+ 2q1+ 2q2+ 1. 2.5 Lema. Para toda valoraci´on v, ˆv=v∗◦θ. Demostraci´on: Por inducci´on sobre la longitud de las proposiciones. 2.6 Definici´on. El ideal engendrado por F={q1, . . . , qm}es I(F) = ½m X i=1 riqi:ri∈Zp[X1, . . . , Xn]¾ 3 Escribiremos (q1, . . . , qm) en lugar de I({q1, . . . , qm}). 2.7 Lema. Si I= (Xp 1−X1, . . . , Xp n−Xn), entonces son equivalentes: (a) q∈I. (b) Para toda valoraci´on v,v∗(q) = 0. Demostraci´on: (a) =⇒(b): Por el Primer Teorema de Fermat. (b) =⇒(a): Por inducci´on sobre n. 2.8 Teorema. Sea A∈P(X1, . . . , Xn). Entonces |=A⇐⇒ θ(A)−1∈(Xp 1−X1, . . . , Xp n−Xn) Demostraci´on: |=A⇐⇒ (∀v)[ˆv(A) = 1] [por 1.5] ⇐⇒ (∀v)[v∗(θ(A)) = 1] [por 2.5] ⇐⇒ (∀v)[v∗(θ(A)−1) = 0] ⇐⇒ θ(A)−1∈(Xp 1−X1, . . . , Xp n−Xn) [por 2.7] 2.9 Lema. Sean q0, q1, . . . qm∈Zp[X1, . . . , Xn]. Son equivalentes: (a) Para toda valoraci´on v, v∗(q1) = · · · =v∗(qm) = 0 =⇒v∗(q0) = 0. (b) Para toda valoraci´on v, v∗((q0+q1+···+qm)(qp−1 1−1) ···(qp−1 m−1)) = 0. (c) (q0+q1+· · · +qm)(qp−1 1−1) · · · (qp−1 m−1) ∈(Xp 1−X1, . . . , Xp n−Xn). (d) q0∈(q1, . . . , qm, Xp 1−X1, . . . , Xp n−Xn). Demostraci´on: (a) =⇒(b): Por ser v∗homomorfismo y por el Primer Teorema de Fermat. (b) =⇒(c): Por el Lema 2.7. (c) =⇒(d): Trivial. (d) =⇒(a): Por el Primer Teorema de Fermat. 2.10 Teorema. Sean A0, A1, . . . , Am∈P(X1, . . . , Xn). Son equivalentes: (a) {A1, . . . , Am} |=A0. (b) θ(A0)−1∈(θ(A1)−1, . . . , θ(Am)−1, Xp 1−X1, . . . , Xp n−Xn). (c) m X i=0 (θ(Ai)−1) m Y j=1 p−1 X k=1 θ(Aj)k∈(Xp 1−X1, . . . , Xp n−Xn). Demostraci´on: (a) ⇐⇒ (b): Por 1.5, 2.5 y 2.9, se tiene {A1, . . . , Am} |=A0⇐⇒ ⇐⇒ (∀v)[ˆv(A1) = · · · = ˆv(Am) = 1 =⇒ˆv(A0) = 1] ⇐⇒ (∀v)[v∗(θ(A1)) = ···=v∗(θ(Am)) = 1 =⇒v∗(θ(A0)) = 1] ⇐⇒ (∀v)[v∗(θ(A1)−1) = · · · =v∗(θ(Am)−1) = 0 =⇒v∗(θ(A0)−1) = 0] ⇐⇒ θ(A0)−1∈(θ(A1)−1, . . . , θ(Am)−1, Xp 1−X1, . . . , Xp n−Xn) (b) ⇐⇒ (c): Por el Lema 2.9. 4 2.11 Nota. Mediante los Teoremas 2.8 y 2.10, los Problemas de la Nota 1.7 se reducen al siguiente: •Problema 3 Dado un conjunto finito de polinomios {q1, . . . , qm}y un polinomio q0 , decidir si q0∈(q1, . . . , qm). 3 IDEALES Y BASES DE GR¨ OBNER 3.1 Notaci´on. En lo que sigue: (1) Usaremos la letra a(posiblemente con sub´ındices) como variable para t´erminos (i.e. polinomios de la forma Xα1 1. . . Xαn n). (2) Usaremos la letra u(posiblemente con sub´ındices) como variable para elementos de Zp. 3.2 Definici´on. En el conjunto de los t´erminos de Zp[X1, . . . , Xn] se define la relaci´on >T por: Xα1 1. . . Xαn n>TXβ1 1. . . Xβn nsyss α1+· · · +αn> β1+· · · +βn´o α1+···+αn=β1+· · ·+βny (∃i∈ {1, . . . , n})[αi> βi∧(∀j)[1 ≤j < i →αj=βj]] 3.3 Definici´on. Sea qun polinomio distinto de cero. (1) Para cada t´ermino a, coef(a, q), representa el coeficiente de aen q. (2) El t´ermino l´ıder de q, TL(q), es el mayor t´ermino a(respecto de >T) tal que coef(a, q)6= 0. (3) El coeficiente l´ıder de qes CL(q) = coef(TL(q), q). (4) El resto de qes R(q) = q−CL(q)TL(q). 3.4 Definici´on. Sea qun polinomio distinto de cero, Fun conjunto de polinomios distintos de cero y aun t´ermino. (1) ρ(q, a) : Zp[X1, . . . , Xn]→Zp[X1, . . . , Xn] est´a definida por: ρ(q, a)(r) = r−coef(aTL(q), r) CL(q)aq. (2) r1−→q,a r2si r2=ρ(q, a)(r1)6=r1. (3) r1−→qr2si existe un t´ermino atal que r1−→q,a r2. (4) r1−→Fr2si existe un q∈Ftal que r1−→qr2. (5) r1 ∗ −→Fr2si existen k∈Nyq0, . . . , qk∈Zp[X1, . . . , Xn] tales que r1=q0−→Fq1−→F· · · −→Fqk=r2. 3.5 Definici´on. Sea Fun conjunto finito de polinomios distintos de cero. (1) qes reducible (respecto de F) si existe un rtal que q−→Fr; en caso contrario, se dice que qes irreducible (respecto de F). 5 (2) qes una forma irreducible (respecto de F) de rsi qes irreducible respecto de Fyr∗ −→Fq. 3.6 Nota. Dado un conjunto finito Fde polinomios distintos de cero, cada polinomio tiene al menos una forma irreducible respecto de F; pero puede tener m´as de una (ver ejemplo en 4.1.2). 3.7 Definici´on. Un conjunto finito Fde polinomios distintos de cero es una base de Gr¨obner si cada polinomio tiene una ´unica forma irreducible respecto de F. 3.8 Teorema (Buchberger, 1976). Si Fes una base de Gr¨obner, entonces I(F) = {q∈Zp[X1, . . . , Xn] : q∗ −→F0}. 3.9 Nota. Mediante el Teorema anterior, el Problema 3 de la Nota 2.11 se reduce a los siguientes: •Problema 4 Dado un conjunto finito Fde polinomios distintos de cero y un polinomio q, calcular una forma irreducible de qrespecto de F. •Problema 5 Dado un conjunto finito Fde polinomios distintos de cero, calcular una base de Gr¨obner Gtal que I(G) = I(F). 4 ALGORITMOS Y EJEMPLOS 4.1 Algoritmo de forma normal 4.1.1 Algoritmo. (de forma normal para el Problema 4) Entrada: Un conjunto finito F={q1, . . . , qm}de polinomios distintos de cero y un polinomio q=u1a1+···+ukak Salida: Una forma irreducible de qrespecto de F. Procedimiento: FN(q, F) i:= 1 mientras–que i≤m j:= 1 mientras–que j≤k si TL(qi) divide a aj entonces FNµq−ujaj CL(qi)TL(qi)qi, F¶ en–otro–caso j:= j+ 1 i:= i+ 1 devolver q 4.1.2 Ejemplo. En Z3[X, Y ] se consideran el conjunto F={q1=X2−1, q2=X2Y2+ 2X2Y+ 2XY 2+ 2XY + 2X, q3=X3−X, q4=Y3−Y}. Entonces FN(X3Y3, F) = XY , pero XY no es la ´unica forma irreducible de X3Y3respecto de F(por ejemplo, XY 2+Y2+ 2Yes otra). Por tanto, Fno es una base de Gr¨obner. 4.1.3 Nota. Es f´acil de comprobar que el algoritmo anterior termina y es correcto. 6 4.2 Algoritmo de base de Gr¨obner 4.2.1 Definici´on. Sean q1,q2dos polinomios distintos de cero. El S-polinomio de q1yq2 es S(q1, q2) = r a1u1 q1−r a2u2 q2, donde ai= CL(qi), ui= TL(qi) y r= mcm(u1, u2). 4.2.2 Algoritmo. (de base de Gr¨obner para el Problema 5) Entrada: Un conjunto finito F={q1, . . . , qm}de polinomios distintos de cero. Salida: Una base de Gr¨obner Gtal que I(G) = I(F). Procedimiento: BG(F) (∀i∈ {1, . . . , m})·ri:= qi CL(qi)¸ G:= {ri:i∈ {1, . . . , m}} G:= Reduce(G) [Supongamos que G={q0 1, . . . , q0 k}] B:= {(q0 i, q0 j) : 1 ≤i < j ≤k} mientras–que B6=∅hacer (q0 i, q0 j) un elemento de B B:= B− {(q0 i, q0 j)} r:= FN(S(q0 i, q0 j), G) si r6= 0 entonces BG(G∪ {r}) devolver G Subalgoritmo. (de reducci´on) Entrada: Un conjunto finito F={q1, . . . , qm}de polinomios m´onicos distintos de cero. Salida: Un conjunto Gde polinomios m´onicos tal que I(G) = I(F) y FN(q, G − {q}) = qpara todo q∈G. Procedimiento: Reduce(F) G:= F si (∃q∈G)[FN(q, G − {q})6=q] entonces i:= inf{j∈ {1, . . . , m}:FN(qj, G − {qj})6=qj} G:= G− {qi} q:= FN(qi, G) si q= 0 entonces Reduce(G) en–otro–caso Reduce(G∪ {q/CL(q)}) en-otro-caso devolver G 4.2.3 Ejemplo. Vamos a aplicar el algoritmo de bases de Gr¨obner al conjunto Fdel Ejemplo 4.1.2: En primer lugar aplicamos el algoritmo de reducci´on y obtenemos G={q0 1= X2−1, q0 2=Y3−Y, q0 3=XY 2+XY + 2Y2+X+Y}yB={(q0 1, q0 2),(q0 1, q0 3),(q0 2, q0 3)}. Elegimos (q0 1, q0 3)∈By calculamos r=FN(S(q0 1, q0 3), G) = XY + 2X+Y+ 2. Puesto que r6= 0, tenemos que calcular BG({q0 1, q0 2, q0 3, r}). Al aplicar el algoritmo de reducci´on se obtiene G={q0 1=X2−1, q0 2=XY + 2X+Y+ 2, q0 3=Y2+ 2}. Puesto que, 7 FN(S(q0 1, q0 2), G) = 0, FN(S(q0 1, q0 3), G) = 0, FN(S(q0 2, q0 3), G) = 0, se tiene que BG(F) = {X2−1, XY + 2X+Y+ 2, Y 2+ 2}. 4.2.4 Teorema. El algoritmo de la base de Gr¨obner es correcto. Demostraci´on (Esquema): La terminaci´on se demuestra a partir del teorema de la base de Hilbert y la correcci´on parcial a partir del siguiente teorema: Teorema (Buchberger) Ges una base de Gr¨obner syss para todo q1, q2∈G, S(q1, q2)∗ −→G0. 4.3 Algoritmos de validez 4.3.1 Algoritmo. (de deducci´on) Entrada: Una proposici´on A0y un conjunto finito Γ = {A1, . . . , Am}de proposiciones. Salida: “S´”, si Γ |=A0; “NO”, en caso contrario. Procedimiento: G:= BG(({θ(Ai)−1 : 1 ≤i≤m}∪{Xp i−Xi: 1 ≤i≤n})− {0}) q:= FN(θ(A0)−1, G) si q= 0 entonces devolver “S´” en–otro–caso devolver “NO” 4.3.2 Teorema. El algoritmo de deducci´on es correcto. Demostraci´on: Sean F={θ(A1)−1, . . . , θ(Am)−1, Xp 1−X1, . . . , Xp n−Xn}yG=BG(F− {0}). Γ|=A0⇐⇒ θ(A0)−1∈I(F) [por 2.10] ⇐⇒ θ(A0)−1∈I(G) [por 4.2.4] ⇐⇒ θ(A0)−1∗ −→G0 [por 3.8] ⇐⇒ FN(θ(A0)−1, G) = 0, ya que FN(θ(A0)−1, G) es la ´unica forma irreducible de θ(A0)−1 respecto de G. 4.3.3 Ejemplo. Consideremos, en L3, la proposici´on A0=♦Yy el conjunto Γ = {A1, A2}, siendo A1=♦XyA2=X→Y. Vamos a usar el algoritmo de deducci´on para decidir si Γ|=A0. G=BG({X2−1, X2Y2+ 2X2Y+ 2XY 2+ 2XY + 2X, X3−X, Y 3−Y} ={X2−1, XY + 2X+Y+ 2, Y 2+ 2}, por el Ejemplo 4.2.3. Puesto que, F N(θ(A0)−1, G) = FN(Y2−1, G) = 0, resulta que Γ|=A0. 4.3.4 Algoritmo. (de validez) Entrada: Una proposici´on A. Salida: “S´”, si |=A; “NO”, en caso contrario. Procedimiento: G:= {Xp i−Xi: 1 ≤i≤n} q:= FN(θ(A)−1, G) si q= 0 entonces devolver “S´” en–otro–caso devolver “NO” 8 4.3.5 Teorema. El algoritmo de validez es correcto. Demostraci´on: An´aloga a la del Teorema 4.3.2, observando que {Xp i−Xi: 1 ≤i≤n}es una base de Gr¨obner. 4.3.6 Ejemplo. Vamos a aplicar el algoritmo anterior para estudiar la validez en L3de las siguientes proposiciones: A1=X↔ ¬¬X(eliminaci´on de la doble negaci´on), A2=X∨¬X (ley del tercio excluido) y A3= (♦X∧(X→Y)) → ♦Y. Sea F={X3−X}. Puesto que, FN(θ(A1)−1, F) = FN(2X4+ 2X3+X2+ X, F) = 0, FN(θ(A2)−1, F) = FN(2X4+2X3+2X, F) = 2X2+XyFN(θ(A3)−1, F) = X2Y2+ 2X2+ 2XY 2+X+ 1, resulta que A1es una tautolog´ıa de L3yA2, A3no lo son. 4.3.7 Algoritmo. (de deducci´on. Versi´on 2) Entrada: Una proposici´on A0y un conjunto finito Γ = {A1, . . . , Am}de proposiciones. Salida: “S´”, si Γ |=A0; “NO”, en caso contrario. Procedimiento: G:= {Xp i−Xi: 1 ≤i≤n} q:= FNµm X i=0 (θ(Ai)−1) m Y j=1 p−1 X k=1 θ(Aj)k, G¶ si q= 0 entonces devolver “S´” en–otro–caso devolver “NO” 4.3.8 Teorema. El algoritmo anterior es correcto. Demostraci´on: An´aloga a la del Teorema 4.3.5. 5 IMPLEMENTACI´ ON Los anteriores algoritmos pueden implementarse directamente en REDUCE. El Ap´endice A es un programa en REDUCE de los algoritmos 4.3.4 y 4.3.7 para la l´ogica trivalente de Lukasiewicz. El Ap´endice B es una sesi´on en REDUCE usando el programa anterior (en la que se ha subrayado los mensajes del sistema). BIBLIOGRAF´A Buchberger, B. (1985), “Gr¨obner Basis: An Algorithmic Method in Polynomial Ideal Theory”, en N.K. Bose, ed. Multidimensional Systems Theory. Reidel, Dordrecht. Hsiang, J. (1985), “Refutational Theorem Proving using Term–Rewriting Systems” Artificial Intelligence,25, pp. 255–300. Kapur, D. y P. Narendran (1985) “An Equational Approach to Theorem Proving in First Order Predicate Calculus”, en 9th IJCAI. Moisil, G.C. (1969) The Algebraic Theory of Switching Circuits Pergamon Press, Oxford. Rescher, N. (1969) Many–valued Logic. McGraw–Hill, New York. 9