Deducción Automática en Anillos Ternarios: Algunos Métodos de Procesamiento del Conocimiento Matemático

Deduion automatia en anillos ternarios: Algunos meto dos de pro esamiento del ono imiento matematio J.A. Alonso-Jimenez  J. Borrego-Daz y A. Chavez-Gonzalez Dpto. Cienias de la Computaion e Inteligenia Artiial. Universidad de Sevilla C/Tara s/n 41012, Sevilla e{mail: jborregoia.es Abstrat En este traba jo se presenta la demostraion automatizada de diversos resultados relativos a los anillos ternarios planos naturales [Kluk y 95℄. Este ejemplo motiva la utilizaion de diversas herramientas de la Logia Computaional para el proesamiento de los axiomas, y la obtenion automatia de demostraiones, as omo la presentaion de varios problemas de investigaion basia relativos a la gestion del ono imiento matematio on tenias de Inteligenia Artiial, basadas en la Logia Matematia. Area: Cienias de la Computaion e Inteligenia Artiial Palabras lave: Demostrai  on autom  atia, OTTER, geometr  as axiom  atias 1 Intro duion La demostraion automatia de teoremas es el area de las Cienias de la Computaion e Inteligenia Artiial que pretende alanzar la meta, propuesta p or Leibniz, de un alulo universal para la obtenion de pruebas meanias en Matematias. La utilidad de los sistemas obtenidos no se limita a las Matematias; se aplian a problemas de Inteligenia Artiial, dise ~no de iruitos, veriaion automatia de programas, y, en general, a ualquier tipo de problemas que requiera razonamiento. El termino razonamiento automatio , introduido en 1980, engloba tanto el dise ~no de estos programas omo otros programas relaionados (p.e. los generadores automatios de mo delos), y sus apliaiones [Wos 85℄. Los primeros programas dise~nados para la obtenion de pruebas meanias datan de los a ~nos inuenta. Pero no es hasta los a ~nos sesenta, on la apliaion direta de tenias lasias de la Logia Matematia (que se remontan a traba jos de Godel, Skolem y Herbrand), uando se obtiene un salto ualitativo en el desarrollo de estos sistemas (entre otros, [Davis y Putnam 60℄, [Robinson 65℄). A partir de estos traba jos, se han desarrollado m ultiples tenias y renamientos que han mejorado sustanialmente los demostradores automatios, hasta el punto de demostrar uestiones abiertas en Matematias 1 . El arater Logio{Matematio de tales sistemas (basados en logias de primer orden o sup erior), junto on la gestion eiente de los distintos motores de inferenia, hae que  Finaniado parialmente por el proyeto DGES PB96{0098-C04{04 y PAI TIC-137. y Finaniado parialemente p or el proyeto DGES PB96{1345 y PAI TIC-137. 1 Quizas el mas imp ortante sea la demostraion de la onjetura de Robbins [MCune 97℄ sobre algebras de Boole, una uestion profundamente estudiada por Tarski y propuesta hae unos sesenta a ~nos. su uso, omo asistente de investigaion en Matematias, sea omplejo: es neesario onoer los meanismos de deduion de nuevos resultados, omo se generan y/o desartan, para orientar, de alg un mo do, la b usqueda de la prueba. Esta irunstania es la diferenia fundamental entre estos sistemas y ualquier otro lengua je de programaion; el usuario no gestiona diretamente la ejeuion del programa, y es, p or tanto, un nuevo nivel de programaion. En el traba jo intro duimos diversas tenias utilizadas en la demostraion automatia de teoremas, usando omo gua de la exp osiion las pruebas que hemos obtenido, on un demostrador automatio, de algunos de los resultados de [Kluk y 95℄, justiando la orreion de algunas de las tenias empleadas. 2 Anillos ternarios planos naturales Los anillos ternarios, intro duidos p or Marshall Hall [Hall 43℄, representan una fundamentaion algebraia para diversas geometras axiomatias. Partiendo del estudio de las propiedades de tales geometras, abstrae su representaion utilizando una op eraion ternaria t : R 3 ! R (donde R es un onjunto en orresp ondenia biyetiva on to das las retas que pasan p or un punto, salvo una). Por ejemplo, en el plano real, la euaion y = t ( x; m; b ) representa la reta de y = mx + b . Existe una orresp ondenia entre los planos anes y las siguientes estruturas denidas en el lengua je L = f t; 0 ; 1 g ( 0 ; 1 onstantes): Deniion 1 Un anil lo ternario plano es una estrutura ( R; f t; 0 ; 1 g ) , on 0 6 = 1 , t : R 3 ! R veriando las siguientes propiedades: 1. 8 a 8 b 8  [ t (0 ; b;  ) =  ^ t ( a; 0 ;  ) =  ℄ . 2. 8 a [ t ( a; 1 ; 0) = a ^ t (1 ; a; 0) = a ℄ . 3. Si b; b 0 ; m; m 0 2 R on m 6 = m 0 , entones el siguiente sistema tiene soluion unia:  t ( x; m; b ) = y t ( x; m 0 ; b 0 ) = y 4. Si a; a 0 ; b; b 0 2 R , on a 6 = a 0 , entones el siguiente sistema tiene soluion unia:  t ( a; x; y ) = b t ( a 0 ; x; y ) = b 0 5. Para ualesquiera a; m;  , la euaion t ( a; m; x ) =  tiene una unia soluion. Se prueba que to do plano afn dene un anillo ternario plano (previa eleion de o ordenadas), y repro amente, to do anillo ternario dene un plano afn (una prueba se puede enontrar, p or ejemplo, en [Blumenthal 61℄) 2 . Por tanto, este tip o de estruturas interpreta, de manera algebraia, este tipo de geometras. El ob jeto de investigaion en este traba jo sera una variante de los anillos ternarios planos, intro duida en [Kluk y 95℄: Deniion 2 Una estrutura h M ; t;  ; f 0 L ; 0 R gi es un anil lo ternario plano natural (NPTR) si veria las siguientes ondiiones: 2 Axiomatiamente, un plano afn es una estrutura de inidenia donde ualesquiera dos puntos distintos estan onetados p or una unia reta; dado un punto P y una reta r no inidente on el, existe una unia reta paralela (disjunta) a r e inidente on P ; y existen uatro puntos no olineales tres a tres. ( A ) 8 x; y ; m 9 ! b [ t ( x; m; b ) = y ℄ . ( B ) 8 m; m 0 ; b; b 0 [ m 6 = m 0 ! 9 ! x ( t ( x; m; b ) = t ( x; m 0 ; b 0 ))℄ . ( C ) 8 x; x 0 ; y ; y 0 [ x 6 = x 0 ! 9 ! m; b ( t ( x; m; b ) = y ^ t ( x 0 ; m; b ) = y 0 ℄ . ( D ) 8 m; b [ t (0 L ; m; b  ) = b ℄ ^ 8 x; b [ t ( x; 0 R ; b  ) = b ℄ . ( E ) La funion ( : )  es biyetiva. 3 Prep o esamiento Para utilizar un demostrador automatio de manera eiente, es neesario reesribir los axiomas que denen a los NPTR 3 . De heho, salvo el axioma ( E ), to dos los demas axiomas estan esritos omo formulas en el lengua je de primer orden L 0 = f t;  ; 0 L ; 0 R g , on t; ( : )  smbolos de funion de aridades 3 y 1, resp etivamente, y 0 L y 0 R smbolos de onstante. Es trivial esribir una formula para ( E ), p ero antes de haerlo, es preferible desribir que tip o de transformaion apliaremos a estos axiomas. Una primera etapa onsiste en obtener una nueva axiomatizaion de la teora, simpli- ando la omplejidad de los axiomas, tanto de los uantiadores omo de la estrutura interna de la formula. Con resp eto a los uantiadores se utilizan las funiones de Skolem . Intuitivamente, una funion de Skolem representa la dep endenia funional de una variable on resp eto a otras, y su uso se fundamenta en el siguiente resultado lasio: Teorema 3 Sean T una teora de primer orden, ' ( ~x; y ) una formula y f un nuevo smbolo de funion n {ario. Si T 0 se obtiene a ~nadiendo a T el axioma 8 ~x [ 9 y ' ( ~x; y ) ! ' ( ~x; f ( ~x ))℄ entones la teora T 0 es una extension onservativa de T , es deir, T y T 0 demuestran los mismos teoremas en el lenguaje de T . Apliando adeuadamente el resultado a los axiomas de una teora, se obtiene una extension onservativa uyos axiomas son formulas sin uantiadores existeniales. Una vez eliminados estos, esribimos la matriz de ada formula en forma normal onjuntiva (onjunion de disyuniones de literales). En nuestro aso (teniendo en uenta que 9 ! x' abrevia la formula 9 x [ ' ( x ) ^ 8 y ( ' ( y ) ! x = y )℄), la extension onservativa que obtenemos es la teora N P T R 0 , formada p or las siguientes disyuniones (llamadas lausulas) 4 : A E : t ( X ; M ; ta ( X ; M ; B )) = B A U : ( t ( X ; M ; Y ) 6 = B ) j ( ta ( X ; M ; B ) = Y ) B E : ( M 1 = M 2) j ( t ( tb ( M 1 ; B 1 ; M 2 ; B 2) ; M 1 ; B 1) = t ( tb ( M 1 ; B 1 ; M 2 ; B 2) ; M 2 ; B 2)) B U : ( M 1 = M 2) j ( t ( X ; M 1 ; B 1) 6 = t ( X ; M 2 ; B 2)) j ( tb ( M 1 ; B 1 ; M 2 ; B 2) = X ) C E ; 1 : ( X 1 = X 2) j ( t ( X 1 ; tm ( X 1 ; X 2 ; Y 1 ; Y 2) ; tb ( X 1 ; X 2 ; Y 1 ; Y 2)) = Y 1) C E ; 2 : ( X 1 = X 2) j ( t ( X 2 ; tm ( X 1 ; X 2 ; Y 1 ; Y 2) ; tb ( X 1 ; X 2 ; Y 1 ; Y 2)) = Y 2) C U; 1 : ( X 1 = X 2) j ( t ( X 1 ; M ; B ) 6 = Y 1) j ( t ( X 2 ; M ; B ) 6 = Y 2) j ( tm ( X 1 ; X 2 ; Y 1 ; Y 2) = M ) C U; 2 ( X 1 = X 2) j ( t ( X 1 ; M ; B ) 6 = Y 1) j ( t ( X 2 ; M ; B ) 6 = Y 2) j ( tb ( X 1 ; X 2 ; Y 1 ; Y 2) = B ) D 1 : t (0 L ; M ; aster iso ( B )) = B D 2 : t ( X ; 0 R ; aster iso ( B )) = B E 1 : inv er sa ( aster iso ( B )) = B E 2 : aster iso ( inv er sa ( B )) = B Las dos ultimas formulas arman la existenia de la inversa (representada p or inv er sa ( : )) de la funion ( : )  que la representada p or omo didad omo aster iso ( : ) 3 Esto no es estritamente neesario, pues es automatizable, y de heho, OTTER lo hae 4 Las lausulas de tip o E son de existenia de soluion , las de tip o U son de uniidad , el smb olo j denota la disyunion y  es el smb olo de negaion. 4 Meanismos de inferenia El siguiente paso para traba jar on la teora es analizar la estrutura de sus axiomas, para elegir las reglas de inferenia adeuadas. Como es una teora on igualdad, junto a las reglas de inferenia propias de la logia de prediados, neesitamos reglas para el razonamiento on igualdad. Entre otras, algunas de las reglas que utilizamos son:  Resolui  on binaria: C 1 j ::: j C k j ::: j C n ; D 1 j ::: j D j j ::: j D m ( C 1 j ::: j C k  1 j C k +1 j ::: j C n j D 1 j ::: j D j  1 j D j +1 j ::: j D m )  donde  es un uniador de maxima generalidad de C k y el omplementario de D j .  Hiperresolui  on: M 1 ;  ; M k ;  A 1 j ::: j  A k j B 1 j ::: j B m ( B 1 j ::: j B m )  (siendo M i ; A i ; B i atomos), donde  es un uniador de maxima generalidad para M j y A j (1  j  k ).  Resolui  on UR: Es similar a la hip erresoluion, p ero devuelve un unio literal.  Demodulai  on: Consiste en utilizar una igualdad omo operador de reesritura: Si tenemos la igualdad t 1 = t 2 orientada, sustituimos en la formula to da instania de t 1 p or la resp etiva instania de t 2 .  Paramodulai  on: L 1 j ::: j L i ( t 1 ) j ::: j L n ; M 1 j ::: j M j  1 j ( t 2 = t 3 ) j M j +1 j ::: j M k ( L 1 j : : : j L i ( t 3 ) j ::: j L n j M 1 j ::: j M j  1 j ( t 2 = t 3 ) j M j +1 j M k )  donde  es un uniador de maxima generalidad de t 1 y t 2 , y L i ( t 3 ) se obtiene sustituyendo to da estania de t 1 en L i p or t 3 (modulo uniador). Estas reglas forman un onjunto refutaionalmente ompleto para la logia lausal de primer orden on igualdad. 5 El demostrador automatio OTTER El demostrador que utilizamos en este traba jo es OTTER [MCune 94℄, desarrollado en el Argonne National Lab oratory, uno de los mas p otentes, y que admite un amplio onjunto de reglas de inferenia, estrategias de b usqueda, et. OTTER demuestra p or refutaion, es deir, dado un onjunto de formulas, intenta deduir una inonsistenia. El esquema de su funionamiento se basa en la estrategia del onjunto sop orte [Wos et al. 65℄: Divide el onjunto de entrada en dos sub onjuntos, las usables y las de soporte . En general, el onjunto de usables suele ser un onjunto onsistente de formulas (p or ejemplo, la teora a estudiar) y el onjunto sop orte el resto (usualmente, la negaion del teorema a demostrar). La estrategia onsiste en apliar las reglas de inferenia eligiendo al menos una formula del onjunto sop orte y aadiendo las onlusiones a ese onjunto (las reglas de inferenia son adeuadas, y p or tanto no es p osible deduir una inonsistenia a partir de un onjunto onsistente) hasta vaiar el onjunto soporte (demostraion no enontrada) o llegar a una inonsistenia. El usuario deb e elegir las reglas de inferenia que se utilizaran y la partiion del onjunto original. Hay que tener en uenta que la estrategia del onjunto sop orte no es ompleta (ualquier partiion del onjunto de entrada no ondue a una inonsistenia). De las lausulas as generadas, OTTER utiliza diversos meanismos para retener las que son interesantes. 6 Teoremas demostrados En esta seion omentamos las pruebas obtenidas on el demostrador. Salvo algunas exep- iones imp ortantes, una primera prueba del teorema la hemos obtenido mediante el mo do autonomo auto2 de OTTER, que es una op ion que, al menos parialmente, automatiza la eleion de las reglas de inferenia y de la estrategia a seguir para enontrar la prueba. Una vez onseguida una prueba, hemos depurado la estrategia de b usqueda de esta para enontrar una mas simple. El traba jo ha sido realizado on la ultima version UNIX/LINUX del programa, en un PC (AMD K6{400). Por uestiones de espaio, solo presentamos algunas araterstias de dihas pruebas. 6.1 Uniidad de 0 L , 0 R Las pruebas obtenidas de la uniidad de los elementos 0 L y 0 R en un NPTR son: Teorema 4 Los elementos 0 L y 0 R son unios on esa propiedad. Demostraion: Uniidad de 0 L : Enontrada p or OTTER en 0.07 segundos: 2 [℄ M1=M2|t(X,M1,B1)!=t(X,M2,B2)|tb(M1,B1,M2,B2)=X. 3 [℄ t(ol,M,asteriso(B))=B. 4 [℄ ol!=o. 5 [℄ t(o,M,asteriso(B))=B. 8 [ur,4,2,3℄ tb(ol,asteriso(t(ol,o,A)),o,A)=ol. 12 [ur,5,2,4℄ tb(ol,asteriso(t(o,o,A)),o,A)=o. 16,15 [para-into,8.1.1.2.1,3.1.1℄ tb(ol,asteriso(A),o,asteriso(A))=ol. 19 [para-into,12.1.1.2.1,5.1.1,demod,16℄ ol=o. 21 [binary,19.1,4.1℄ $ F. Las lausulas no inferidas (las hipotesis, on [℄) son axiomas de N P T R 0 o la negaion del teorema. Por ejemplo, las lausulas ol!=o y t(o,M,asteriso(B))=B arman la existenia de otro ero a la izquierda. La prueba de la uniidad de 0 R obtenida es: 5 [℄ X1=X2|t(X1,M,B)!=Y1|t(X2,M,B)!=Y2|tm(X1,X2,Y1,Y2)=M. 7 [℄ t(X,or,asteriso(B))=B. 8 [℄ or!=o. 9 [℄ t(X,o,asteriso(B))=B. 19,18 [ur,8,5,7,7℄ tm(or,o,A,A)=or. 94 [ur,9,5,8,9,demod,19℄ or=o. 96 [binary,94.1,8.1℄ $ F. 6.2 Propiedades del pro duto A partir de la op eraion ternaria t se pueden denir una multipliaion y una suma en un N P T R . El pro duto se dene omo a  b = t ( a; b; (0 L )  ) se verian las siguientes propiedades: Prop osiion 5 Sea M un NPTR. En las ondiiones anteriores, se veria que: 1. Para ualesquiera a; b 2 M , si a 6 = 0 L , existe un unio elemento x tal que a  x = b . 2. Para ualesquiera a; b 2 M , si a 6 = 0 R , existe un unio elemento x tal que x  a = b . 3. Para ualesquiera a; b 2 M a  b = 0 L sii a = 0 L o b = 0 R . Propiedad Tiemp o (s.) Cl. generadas Retenidas Long. prueba (1), uniidad 0.06 590 146 7 (1), existenia 0.02 145 58 9 (2), uniidad 0.01 55 20 6 (2), existenia 0.01 9 5 4 (3), = ) 0.02 56 27 6 (3), ( = 0.00 14 10 2 6.3 Propiedades de la suma De la propiedad (1) de la prop osiion anterior se tiene que para ada x 6 = 0 L existe un unio elemento e ( x ) 2 M tal que x  e ( x ) = x . Si denimos e (0 L ) = 0 R , la funion e : M ! M esta bien denida (en N P T R 0 ) p or las lausulas  (e(ol) = or).  (X = ol) | (prod(X,e(X)) = X).  (X = ol) | (prod(X,Y) != X) | (e(X) = Y). As, denimos una nueva op eraion, +, omo a + b := t ( a; e ( a ) ; b  ). Prop osiion 6 Sea M un N P T R 0 1. Para todo a 2 M , a + 0 L = a y 0 L + a = a . 2. Para ualesquiera a; b 2 M existe un unio x 2 M tal que a + x = b . Propiedad Tiemp o (s.) Cl. generadas Retenidas Long. prueba (1) a + 0 L = a 0.01 9 6 5 (1) (0 L + a ) = a 0.00 3 3 1 (2), existenia 0.02 95 83 7 (2), uniidad 0.01 98 31 7 6.4 B usqueda de soluiones Po dra pareer que, on las demostraiones p or refutaion, se pierde ierta informaion que es interesante. Por ejemplo, en la propiedad (2) de la prop osiion 5, 8 a [ a 6 = 0 R ! 9 ! x ( x  a = b )℄ puede ser muy util ono er la expresion de x on resp eto a los elementos a y b . Existe una primera diultad para resolver esta uestion, y es si tal expresion existe: Demostrando la existenia de un elemento no nos asegura que este se pueda expresar de manera simple en el lengua je utilizado. En el aso que nos oupa, esta propiedad s es ierta; es onseuenia del Teorema de Herbrand : Teorema 7 Sea T una teora de primer orden uyo axiomas son formulas abiertas, y sea ' ( x ) una formula abierta. Son equivalentes:  T ` 9 x' ( x )  Existen t 1 , . . . t n terminos errados tales que T ` ' ( t 1 ) _ ::: _ ' ( t n ) . Corolario 8 Existe un L 0 {termino t ( u; v ) tal que N P T R 0 ` u 6 = 0 R ! t ( u; v )  u = v Demostraion: Para apliar el teorema anterior a la teora N P T R 0 , expandimos el lengua je de tal teora on dos nuevas onstates, a; b y tomamos la teora T en el nuevo lengua je uyos axiomas son los de N P T R 0 . Por tanto, T ` 9 x [ a 6 = 0 R ! ( a  x = b )℄ Apliando el teorema anterior, existen terminos errados t 1 ;:::;t n tales que T ` ( a 6 = 0 R ! t 1  a = b ) _    _ ( a 6 = 0 R ! t n  a = b ) p ero omo T ` a 6 = 0 R ! 9 ! x [ x  a = b ℄, utilizando los axiomas de igualdad, se onluye que T ` a 6 = 0 R ! t 1  a = b El termino t 1 es un termino (errado) en el lengua je L 0 [ f a; b g . Si t ( u; v ) es el L 0 {termino que se obtiene sustituyendo las onstantes a y b p or u y v resp etivamente, entones, p or el teorema de onstantes se veria que N P T R 0 ` u 6 = 0 R ! t ( u; v )  u = v El orolario anterior nos asegura la existenia de una expresion de este tip o. La fundamentaion de la obtenion de respuestas es una generalizaion del onepto de respuesta utilizada en programaion logia (por ejemplo en PROLOG) [Kunen 96℄. De heho, OTTER tiene implementado una funion, $ ans ( X ), que devuelve el valor obtenido para la variable X . La b usqueda del termino t ( u; v ) sigue la idea de la demostraion anterior: La entrada de OTTER son los axiomas de N P T R 0 junto on el siguiente onjunto sop orte:  (a != or).  (prod(X,a) != b) | $ ans(X) y (en 0.1 seg.) nos devuelve la soluion 5 $ans(tb(or,asteriso(b),a,asteriso(ol))) , es deir, t ( u; v ) = tb (0 R ; v  ; u; (0 L )  ) Interpretando este resultado en el lengua je original de NPTR, el elemento x tal que x  a = b , para a 6 = 0 R , es la unia soluion de la euaion t ( x; 0 R ; b  ) = t ( x; a; (0 L )  ). 6.5 Isotopas: B usqueda de funiones Veamos p or ultimo, omo se puede estudiar la existenia de funiones usando el demostrador. Aparentemente, el razonamiento on funiones debera de utilizar una logia de orden superior. Sin embargo, no es neesario este tip o de ampliaiones en general. Veamos un ejemplo. El teorema 4.2 de [Kluk y 95℄ arma que la propiedad de ser NPTR se onserva ba jo isotopas. Una isotopa entre dos anillos ternarios planos ( M ; t 1 ) y ( M ; t 2 ) (para simpliar, on el mismo universo) es una 4{upla de p ermutaiones de M , ;  ;  ; Æ , tales que para ualesquiera x; m; b 2 M Æ ( t 2 ( x; m; b )) = t 1 (  ( x ) ;  ( m ) ;  ( b )) El teorema asegura que si ( M ; t 1 ;  ; 0 L ; 0 R ) es un NPTR, entones ( M ; t 2 ;   1 (0 L ) ;   1 (0 R )) admite una estrutura de NPTR, para una ierta apliaion b 7! b  No vamos a desribir la demostraion, usando OTTER, de este heho, solo nos ouparemos de la uestion mas imp ortante, la existenia de la apliaion b 7! b  tal que ( M ; t 2 ;  ;   1 (0 L ) ;   1 (0 R )) es un NPTR. Para enontrar tal funion, razonamos omo en la subseion anterior, y tomamos omo onjunto sop orte las siguientes formulas: delta(t2(X,M,B)) = t(alfa(X),beta(M),gamma(B)). (inversa-delta(delta(X)) = X). (delta(inversa-delta(X)) = X). 5 Esta no es la soluion que ofree OTTER en el mo do auto2, que es mas ompleja. La que ofreemos ha sido obtenida apliando distintas estrategias para dirigir al demostrador haia una simpliada. Como ya hemos justiado anteriormente, ualquier soluion denota el mismo elemento, pues es unio. (alfa(inversa-alfa(X)) = X). (inversa-alfa(alfa(X)) = X). (beta(inversa-beta(X)) = X). (inversa-beta(beta(X)) = X). (gamma(inversa-gamma(X)) = X). (inversa-gamma(gamma(X)) = X). (alfa(ol2) = ol). (beta(or2) = or). (all X ((all M (t2(ol2 , M , X) = b)) -> $ans(X))). La ultima de las uales exige la respuesta para X que nos asegura que   1 (0 L ) es el ero a la izquierda. La respuesta obtenida es $ans(inversa-gamma(asteriso(delta(b)))) , es deir, x  =   1 ( Æ ( x )  ) es la apliaion p edida. 7 Conlusiones Hemos mostrado el uso fundamentado de un demostrador automatio para la investigaion en Matematias, eligiendo omo aso de estudio los anillos ternarios. El futuro traba jo reejara, en el aso esp eial de este tip o de estruturas, los prinipales problemas a resolver en este amp o, entre los que destaamos  El dise ~no de estrategias para eliminar, durante el pro eso, informaion redundante.  Estrategias para onduir la prueba y obtener as demostraiones mas simples.  En el aso onreto de los anillos ternarios, busar otas para la omplejidad de las lausulas de una demostraion en funion del teorema{ob jetivo, de origen geometrio. Referenias [Blumenthal 61℄ Blumenthal, L.M.: A mo dern view of Geometry. Freeman, 1961. [Davis y Putnam 60℄ Davis, M.; Putnam, H.: A omputing proedure for quantiation theory. Journal of the ACM 7 (3), 201{215 (1960). [Hall 43℄ Hall, M.: Projetive Planes Trans. of AMS 54, 229{277 (1943). [Kluk y 95℄ Kluk  y, D.: Isotopi Invariants of natural planar ternary rings. Mathematia Bohemia 120 (3), 325{335 (1995). [Kunen 96℄ Kunen, K.: The Semantis of Answer Literals. J. Automated Reasoning 17 (1996), 83-95. [MCune 94℄ MCune, W.: OTTER 3.0 Referene Manual and Guide. Teh. Rep ort ANL- 94/6, Argone National Lab oratory, 1994. [MCune 97℄ MCune, W.: Solution of the Robbins Problem , J. Automated Reasonning 19 (3), 263{276 (1997). [Robinson 65℄ Robinson, J.A.: A mahine oriented logi based on the Resolution Priniple . J. of the ACM 12, 23{41 (1965). [Wos et al. 65℄ Wos, L.; Robinson, G.; Carson, D.: EÆieny and ompleteness of the set of support strategy in theorem proving. J. of ACM 12 (4), 536{541 (1961). [Wos 85℄ Wos, L.: What is Automated Reasonning? J. of Automated Reasonning 1, 6{9 (1985).