Razonamiento

razonM´todos algebraicos de razonamiento autom´tico e a Jos´ A. Alonso Jim´nez e e Sevilla, 4 de Julio de 1988 El objetivo del presente trabajo es la resoluci´n mediante algoritmos alo gebraicos de problemas del c´lculo proposicional cl´sico, de los c´lculos proposia a a cionales polivalentes y de la l´gica mon´dica. o a El cap´ ıtulo 1 es un estudio detallado de las relaciones can´nicas. Una orelaci´n binaria −→ en un conjunto E es can´nica si para cada elemento x de o o E existe un unico elemento y tal que x −→∗ y (i.e. existen x1 , . . . , xn tales que ´ x = x1 −→ x2 −→ · · · −→ xn = y) e y es −→-irreducible (i.e. no existe ning´n u z de E tal que y −→ z). La finalidad de este cap´ ıtulo es la demostraci´n o de condiciones equivalentes a la de canonicidad que nos permitan construiralgoritmos para calcular bases de Gr¨bner. o En cap´ ıtulo 2 estudiamos las bases de Gr¨bner en Zp [X1 , . . . , Xn ] y o damos nuevos criterios para la eliminaci´n de reducciones innecesarias en el o algoritmo de construcci´n de bases de Gr¨bner. o o En el cap´ ıtulo 3 usamos las bases de Gr¨bner para resolver algoritmio camente problemas de los c´lculos proposicionales. Est´ dividido en dos partes.a a En la primera, estudiamos el c´lculo proposicional cl´sico. Demostramos que a a una proposicion Q es consecuencia de un conjunto finito de proposiciones {P1 , . . . , Pm } si, y s´lo si, ST (Q) + 1 pertenece al ideal de Z2 [X1 , . . . , Xn ] o 2 engendrado por {ST (Pi ) + 1 : 1 ≤ i ≤ m} ∪ {Xi + Xi : 1 ≤ i ≤ n}, donde ST es la aplicaci´n del conjunto de proposiciones en el anillo Z2 [X1 , . . ., Xn ] o definida recursivamente por:  si P es una variable;  P,  ST (P ) = ST (Q) + 1, si P es ¬Q;   ST (Q)ST (R), si P es Q ∧ R. La segunda condici´n es decidible mediante bases de Gr¨bner, lo que nos pero o mite construir un algoritmo algebraico para decidir la deducibilidad. Otros problemas que se resuelven utilizando m´todos an´logos son el de la validez e a (dada una proposici´n,determinar si es v´lida), el de la consistencia (dado o a un conjunto de proposiciones, determinar si es consistente) y el de la equivalencia (dados dos conjuntos de proposiciones determinar si son equivalentes). En la segunda parte estudiamos los c´lculos proposicionales polivalentes. Dea mostramos que en un c´lculo proposicional con un n´mero primo, p, de valores a u de verdad, una proposici´n Q esconsecuencia de un conjunto finito de proposio ciones {P1 , . . . , Pm } si, y s´lo si, ST (Q)+1 pertenece al ideal de Zp [X1 , . . . , Xn ] o

p engendrado por {ST (Pi ) + 1 : 1 ≤ i ≤ m} ∪ {Xi − Xi : 1 ≤ i ≤ n}, donde ST es la aplicaci´n del conjunto de proposiciones en el anillo Zp [X1 , . . . , Xn ] o definida recursivamente por:

ST (P ) =

P,

si P es una variable;

STk (ST (Q1 ), . .. , ST (Qr )), si P es k(Q1 , . . . , Qr ).

y para cada conectiva r-aria k, STk es la aplicaci´n de Zp [X1 , . . . , Xn ]r en el o anillo Zp [X1 , . . . , Xn ] definida por:
r p−1

STk (q1 , . . . , qr ) =
0≤i1 ≤p−1 ··············· 0≤ir ≤p−1

Hk (i1 , . . . , ir )
m=1 j=0 j=im

qm − j . im − j

y Hk : Zr → Zp es la tabla de verdad de la conectiva k. La segunda condici´n o p esdecidible mediante bases de Gr¨bner, lo que nos permite construir un algoo ritmo algebraico para decidir la deducibilidad. An´logamente a lo obtenido en a la primera parte, damos algoritmos algebraicos para la validez, la inconsistencia y la equivalencia. Finalmente, mostramos c´mo transformar los anteriores o algoritmos para c´lculos proposicionales con un n´mero no-primo de valores de a u verdad. En elcap´ ıtulo 4 usamos las bases de Gr¨bner para resolver algorito micamente problemas de la l´gica mon´dica. Demostramos que si L es un o a lenguaje de primer orden cuyos s´ ımbolos no l´gicos son las constantes c1 , . . . , cr o y los s´ ımbolos de predicados mon´dicos p1 , . . . , pm y L es el lenguaje obtenido a a˜adi´ndole a L 2m nuevas constantes cr+1 , . . . , cn , una sentencia B de L es n...