Demostración Automática

Mtro. José Alfredo Amor

Facultad de Ciencias, UNAM

Dr. Raymundo Morado

Instituto de Investigaciones Filosóficas, UNAM

1. Introducción

La lógica es tanto el arte como la ciencia de la demostración. Nos enseña a inferir correctamente y nos explica y analiza el por qué de esa corrección. Nos dice qué es obtener buenas conclusiones a partir de la información inicial y nos permite escudriñar la estructura más profunda de la razón.

Un ideal de la Lógica es entender la inferencia correcta tan bien que incluso sea posible dar recetas, procedimientos automáticos para que cualquier agente, humano o no, pueda tener garantizada la corrección lógica de su manera de procesar la información. Debemos aquí distinguir entre el ideal de inferir bien y el de demostrar. Leibniz dijo una vez que sería bueno, en vez de largas discusiones, poder simplemente sentarse a calcular quién tiene la razón. Hoy día las discusiones sobre aritmética son fácilmente zanjadas consultando una calculadora. Se trata tan sólo de obtener la conclusión. Pero la calculadora, aunque da la respuesta correcta, no la demuestra. La razón es que normalmente no nos provee con la justificación de su inferencia. Si alguien tan sólo nos da una respuesta, aunque la respuesta sea correcta, no nos ha dado una demostración. Para decir que tenemos una demostración, además de que los pasos inferenciales sean legítimos, necesitamos tener razones que los legitimen. Cualquier persona puede hacer una buena inferencia. Pero si se le pregunta por la justificación de tal inferencia, es común que la persona no la sepa. Cuando añadimos claras justificaciones a las buenas inferencias es cuando tenemos pruebas. Tales pruebas o demostraciones serán tan buenas como las justificaciones. Hay buenas pruebas y malas pruebas.

La demostración automática (DA) extiende el ideal de Leibniz de convertir a la lógica en un cálculo mecánico. Desde el siglo XIII, Raymundo Lull construyó aparatos rudimentarios para explorar automáticamente series de combinaciones entre conceptos. Pero fue hasta el siglo XX que aparecieron aparatos capaces de procesar información con suficiente velocidad y exactitud. Estamos en el comienzo de la era de la DA, y esperamos que con estos auxiliares teóricos y prácticos nuestra capacidad de entender el mundo se acreciente exponencialmente.

El ideal es automatizar la construcción de pruebas de la misma manera que tenemos formas automáticas de hacer aritmética, o recetas de cocina. Por supuesto, no tenemos recetas para todo. Pero mientras más recetas tengamos, mejor. Las recetas, como lo sabe cualquier buen cocinero o cocinera, no sólo no limitan nuestra creatividad sino que nos ayudan a librarnos de la parte que no es creativa. Hacemos mecánicamente la parte "mecánica" y así podemos concentrarnos en la parte interesante, las variaciones sobre el tema básico ya dominado. Las recetas no son instrumentos para pensar menos, sino para hacer más expedita la parte mecánica. Por ejemplo, antiguamente había que copiar los libros a mano. Ahora que tenemos máquinas para reproducirlos, podemos emplear nuestro tiempo en leerlos, lo que requiere más pensamiento. Claro, algunas personas se asustan con el progreso. Creen que usar computadores significa dejar de pensar. Eso es tan absurdo como tener miedo de usar termómetros que automáticamente procesan información sobre la temperatura del medio ambiente y la convierten en algo más fácil de manipular. O como temer a la célula fotoeléctrica que activa un farol de la calle al atardecer, o a un reloj despertador que nos avisa del paso del tiempo.

El procesamiento de la información no es en sí mismo ni bueno ni malo. Podemos emplearlo de miles de maneras. Pero la célula fotoeléctrica, el termómetro, y el reloj deben procesar bien la información. ¿Qué es procesar bien la información? Eso no lo sabemos por completo todavía. La lógica es una ciencia en desarrollo. Pero ya sabemos una parte importante de la respuesta. Por ejemplo, si la conclusión a la que llegamos a partir de los datos iniciales es inevitable, entonces el procesamiento de la información fue bueno. Esta "inevitabilidad" le da certeza a la conclusión: si los datos corresponden a la realidad, la conclusión corresponde también. Buscando esta seguridad, los primeros desarrollos lógicos de la DA trataron de usar lógicas que garantizaran el paso seguro de los datos iniciales o premisas a las conclusiones. Nosotros hablaremos sobre todo de métodos seguros e infalibles para procesar información, pero debemos mencionar que tales métodos pueden costar mucho tiempo y recursos. Para algunos objetivos, es sensato utilizar sistemas menos exigentes: lógicas de probabilidades, factores de confianza, inferencias no-monotónicas, lógica difusa, etc. Estos son desarrollos relativamente más recientes, y no los tocaremos en detalle.

En esta sección introductoria, dibujaremos un breve panorama histórico para ubicar a la DA dentro del desarrollo de las máquinas inteligentes. La idea conductora es que las máquinas lógicas pueden tener muchas implementaciones y estar dirigidas a toda una gama de aplicaciones. De momento pensamos a los sistemas de DA como computadoras a base de circuitos eléctricos dentro de tabletas de silicón. Pero han sido (y serán) muchas otras cosas. Concluimos la introducción con una presentación de diferentes razones para desarrollar la DA, tanto por su utilidad teórica como práctica.

La segunda sección incluye apartados sobre la programación lógica (muy breve, pues es tratada en otra parte de este libro) y sobre el Teorema Básico para las pruebas por refutación. Para dar una idea más rica de lo que puede ofrecer la DA, revisamos mecanismos básicos usados en casi todos los sistemas de este tipo: el uso de la unificación mediante la substitución, la regla de resolución y ejemplos de transformación a forma clausular. A lo largo de esta sección usamos ejemplos clásicos pero con enfoques nuevos, como por ejemplo una curiosa versión de la paradoja de Russell y una exploración a fondo de una forma más sencilla y más poderosa de una fórmula de Gilmore.

Para estas alturas, nuestros lectores habrán visto que la lógica para una máquina no siempre se parece a la de los humanos. Los humanos tenemos ventajas y desventajas frente a un sistema no humano de inferencia. En la tercera parte pasamos revista a reglas, estrategias y métodos, cuyo uso y desarrollo han aportado contribuciones originales a la teoría de los sistemas lógicos. Estos mecanismos no intentan ser intuitivos y obvios para los humanos sino eficientes para las máquinas; no elegantes y poderosos en principio, sino prácticos y astutos en el uso. Esta orientación hace que estos desarrollos lógicos transiten por caminos poco explorados y que la lógica se enriquezca con sistemas inferenciales en los que el hombre ya no es el centro del universo.

Antes de entrar en materia, quisiéramos mencionar que este ensayo contiene algunas cosas de interés incluso para conocedores del tema. Ubicamos brevemente a la DA en la historia de la lógica y tratamos de explicar su utilidad y dar ejemplos didácticos. Los ejemplos incluyen variantes novedosas de paradojas que abarcan desde los griegos hasta Russell.

En el aspecto técnico, nuestra presentación de la subsunción es completamente general y no se limita a la subsunción de cláusulas, como es común en la literatura. Ofrecemos una formulación más poderosa y breve de una fórmula famosa de Gilmore; esto permite dar una prueba especialmente instructiva de su validez por resolución. Finalmente, el lector encontrará una prueba de la ley de cancelación para grupos mediante paramodulación.

1. Panorama histórico

Cuando hablamos de la automatización de las demostraciones es inevitable pensar en máquinas que implementen ciegamente algunos principios lógicos. El uso de máquinas para apoyar la actividad lógica tiene una larga y extraña historia. En el delicioso libro de Martin Gardner (Gardner 1983), se encontrará información a granel. Por ejemplo, a finales del siglo XIII, Raymundo Lull creó un abigarrado sistema de círculos de metal o pergamino, pintados de vivos colores. Era una máquina lógica para producir combinaciones de conceptos. Hace doscientos años, Charles Stanhope reconstruyó a los silogismos con madera y cristal. En 1886, el lógico Charles Dodgson (quien escribió Alicia en el País de las Maravillas bajo el pseudónimo de Lewis Carroll) usó cartón y piezas de colores. En 1903 Annibale Pastore usó bandas y ruedas para probar estructuras silogísticas. Éstos no fueron juegos inútiles. Lull trató de usar la combinatoria para la defensa de la religión católica, Stanhope estudió a la predicación como identidad, Carroll generalizó los diagramas de Euler y Venn mientras que Pastore dió una de las mas dramáticas demostraciones de la presencia de estructuras "lógicas" en fenómenos de mecánica simple.

La primera máquina lógica de importancia fue hecha construír en 1869 por William Stanley Jevons. El "piano lógico" de Jevons fue específicamente creado para ilustrar en el salón de clase la superioridad de la nueva lógica booleana sobre la anquilosada teoría aristotélica. Después vendrían las máquinas de Allan Marquand (1885) y Charles P. R. Macaulay (1913). Fue natural reemplazar poleas y engranes con circuitos eléctricos cuando éstos aparecieron. La primera máquina lógica eléctrica fue usada para resolver silogismos por Benjamin Burack en 1936, y once años después dos jóvenes estudiantes de licenciatura, William Burkhart y Theodore A. Kalin construyeron la primera máquina lógica eléctrica para ahorrarse esfuerzo haciendo los ejercicios que les dejaba su maestro, Quine. Muchas otras han seguido, como aquella construída en 1951 por Robert W. Marks que anunciaba por un alto-parlante cuando el enunciado era falso, en una voz profunda: "Mi nombre es Leibniz Boole De Morgan Quine. No soy sino un robot complicado y algo neurótico, pero me da un gran placer anunciar que su afirmación es totalmente falsa" ["My name is Leibniz Boole De Morgan Quine. I am nothing but a complicated and slightly neurotic robot, but it gives me great pleasure to announce that your statement is absolutely false"].

A mediados de los años cincuenta, el desarrollo de las computadoras permitió a las universidades el acceso a las primeras máquinas y en 1954, en un congreso en la Universidad de Cornell, se reunieron un número considerable de lógicos y computólogos. Abraham Robinson, de los Laboratorios Argonne, propuso utilizar los "Universos de Herbrand" y algunos teoremas de la lógica para atacar el problema de usar computadoras para demostración automática de teoremas.

En 1957 se publican los resultados de una máquina que demuestra, llamada "The Logic Theory Machine", realizado por Newel, Simon y Shaw, llegando a demostrar 40 teoremas de Principia Mathematica. En 1958 Gilmore, usando formas normales disyuntivas y los universos de Herbrand, logra dar demostraciones automáticas de fórmulas moderadamente complejas de lógica de primer orden sin igualdad como:

x y z [{<(Pyz [Qy Rx]) Pxx> <([Pzx Qx] Rz) Pxy>} Pzz]

Esta fórmula es una verdad lógica, es decir, la fórmula es verdadera independientemente de la interpretación que se haga de los predicados P, Q, y R, respecto a cualquier universo no vacío. Pero pocas personas la encontrarán obvia o trivial.

En 1958, Hao Wang, en una IBM, desarrolla programas que prueban 220 teoremas de Principia Mathematica y en 1960 Martin Davis y Hilary Putnam proponen un mejor algoritmo para fórmulas instanciadas en forma normal conjuntiva o forma clausular. Al final de estos primeros diez años de DAT, en 1965 J. A. Robinson publica su regla de resolución con unificación, lo cual genera un "boom" de la DAT.

Como conclusión de esta primera década, podemos decir que no sólo se dieron los primeros logros en DAT, sino que surgieron las ideas y métodos básicos de DAT que se desarrollaron en las décadas siguientes, sobre todo en los Laboratorios Argonne.

En 1980 Larry Wos propone el término "Razonamiento Automatizado" para reemplazar el más tradicional de "Demostración Automática de Teoremas".⁽¹⁾ Con ello quiere enfatizar que las búsquedas de solución no son ciegas y rutinarias, sino que puden involucrar planeación, ponderación, estrategias, etc.

Curiosamente, por la división entre hardware y software, hay pocas máquinas lógicas hoy día, si no contamos los avances en circuitos lógicos integrados o las máquinas japonesas especializadas para programación lógica. Es mucho más fácil encontrar lógica en software educativo, como lo demuestra una somera revisión de The Computers and Philosophy Newsletter o el Computerized Logic Teaching Bulletin.

La relación entre DAT y computadoras ha sido historicamente muy estrecha. Pero hay que precaverse contra la tentación de creer que la demostración mecánica necesita de máquinas inhumanas. Cualquier persona puede calcular mecánicamente, y es un error reducir la informática a la tecnología de las computadoras. Se dice que la ciencia de la computación tiene tan poco que ver con las computadoras como la astronomía con los telescopios. El uso de telescopios no significa que la astronomía se dedique a investigar la construcción y manejo de telescopios. Similarmente, la computadora ayuda a explorar el universo de la computación y el pensamiento mecánico, pero es sólo un instrumento para la ciencia general del procesamiento de la información. Hay que recordar que cuando el padre de la informática actual, Alan Turing, hablaba de "calculadoras" en los años treinta, se refería a personas. Computar es una actividad tan humana como mecánica, y aprendemos sobre nuestra propia mente al analizar sistemas computacionales.

1. ¿Para qué sirve la demostración automática?

Hay varias motivaciones para la investigación en DA, tanto teóricas como prácticas. Antes de dar ejemplos, digamos unas palabras sobre la concepción de la inferencia como búsqueda computacional. ¿Qué es la inteligencia? Principalmente (aunque no solamente), es poder encontrar soluciones a nuevos problemas. Los problemas pueden ser intelectuales, emocionales, prácticos. Pueden involucrar lenguaje, movimientos corporales, relaciones y acciones interpersonales. Hay personas que son inteligentes en lo que piensan pero cometen errores en lo que dicen o lo que hacen; que pueden conducir bien un auto, pero destrozan un matrimonio; que pueden escribir un informe pero no un poema; que pueden construír una teoría pero no una silla.

Hay muchos tipos de inteligencia, pero en todos hay una estructura básica: partimos de cierta situación o contexto al que hay que tomar en cuenta y buscamos la solución a un problema o dificultad. La situación es como (aunque no totalmente) una serie de premisas y la solución es como lo que deseamos extraer de ellas, la conclusión o teorema de ese sistema. Pero llegar a la meta exige encontrar un camino, un método, que nos lleve de la situación presente a la que deseamos. La búsqueda de ese camino es lo que desearíamos automatizar. Buscamos una automatización parcial de la inteligencia, tanto para probar que algo es verdadero, como para probar que algo es falso (refutar). No hay que olvidar que refutar es demostrar una negación. (Hay quienes se impacientan con los científicos y filósofos que refutan muchas cosas, sin darse cuenta que el reconocimiento de la ignorancia es el inicio de la sabiduría, pues siempre se aprende algo al refutar una falsedad.)

También es parte de la inteligencia reconocer cuando algo no puede ser alcanzado o demostrado de cierta manera. Por ello debemos complementar la DA con la generación de contraejemplos. La primera encuentra demostraciones y la segunda prueba que no se pueden encontrar. Es importante darse cuenta de que con simples multiplicaciones podemos calcular el área de rectángulos; también es importante darnos cuenta de que así no podemos calcular el área de círculos. Similarmente, con lógica proposicional podemos justificar el modus ponens pero no podemos justificar la regla de generalización existencial.

Cuando probamos que hay una demostración, lo que probamos es la inconsistencia de afirmar las premisas P y la negación de la conclusión C. En cambio, demostrar que no hay una demostración de C a partir de las premisas P significa que es consistente conjuntar la negación de C con P. Cada demostración puede ser vista como una prueba de inconsistencia y cada construcción de modelos como una prueba de consistencia.

Tanto la derivación o demostración de las conclusiones, como la creación de modelos en que las premisas son verdaderas pero la conclusión falsa, son relativas al sistema en que se construyen. Un sistema más poderoso eliminará modelos, y tal vez permita una demostración. Un sistema más débil perderá la posibilidad de demostrar algunas cosas. Pero, sin cambios en el sistema, lo que se prueba queda probado, y lo que se descubre que no se puede probar nunca se probará. En lo que sigue nos concentraremos en la búsqueda de demostraciones, no de modelos.

Otra motivación es la utilidad teórica. Mencionamos antes que la lógica es tanto un arte como una ciencia. Deseamos usar y entender los mecanismos para razonar mejor. La investigación sobre DA nos sirve para ambas cosas. La ciencia lógica se ha enriquecido enormemente al tratar de modelar e implementar sistemas para la mecanización de las inferencias, especialmente usando computadoras. Es sabido que uno entiende a veces mejor las cosas si se las explica a otro. Y mientras más tonto sea el otro, mayor claridad y precisión son necesarios para comunicarnos con exactitud. La computadora es una ayuda invaluable en este empeño. A menos que esté descompuesta, la máquina hace lo que le decimos que haga y nada más. Si las cosas no resultan como esperamos, sólo podemos culpar a nuestras instrucciones. Podemos dividir esta utilidad teórica en (1) uso de estrategias, (2) teoría de la complejidad, (3) lógicas computacionales y (4) solución de problemas abiertos.

Sobre el uso de estrategias, debemos considerar que dentro de la ciencia lógica, una parte fundamental es la teoría de la prueba. En ella analizamos las propiedades generales de los sistemas que modelan las demostraciones. Y la DA es el lazo que une a la ciencia de la demostración con el arte de las estrategias más eficientes para lograr demostrar algo. Cuando alguien propone una demostración X, la lógica puede examinarla como arte y como ciencia. Como ciencia, la pregunta fundamental es si X es verdaderamente una demostración, en qué sentido y qué tan correcta. Como arte, la pregunta es si X ejemplifica una estrategia eficiente y general, una estrategia que pueda aplicarse más a menudo y mejor que otras. Esta pregunta, de orden teórico, tiene importantes consecuencias prácticas y ha llevado a la exploración de estrategias que no se adaptan bien a las características humanas (limitada memoria, lentitud en el procesamiento) pero que se adaptan bien a las de las máquinas actuales (limitada capacidad estratégica, falta de sentido común).

Otra utilidad teórica es en el campo de la teoría de la complejidad. Cuando buscamos implementar sistemas computacionales que serán usados en el mundo real, no es suficiente saber que cierto problema tiene una solución en principio. Queremos saber qué tantos recursos y cuánto tiempo nos tomará obtener la solución. Esto ha dado un gran impulso a la teoría general de la complejidad computacional, es decir, el estudio del tipo u orden de los recursos que serán necesarios para resolver una clase de problemas con técnicas específicas.

También es útil el estudio de la DA para el desarrollo de lógicas computacionales. Necesitamos sistemas que tomen en cuenta que el valor de verdad de las proposiciones cambia continuamente y que hay propiedades formales importantes en los procesos, incluyendo la modificación, creación y destrucción de estados. Esto ha estimulado la creación de lógicas "dinámicas" y "lineales" que toman en cuenta el aspecto no estático que tiene el pensamiento en el mundo real.

Finalmente, estos estudios han reportado soluciones de problemas abiertos. Los sistemas para DA de teoremas no se han limitado a los teoremas conocidos. En matemáticas hay problemas que son muy difíciles porque antes de llegar a una conclusión hay que considerar todas las variantes posibles. Hay que generar todos los casos y checarlos uno por uno. Por ejemplo, el problema topológico de los cuatro colores requirió el uso de computadoras para examinar exhaustivamente todas las combinaciones relevantes. El problema era averiguar si 4 colores bastan para colorear cualquier mapa sin que ningún par de países vecinos tengan el mismo color. Se puede ver que 3 colores no son suficientes. Por ejemplo, si coloreamos Argentina, Bolivia, Brasil y Paraguay, necesitaremos 4 colores para que ningún par de vecinos tengan el mismo color. En México, necesitamos 4 colores para colorear Estado de México, Hidalgo, Puebla y Tlaxcala. Otra manera de formular el problema es preguntarse si puede haber cinco países compartiendo cada uno al menos algunos metros de frontera con cada uno de los otros. El lector puede divertirse tratando de imaginar un mapa con esos cinco países. El teorema de los cuatro colores, demostrado con ayuda de computadoras, dice que tal mapa no existe pues demandaría cinco colores diferentes, y cuatro son suficientes siempre. Hay muchos otros resultados nuevos en áreas como la geometría algebraica, teoría de redes, álgebra booleana, lógica combinatoria, teoría de grupos, álgebra de Robbins, etc. Es importante emfatizar que el campo de la DA no sólo ha sistematizado importantes estrategias de prueba útiles para las matemáticas, sino que incluso ha creado nuevos resultados y nuevos problemas.

Ahora bien, la utilidad de la DA no se limita al aspecto teórico. También tiene utilidad práctica en los campos de (1) verificación y síntesis de programas, (2) diseño y verificación de circuitos y (3) diseño y manejo de bases de datos.

Veamos primero su utilidad en la verificación y síntesis de programas. Vimos que encontrar una solución es como encontrar una demostración. La situación y la meta son como las premisas y la conclusión. Mientras mejor formulado esté el problema, más claro es el camino hacia su solución. Por ello, una aplicación natural de los métodos de DA es en el contexto de la generación de programas de computadora. Podemos expresar con relativa claridad los objetivos del programa, el comportamiento que se espera, y las condiciones de aplicación. Es decir, podemos tratar de escribir rigurosamente la entrada (input, situación inicial o premisas), la corrida (comportamiento del programa o derivación), y la salida (output, meta o conclusión). Nuestro objetivo puede ser producir el programa que necesitamos o, si ya lo tenemos construído, verificar que hace lo que se desea que haga.

Supongamos que deseamos un programa o rutina para pasar todos los objetos de A hasta B mediante la repetición de ciclos en cada uno de los cuales sustraemos un objeto de A y se lo agregamos a B hasta agotar A. ¿Cómo sabemos si nuestro programa funciona? Por ejemplo, podemos detectar invariancias. Sabemos que después de cada ciclo, si el método se sigue rigurosamente, el número de objetos en A decrece pero la suma de los objetos en A y B se mantiene constante. Esta invariancia permite descubrir casos en que el programa falla.

Otro uso práctico de la DA es en el diseño y verificación de los llamados circuitos lógicos. Sabemos desde hace décadas que las constantes lógicas como la conjunción, la disyunción y la negación tienen correlatos en los circuitos lógicos en serie, paralelo, e invertidores. Para ser verdadera, una conjunción necesita que ambos conyuntos sean verdaderos; análogamente, un circuito con dos tramos en serie necesita que pase la electricidad en ambos tramos para que pase en el circuito entero. Una disyunción sólo necesita la verdad de uno de los disyuntos, igual que un circuito en paralelo sólo precisa que pase electricidad en alguno de los tramos. Y la negación produce una oración con el valor opuesto, de manera análoga a un inversor eléctrico.

El comportamiento de los circuitos eléctricos es similar a las relaciones lógicas de las conectivas proposicionales. Podemos especificar el comportamiento en términos lógicos y automáticamente generar diseños de circuitos eléctricos que tengan las propiedades que deseamos. O, si ya tenemos el diseño, traducirlo al lenguaje lógico y verificar con técnicas lógicas si del diseño se derivan las propiedades que buscábamos. Todo esto sin tener que construír todavía un solo circuito. Y además de los circuitos lógicos, se pueden verificar otros circuitos. Por ejemplo, se ha producido una prueba completamente automatizada de la corrección de un circuito que implementa el estándar internacional (de la IEEE) para cálculos con punto flotante. Se han verificado también circuitos de tamaño comercial para adición y multiplicación y para sistemas de seguridad.

Finalmente, la DA es útil en el diseño y manejo de bases de datos. Una base de datos útil no es simplemente un montón inerte de informaciones. Aunque originalmente sólo sepamos que en el salón de clases hay 32 alumnas y 28 alumnos, estos datos pueden manipularse para obtener otros datos derivados: Hay más alumnas en ese salón, hay cuatro alumnos menos, el total son 60, etc. Una base de datos normalmente incluye una maquinaria inferencial que procesa la información y extrae otra información que sólo estaba implícita y dispersa en los datos inciales. Estas bases de datos son llamadas "deductivas", y la maquinaria inferencial puede utilizar sofisticadas técnicas de DA para extraer el conocimiento que necesitamos.

La lógica es importante en dos aspectos de las bases de datos. Por un lado, puede ser una guía para la representación concreta de datos. Por otro, puede ofrecer los mecanismos para especificar la información en abstracto que queremos manipular. Veamos primero la representación concreta dentro de la máquina: La información que añadimos a la base de datos puede estar escrita en una forma similar a la que normalmente empleamos en lógica, es decir, con una estructura oracional formada básicamente por nombres y variables de objetos, funciones, predicados, conectivas y cuantificadores. Para guardar la información de que Juan es hombre y María es mujer, representamos a Juan y a María como estructuras en la computadora, las enlazamos a sus predicados, y finalmente las conjuntamos mediante una función que produce oraciones complejas. En la computadora esto puede estar presente en registros (registers), ristras (arrays), apuntadores (pointers), etc., en una sintaxis que sigue a la de la lógica matemática clásica.

Pero este primer aspecto tiene dos cualificaciones. La primera cualificación es que este método de representar la realidad, aunque es el más común y el que normalmente encontramos en los lenguajes humanos, no es el único. Podemos tener lógicas combinatorias donde no hay objetos y propiedades sino únicamente "combinadores". Hay muchos tipos de lenguajes lógicos y rara vez se siguen completamente las estructuras del lenguaje natural.

La segunda cualificación es que la representación en la computadora comúnmente se divorcia de las estructuras lógicas y gramaticales. En sistemas coneccionistas los datos están "dispersos" en toda una red de asociaciones. Son los lazos entre los nodos, su fuerza, propiedades y direcciones, lo que contiene la información. Igual que parece ocurre dentro del cerebro humano, la representación dentro de una computadora puede carecer de signos lingüísticos a la usanza lógica.

El otro aspecto que mencionamos sobre la utilidad de la lógica para el estudio e implementación de bancos de datos era la representación abstracta de lo que queremos manejar. La información puede ser especificada, en un lenguaje de alto nivel, usando lógica clásica. En vez de usar el español o el inglés para definir lo que queremos que contenga nuestra base de datos, podemos usar el lenguaje usual de la lógica. Queda entonces claro que el objetivo al preguntar por algo a la base de datos es averiguar si se sigue lógicamente de los datos que se tienen a través de la maquinaria inferencial disponible. Las consultas a bases de datos pueden así verse como peticiones de demostración automática de teoremas (conclusiones del sistema).

1. Programación Lógica

La máquina inferencial puede tener reglas especiales de acuerdo a la base de datos a la que se va a aplicar. Los principios y reglas más generales, sin embargo, son los de la lógica clásica. Esto no es una limitación ya que los demostradores automáticos pueden usar otras lógicas subyacentes. Además de la lógica matemática clásica, hay lógicas probabilísticas, difusas, no-monotónicas, etc., sin contar los casos de sistemas expertos que usan "grados de confiabilidad" que implementan formas de inferencia difíciles de sistematizar. Cada sistema distinto ofrece ventajas y desventajas comparado con la lógica clásica. Por ejemplo, hay demostradores que siguen sistemas de lógicas relevantes. La ventaja es que el árbol de búsqueda se poda severamente si nos limitamos a considerar enunciados temáticamente pertinentes. La desventaja es que la lógica relevante es difícil de implementar eficientemente y tiene problemas de decidibilidad.

La programación lógica consiste en utilizar las reglas y principios lógicos que normalmente interpretamos como afirmaciones (una "semántica declarativa"), e interpretarlos como órdenes o comandos dados a la computadora (una "semántica procedural").

Es común confundir la programación lógica con los lenguajes en que se ha implementado. El lenguaje de programación en lógica más famoso es Prolog, desarrollado a principios de los setentas por Colmerauer en Marsella. Aunque limitado a las cláusulas Horn (básicamente, condicionales simples o anidados), es un lenguaje poderoso y práctico en el que podemos decirle a la computadora lo que deseamos, en vez de tener que especificar cómo lo deseamos. Desgraciadamente, tiene algunas propiedades que dificultan seriamente darle una semántica puramente declarativa, como el supuesto de mundo cerrado (closed world assumption, el supuesto de que ya tenemos toda la información pertinente), el comportamiento de la negación no como falsedad sino como fracaso del intento de demostración (negation as failure), y la orden de abandonar ciertas búsquedas, recortando (cut) el árbol de búsqueda.

1. Teorema Básico para pruebas por refutación

¿Cómo saber cuántos números primos hay? Revisar cada número es imposible. Aunque al poco tiempo los primos se van encontrando más y más espaciados, el que no encontremos un primo a pesar de revisar miles de números no prueba que el siguiente no esté a la vuelta de la esquina. Una prueba muy elegante de que siempre habrá más números primos es partir del supuesto de que hay un número finito y derivar una contradicción. Multipliquemos todos los primos. Aunque sean muchos, supusimos que el número de ellos es finito, así es que el resultado es un número natural. Añadiendo 1 al producto de la multiplicación de los primos, obtendríamos un número que no se divide exactamente por ningún primo (pues sobra 1). Pero eso significa que tenemos un nuevo número primo, contra nuestra hipótesis. Para probar que hay una cantidad infinita de números primos, hemos demostrado que negarlo nos lleva a una contradicción.

Del ejemplo anterior podemos sacar una moraleja. Usualmente, mientras más información tenemos, más fácil es llegar a la conclusión. Un truco muy útil para probar una conclusión a partir de una serie de premisas ₁,..., _n, es añadir algo más de información a esa serie. El truco es añadir la negación (¬) de lo que queremos probar y demostrar que ¬ es insostenible bajo el supuesto de ₁,..., _n. En otras palabras, si podemos reducir a un absurdo la opinión contraria a , entonces queda probada por eliminación. Hemos probado que es consecuencia lógica de la serie de enunciados ₁,..., _n. Eso se puede entender intuitivamente. Ahora tratemos de entenderlo rigurosamente.

¿Qué significa decir que cierto enunciado, al que podemos llamarle , es consecuencia lógica de una serie de enunciados ₁,..., _n? Quiere decir que esa serie de enunciados hace que sea necesario. Por supuesto, no tiene que ser necesario en sí mismo, sino tan sólo necesario para el supuesto de que ₁,..., _n contiene sólo verdades. Esta relación la simbolizamos como "₁,..., _n ". En otras palabras, estamos diciendo que es imposible que la serie ₁,..., _n tenga sólo miembros verdaderos pero sea falsa. No hay manera (no hay modelo) en que esto ocurra. En lógica clásica esto significa que la persona que sostuviera ₁,..., _n junto con ¬ se estaría contradiciendo a sí misma, estaría siendo inconsistente.

Lo diremos todavía más técnicamente: Sean ₁,..., _n, enunciados de un lenguaje L de primer orden con igualdad. Entonces,

() ₁,..., _n si y sólo si {₁,..., _n, , ¬} es inconsistente (no tiene modelo).

Para demostrar esta equivalencia basta mostrar que si suponemos la parte de la izquierda ("₁,..., _n ") tenemos que aceptar también la de la derecha ("{₁,..., _n, , ¬} es inconsistente") y viceversa. Empezaremos de izquierda a derecha.

() Empezamos suponiendo el lado izquierdo, es decir, que toda interpretación que haga verdaderos a todos los elementos de la serie ₁,..., _n tiene que hacer verdadero a . Eso es lo que significa el símbolo "". En nuestra lógica clásica, para interpretar a ¬ como verdadero hay que interpretar a como falso. Entonces, no es posible que haya una interpretación que haga verdaderos a todos los enunciados de la serie ₁,..., _n, y también a ¬. O, para decirlo técnicamente, no hay modelo para el conjunto {₁,..., _n, , ¬}.

() Ahora demostraremos la equivalencia de derecha a izquierda. Partimos esta vez de suponer que no hay una interpretación posible que haga verdaderos a todos los enunciados de la serie ₁,..., _n,,¬. Pero, cada interpretación determina un valor para cada enunciado de L, dando algún valor de verdad a ¬ y el opuesto a . Entonces, cualquier interpretación que haga verdaderos a los enunciados en ₁,..., _n,, tiene que hacer verdadero a .

Con esto tenemos las dos direcciones de la equivalencia. Como nuestra afirmación ha sido demostrada podemos llamarla un "teorema". De hecho, este es el teorema básico para pruebas por refutación.

1. Unificación mediante substitución

Hay una antigua broma del tiempo de los griegos clásicos que consiste en preguntarle a alguien, digamos Nikolás, si cree que todavía tiene lo que no ha perdido. Nikolás responde que sí, que lo que no se ha perdido todavía se tiene. Entonces se le pregunta si ha perdido cuernos. Nikolás confiesa que no ha perdido cuernos, y se da cuenta de que está forzado a admitir que todavía los tiene.

Lo que tenemos en este ejemplo es una proposición de la forma: Cualquier persona p tiene toda cosa c que no haya perdido. Nikolás es una persona, y no ha perdido cuernos. Así es que unificando la variable p con "Nikolás", y la variable c con "cuernos", podemos sacar conclusiones en detrimento del pobre Nikolás.

Igualmente, examinemos una proposición como "La vida no tiene sentido". A pesar del artículo definido "la", es claro que estamos hablando de cualquier vida, presente, pasada o futura, no de una en especial. Puede ser parafraseado como "Cualquiera vida v no tiene sentido". Esto habla, entre otras, sobre la vida de usted, y la mía, y la de Mahatma Gandhi. Se concluye de ese punto de vista tan pesimista que "La vida de Gandhi no tiene (o tuvo) sentido". Llegamos a la conclusión dándonos cuenta de que podemos unificar la variable v con "la vida de Mahatma Gandhi". El proceso de unificación permite identificar diferentes proposiciones reemplazando variables como p, c y v mediante las substituciones adecuadas.

El reto de la unificación es encontrar valores para las variables que hagan a dos expresiones idénticas. Podemos ver a la substitución que buscamos como un conjunto de parejas en las que el primer término es la variable a substituír y el segundo término es aquello con lo que se va a substituír la variable. Por ejemplo, una substitución, llamémosle , podría ser{p/Nikolás, c/cuernos}. Al resultado de aplicar la substitución , sobre una fórmula lo representamos como y decimos que es un posible unificador: unifica a y a si y sólo si = . Por supuesto, cualquier fórmula se unifica consigo misma mediante el unificador vacío {} que es una substitución vacua.

En nuestro segundo ejemplo, reemplazamos la frase original "La vida no tiene sentido" por algo menos general como "La vida de Gandhi no tuvo sentido". Decimos que la fórmula primera subsume a la segunda que es más específica. En general, dada una substitución , cualquier fórmula subsume a , es decir, subsume al resultado de aplicar la substitución a . Si no tiene variables o es vacía o no tiene variables en común con , esta subsunción es vacua porque no cambia. Por supuesto, podemos substituír unas variables por otras. Por ejemplo, con {x/y} convertimos a "Juan es un x" en "Juan es un y", pero es claro que lo único que hemos hecho es una variante. Decimos que A es variante de B si y sólo si A subsume a B, pero también B subsume a A. En cambio, A subsume propiamente a B si y sólo si A subsume a B pero no al revés.

Desde el punto de vista lógico, lo importante es que de podemos inferir, entre otras cosas, todo lo que subsuma. Todo lo que obtenemos por unificación a partir de un conjunto de proposiciones, queda tan demostrado como mismo. Por eso Nikolás se comprometió a que tenía cuernos desde el momento que dijo que tenía todo lo que no había perdido.

Recordemos que una fórmula implica a cualquier fórmula ( v ). Al añadir alternativas decimos lo mismo o menos que la fórmula original. Por ello subsume a ( v ). Podemos generalizar la noción de subsunción de la siguiente manera:

Sean A y B disyunciones cuyos disyuntos representamos respectivamente como Dis(A) y Dis (B).. Decimos que A subsume a B si hay una sustitución tal que Dis(A) Dis(B). Es decir, si todas las literales de A bajo se convierten en literales de B.

Ejemplos: Q(x) subsume a Q(c) R(y)

Q(a) R(y) subsume a P(x) Q(a) R(c)

P(x) P(f(x)) subsume a P(f(y)) P(f(f(y)))

Intuitivamente una disyunción subsume a otra cuando contiene ya toda la información de un disyunto o parte disyuntiva de la otra por lo que, siendo ambas disyunciones, la implica lógicamente. Obsérvese también que la subsunción es una relación transitiva. Así, la relación de subsunción permite eliminar disyunciones redundantes por ser disyunciones ya subsumidas. Esto permite tener un operador de subsunción Sub para conjuntos de disyunciones de modo que, si S es un conjunto de disyunciones, Sub(S) sea un subconjunto de S en el que no haya disyunciones subsumidas por otras.

Para que el resultado sea único, podemos definir a Sub(S) como el subconjunto de S producido de la siguiente manera: siguiendo el orden alfabético de las disyunciones de S (se podría usar otro orden), eliminamos todas las disyunciones subsumidas por la primera disyunción. A continuación eliminamos todas las subsumidas por la siguiente disyunción de entre las que queden, etcétera. El resultado es un conjunto único Sub(S) en el que ninguna disyunción es subsumida por otra de Sub(S). Obsérvese que todo modelo de S es también modelo de Sub(S) e inversamente porque solamente se ha limpiado a S de material redundante (si lo había).

Sobre la unificación, es importante notar que a veces no hay un unificador y a veces hay varios. Por ejemplo, no hay manera de unificar "Juan es un x" con "María es una y". En cambio, hay varias combinaciones para unificar "Juan es un x" con "Juan es un y". Por ejemplo, {x/y} que produce "Juan es un y", {y/x} que produce "Juan es un x", y {x/hombre, y/hombre} que produce "Juan es un hombre". Normalmente es preferible no usar la tercera unificación porque ya está subsumida en las anteriores. Es mejor obtener la conclusión más general posible porque después podemos instanciarla como mejor convenga. Por ello, usamos la noción de unificador más general, es decir, la combinación que en este caso produce el resultado más general posible (no subsumido propiamente por el producto de otra unificación sobre las mismas fórmulas). Siempre que haya un unificador, habrá un único unificador más general (o varios de ellos, variantes cada uno de los otros).

Para regresar al ejemplo de Nikolás, teníamos que unificar dos oraciones: "Nikolás no ha perdido x", y "p no ha perdido c". La cuantificación universal implícita en "Nikolás no ha perdido x" nos dice que Nikolás no ha perdido nada. Al especificar que tiene cuernos estamos perdiendo información, pues Nikolás se ha comprometido a que todavía tiene todo y ésta es la conclusión más general. Así, aunque un unificador sería {p/Nikolás, c/cuernos, x/cuernos}, éste no es el unificador más general. Si usamos {p/Nikolás, c/x}, podemos tener la premisa general "Nikolás no ha perdido x", y obtener de ella la conclusión general "Nikolás todavía tiene x", sin importar qué sea x.

Veamos ahora un método para usar nuestras unificaciones. Se llama "resolución".

1. Resolución

Contaban los griegos que cuando un perro llega a una bifurcación persiguiendo a una presa, olfatea uno de los caminos y, si no encuentra el rastro, se lanza por el otro camino sin detenerse a olfatearlo. La idea es que el perro hace instintivamente un silogismo disyuntivo: la presa se fue por uno de los dos caminos; no se fue por el primero, así es que debió irse por el segundo. Esto lo podemos simbolizar

A B

¬A

______

B

y puede generalizarse a casos como

A B

¬A C

________

B C

o

A B ¬D

¬A C ¬E

________________

B C ¬D ¬E

A las disyunciones donde cada disyunto es una letra o una letra negada, las llamamos cláusulas y a las letras o letras negadas las llamamos literales. Así pues, una cláusula es una disyunción de literales. Como puede verse, un par de disyuntos que aparecen con la misma letra afirmada y negada se eliminan y se concluye la disyunción de todos los demás en la conclusión o cláusula resolvente. La razón es que algún otro de los disyuntos debe ser verdad, ya que A es afirmada en una de las premisas o cláusulas padres y negada en la otra.

La regla de resolución nos permite hacer todas las inferencias de este tipo:

L Q₁ ... Q_m

¬L R₁ ... R_n

________________________

Q₁ ... Q_m R₁ ... R_n

¿Qué pasa en el caso especial de tener como cláusulas padres a L y ¬L? El resultado es que no queda ningún disyunto. Esto lo llamamos la cláusula vacía , y como nos quedamos sin alternativas, no hay forma de que sea verdadera. Es decir, es una contradicción y el conjunto original de premisas queda refutado si puede resolverse en la cláusula vacía.

Hasta aquí la regla de resolución es una simple generalización del silogismo disyuntivo que ejecuta, si hemos de creer a los griegos, hasta un perro. Pero esto se vuelve más interesante al formular la regla para admitir sustituciones. Por ejemplo, si aplicamos a las cláusulas padres (Pxf(x) ¬Qxy ¬Ry) y (¬Paz ¬Rz) la sustitución {x/a, z/f(a)}, obtenemos por unificación (Paf(a) ¬Qay ¬Ry) y (¬Paf(a) ¬Rf(a)). Con esto, podemos resolver a ¬Qay ¬Ry ¬Rf(a).

Escribamos esto con más precisión. Si L es una literal entonces L^c denota la literal "de signo contrario"; es decir, si L=P entonces L^c = ¬ P y si L = ¬ P entonces L^c = P. Robinson propuso que, si C y D son cláusulas sin variables en común, y L y M son disyuntos de C y D respectivamente tales que µ es el unificador más general (umg) de L^c y M, entonces la fórmula E F (donde E es idéntica a µC, excepto por carecer del disyunto µL y F es idéntica a µD, excepto por carecer del disyunto µM) es un resolvente de C y D. Esquemáticamente:

C D

---------------------------

(µC-µL) (µD-µM) (µ es el umg de {L^c, M})

Ejemplo: Si C=Q(x,b) P(z,a) y D = ¬ Q(a,w) R(w,b) entonces E = P(z,a) R(b,b) es un resolvente de C y D, y el umg es µ ={x/a,w/b}. Esquemáticamente:

Q(x,b) P(z,a) ¬ Q(a,w) R(w,b)

-------------------------------------------------------

P(z,a) R(b,b) µ ={x/a,w/b} es el umg de

{Q(x,b)^c, ¬ Q(a,w)}.

Ejemplo: Si C = P(b) R(f(a)) y D = ¬ P(y) ¬ Q(g(y)) entonces el resolvente bajo µ ={y/b} es E = R(f(a)) ¬ Q(g(b)). Esquemáticamente:

P(b) R(f(a)) ¬ P(y) ¬ Q(g(y))

-------------------------------------------------------

R(f(a)) ¬ Q(g(b)) µ ={y/b} es el umg de

{P(b)^c, ¬ P(y)}.

La regla de resolución binaria con sustitución es correcta. Es decir, al aplicarla el resolvente es una consecuencia lógica de las premisas. Sin embargo, no hay garantía de poder derivar cualquier consecuencia lógica directamente; en este sentido no es completa. Aun así, la resolución es una regla que cumple ser refutación completa: si se tiene un conjunto inconsistente de cláusulas, entonces, aplicando resolución, necesariamente hay algún camino para llegar a la cláusula vacía .

METATEOREMA (de Loveland): Si K es un conjunto de cláusulas de un lenguaje de primer orden con igualdad, entonce K es inconsistente si y sólo si hay una deducción de la a partir de K usando unicamente resolución.

COROLARIO: Si es teorema a partir de ₁, ..., _n (dicho en símbolos, ₁, ..., _n ), podemos demostrarlo con el siguiente procedimiento de DA:

1. Negar .

2. Formar el conjunto K = {¬, ₁, ..., _n} en forma clausular.

3. Aplicar pasos de resolución a K hasta obtener .

Por ejemplo, supongamos que deseamos hablar sobre varios hermanos: Juan, Jorge, Jesús, Javier y Jaime, todos ellos hijos de los mismos padres. ¿Podemos decir que la relación de ser hermano es transitiva? Es decir, si A es hermano de B, y B es hermano de C, entonces ¿A es hermano de C? Nótese que A, B y C pueden ser nombres de cualesquiera de los hermanos, incluso repetidos. Por ejemplo, {A/Juan, B/Jorge, C/Jaime}, o {A/Javier, B/Jesús, C/Javier}.

La respuesta intuitiva es que la relación de ser hermano es transitiva: se es hermano de los hermanos de nuestros hermanos. Pero un poco de reflexión demuestra que esto no es así. Sabemos que uno es hermano de sus hermanos (simetría). Pero nadie es hermano de sí mismo (anti-reflexividad). El problema es que la reflexividad se sigue de la simetría y la transitividad en conjuntos donde cada uno de sus elementos tiene la relación con alguien o alguien con él, es decir, donde no hay "puntos aislados". Demostraremos este pequeño teorema usando resolución con sustitución:

TEOREMA: Si una relación R es simétrica, transitiva y sin puntos aislados, entonces R es reflexiva.

Primero escribimos rigurosamente las premisas y la conclusión:

R es simétrica: x y (Rxy Ryx)

R es transitiva: x y z [(Rxy Ryz) Rxz]

R no tiene puntos aislados: x y (Rxy Ryx)

R es reflexiva: x Rxx

Por el Teorema Básico para pruebas por refutación que vimos antes, la conclusión se sigue de las premisas si y sólo si no hay modelo (es inconsistente) el siguiente conjunto de afirmaciones:

{x y (Rxy Ryx), x y z [(Rxy Ryz) Rxz], x y (Rxy Ryx), ¬x Rxx}

es decir, las premisas junto con la negación de la conclusión. Poniendo eso en forma clausular, lo que investigaremos es si no hay modelo (si es inconsistente) el siguiente conjunto:

CL = { [¬Rxy Ryx], [¬Rwu ¬Ruv Rwv], [Rzf(z) Rf(z)z], [¬Rcc]}.

En un momento explicaremos como encontrar la forma clausular de cualquier oración de lógica de primer orden. De momento baste enunciar el

METATEOREMA (de Skolem): Un conjunto de enunciados de lógica de primer orden con igualdad es consistente si y sólo si el conjunto de las formas clausulares de ellos es consistente.

Demostraremos ahora que no es consistente el conjunto CL derivando de él la cláusula vacía mediante tan sólo la regla de resolución con substitución:

A las cláusulas [¬Rxy Ryx] y [Rzf(z) Rf(z)z] les aplicamos la substitución {x/c, y/f(c), z/c} que nos da [¬Rcf(c) Rf(c)c] y [Rcf(c) Rf(c)c]. Resolviendo, tenemos Rf(c)c Rf(c)c, que es lógicamente equivalente a Rf(c)c a secas. Dicho en español, hay un hermano f(c) para c (elemento de nuestro dominio de hermanos), pues todos tienen algún hermano y la relación es simétrica (va para los dos lados o para ninguno).

Rf(c)c permite resolver con ¬Rxy Ryx una vez que aplicamos la substitución {x/f(c), y/c} y obtenemos Rcf(c). En español, c es hermano de f(c). No se confunda con la afirmación complementaria anterior, Rf(c)c, de que f(c) es hermano de c.

Ahora podemos usar la cláusula [¬Rwu ¬Ruv Rwv], transformada mediante la substitución {w/c, u/f(c)} en [¬Rcf(c) ¬Rf(c)v Rcv]. Nótese que no sustituímos todavía la "v". Por resolución con Rcf(c), tenemos ¬Rf(c)v Rcv. Dicho más claramente, la transitividad nos lleva a que si f(c) es hermano de v, c lo es también.

La v en ¬Rf(c)v Rcv podría sustituírse con {v/c} dándonos ¬Rf(c)c Rcc. Es decir, como acabamos de decir que si f(c) es hermano de v, c lo es también, lo aplicamos al caso en que v es c: cuando f(c) es hermano de c, c también es hermano de c, es decir, ¡hermano de sí mismo!

Esta disyunción ¬Rf(c)c Rcc se resuelve con la negación de la conclusión que era ¬Rcc (negar que la reflexividad se siga). Pero esto arroja ¬Rf(c)c, que contradice Rf(c)c, que fue la primera inferencia que obtuvimos. Tenemos algo y su negación por lo que obtenemos mediante resolución la cláusula vacía que buscábamos.

Este ejemplo muestra el potencial de la resolución con substitución como regla de inferencia. No es de asombrarse que la resolución sea la regla fundamental detrás de la maquinaria inferencial de Prolog, el lenguaje de programación lógica mencionado más arriba, así como del demostrador automático Otter ("nutria", en español) que utiliza con eficiencia la lógica de primer orden con igualdad, resolución (incluyendo variantes) y reducción al absurdo.

1. Forma Clausular

Para aplicar resolución es útil poner nuestra información en una forma fácil de manipular, una forma llamada forma clausular canónica. Podemos ver nuestra información inicial como la conjunción de diferentes hipótesis o condiciones. Por ello, es conveniente reescribir el conjunto de las premisas como la conjunción de varios condicionales materiales, es decir, una conjunción de disyunciones. (A esto se le llama Forma Normal Conjuntiva.)

Para empezar, hay que notar que una misma variable puede usarse en varias oraciones. Es mejor dar a cada oración sus propias variables, lo que llamamos estandarizar. Por ejemplo, "Todo cambia" y "Todo termina" pueden escribirse como "Para toda x, x cambia" y "Para toda x, x termina", pero es mejor reescribir la segunda oración como "Para toda y, y termina". Así podemos hacer substituciones uniformes de las x que cambian sin afectar a lo que decimos sobre las que terminan. Incluso si las x están en la misma oración, como en "Toda x cambia y alguna x termina" son diferentes cuantificaciones y es mejor reemplazarlas por diferentes variables como "Toda y cambia y alguna z termina". (Para un ejemplo práctico, véase la sección sobre unificación y trátese de unificar "Nikolás no ha perdido x" con "x no ha perdido cuernos"; es imposible hacer la unificación antes de estandarizar.)

Acto seguido procedemos a eliminar cuantificadores existenciales. Este proceso es llamado skolemización en honor del gran lógico Thoralf Skolem.⁽²⁾ Es conveniente pasar todos los cuantificadores al inicio de la oración para ver con claridad su tipo (un universal negado es realmente un existencial; un existencial como antecedente funciona realmente como un universal, etc.). Esto puede hacerse mecánicamente de varias maneras y el resultado es una forma prenex de la oración original.

Otra ventaja de la forma prenex es que con ella podemos ver fácilmente cuáles cuantificadores están dentro del alcance de cuáles. No es lo mismo decir que todo pueblo adora a algún dios a decir que hay algún dios adorado por todo pueblo. El dios del pueblo otomí puede ser diferente del dios del pueblo tibetano. Los existenciales ("algún", "cierto", "al menos un") dependen de los universales dentro de cuyo alcance viven. Todo alumno tiene alguna cabeza pero esa cabeza es la de cada alumno especial. Por ello, al skolemizar tenemos que sustituír las variables existenciales por funciones que dependan de las variables universales dentro de cuyo alcance estén. La frase "Todo p adora a algún d" se convierte en "p adora al dios-de(p)". La función "dios-de" permite eliminar el existencial "algún" sin perder la dependencia del cuantificador universal previo; no se adora a algún dios a secas, sino al que corresponde a p.

Después de haber standarizado las variables, prenexado los cuantificadores y skolemizado la fórmula. Podemos borrar los cuantificadores universales, como cuando decimos en álgebra que (x + y) = (y + x): no necesitamos decir explícitamente que hablamos de todo x y todo y de nuestro universo de discurso. Tenemos ahora una oración que podemos manejar con cálculo proposicional y poner en forma normal conjuntiva: conjunciones de disyunciones de literales (recuérdese que una literal es una fórmula atómica o su negación). Podemos enunciar ahora el siguiente metateorema sobre la transformación a forma clausular:

METATEOREMA: Toda fórmula de un lenguaje de primer orden con igualdad se puede transformar a una forma clausular cl() por medio de un algoritmo.

Esto es importante por el metateorema de Skolem que habíamos mencionado más arriba:

METATEOREMA: es consistente si y sólo si cl() lo es. En general, el conjunto {₁, ..., _k} es consistente si y sólo si {cl(₁), ..., cl(_k)} lo es.

Por lo tanto, no necesitamos buscar estrategias de refutación para cualquier tipo de fórmulas. Basta buscarlas para las que están ya "limpias" en forma clausular, sin preocuparnos por complicaciones como cuantificadores, condicionales, equivalencias, o fórmulas anidadas de maneras sorpresivas. Demos un ejemplo con un cuento. Considere la siguiente historia:

Hubo una vez un hombre tan cascarrabias que durante casi toda su vida nunca alabó a nadie, ni siquiera a sí mismo. En su lecho de muerte profirió por primera y única vez una alabanza: "Alabo a aquellos que no se alaban a sí mismos". Y murió en el acto.

¿Es esta historia posible? No; la historia dice que el hombre profirió una alabanza pero es lógicamente imposible que alguien profiera sólo esa alabanza: "Alabo a aquellos que no se alaban a sí mismos". La razón es que esa frase es paradójica, semánticamente indeterminada y por ende no es una alabanza en realidad, aunque suene como si lo fuera. Efectivamente, profirió sonidos que parecieron una alabanza, pero no lo eran.

Para entender por qué es imposible alabar a todos y sólo a aquellos que no se alaban a sí mismos, basta percatarse que ese hecho haría verdad que el hombre alabó exactamente a aquellos que no se alabaron a sí mismos, es decir, para cualquier x, [Alabó(h, x) si, y sólo si, No Alabó (x, x)]. Si esa proposición universal fuera verdad, sería verdad la instancia [Alabó(h, h) si, y sólo si, No Alabó (h, h)]. Ahora bien, ¿es verdad que el hombre de nuestra historia se alabó a sí mismo exactamente en caso de que no lo hiciera? Eso es una contradicción pues si le alcanza su propia alabanza entonces no debe incluírsele entre aquellos a los que el moribundo se refería, y si no le alcanza, entonces debiera alcanzarle. Ya que esa instancia es imposible, la generalización es imposible también (no, la excepción no confirma la regla).

Los instruidos en lógica reconocerán que esto es una variante más de la paradoja de Russell, que destruyera hace un siglo la teoría ingenua de conjuntos y el programa logicista fregeano. Es una lástima, porque efectivamente aquellos que no se alaban a sí mismos son dignos de alabanza. Y sólo ellos...⁽³⁾

La simbolización puede ser: No hay y tal que para cualquier x, [Alabó(y, x) si y sólo si, No Alabó (x, x)]. Dicho más rigurosamente, ¬y x [A(y, x) ¬A(x, x)]. Podemos ahora transformar esto a forma clausular y demostrarlo mediante resolución con substitución: ¬y x [A(y, x) ¬A(x, x)] es una verdad lógica si y x [A(y, x) ¬A(x, x)] no tiene modelo, es decir, skolemizando con y por h y obteniendo la forma clausular, si [¬A(h,x) ¬A(x,x)] [A(x,x) A(h,x)] no tiene modelo.

Instanciando la x como [¬A(h,h) ¬A(h,h)] [A(h,h) A(h,h)] podemos resolver los conyuntos en ¬A(h,h) y A(h,h) que a su vez se resuelve en . QED.

Mencionamos antes una fórmula de Gilmore demostrada automáticamente hace cuarenta años:

x y z [{<(Pyz [Qy Rx]) Pxx> <([Pzx Qx] Rz) Pxy>} Pzz]

La fórmula de Gilmore tiene una versión más breve y más fuerte de la que se obtiene fácilmente: x y z [{<(Qy Rx) Pxx> (Qx Rz)} Pzz] pues la parte cuantificada de la fórmula de Gilmore puede ser vista como {<(A [B C]) D> <([E F] G) H>} I, que se sigue de {<(B C) D> (F G)} I, que corresponde a nuestra versión. Piénsese en que ( ) implica a y esto a ( ).

Aunque es más fuerte, nuestra versión puede ser más fácil de entender. Ya que (B C) D es equivalente a (¬B D) (C D), tenemos que la fórmula de Gilmore será un teorema si x y z [{<(¬Qy Pxx) (Rx Pxx)> (Qx Rz)} Pzz] lo es.

Para reducción al absurdo, supongamos la falsedad de la fórmula simplificada, es decir, la verdad de: x y z [{<(¬Qy Pxx) (Rx Pxx)> (Qx Rz)} ¬Pzz]. Esta fórmula contiene 4 conyuntos:

(1) ¬Qy Pxx, es decir, Qy Pxx

(2) Rx Pxx, es decir, ¬Rx Pxx

(3) Qx Rz, es decir, ¬Qx Rz

(4) ¬Pzz

Entonces debe haber alguna y a la que Q se aplique, para evitar conflicto entre el conyunto 4 y el consecuente del 1, pues si el antecedente de 1 fuera siempre falso, toda x cumpliría Pxx, y no quedaría una z para satisfacer 4. Tomando un individuo al que Q se aplique, tenemos (por el conyunto 3) que R se aplica a una z que tiene la relación P consigo mismo (por 2) pero no la tiene (por 4). Eso es un absurdo, por lo que nuestra fórmula simplificada debe ser una verdad lógica.

Otra manera de ver esto es skolemizando la variable "y" como fx, y la variable z como gx. Ahora instanciamos la x de la siguiente manera:

Pero las instanciaciones (¬B), (AB), (¬A C), (¬D) y (¬C D) no pueden ser simultáneamente verdaderas. Nuestro supuesto original (de que la fórmula simplificada puede ser falsa) nos lleva a una contradicción mediante una sequencia clara de resoluciones. Para un humano es difícil encontrar las combinaciones adecuadas, o incluso buscarlas para probar fórmulas poco intuitivas.

Nos hemos detenido en los detalles de estas demostraciones de la fórmula de Gilmore (¡en su forma simplificada!) para dramatizar el hecho de que la DA nos ofrece desde hace décadas nuevos conocimientos lógicos.

1. Otras reglas de inferencia

La regla de hiperresolución es una macroinferencia basada en la regla de resolución, cuyo objetivo es producir una cláusula positiva (llamada hiperresolvente) a partir de una sucesión de varias cláusulas, una de ellas negativa⁽⁴⁾ o mixta (llamada núcleo) y todas las demás positivas (llamadas satélites o electrones). La regla de hiperresolución obtiene el hiperresolvente "de un golpe" pero para entender que lo que hace es equivalente a una serie de resoluciones, veremos a éstas en serie: en la cláusula núcleo (negativa o mixta) se resuelve primero la literal negativa de la extrema derecha con el primer satélite, luego el resolvente de ellas con el segundo satélite, y así sucesivamente. Debe haber tantos satélites como literales negativas en la cláusula núcleo. El último resolvente obtenido del penúltimo resolvente y del último satélite, es el hiperresolvente del sistema.

Ejemplo:

Núcleo= Padre(y,z) ¬ Madre(x,z) ¬Casado(x,y)

Satélite₁= Casado(Tere,Pedro) Masviejo(Tere,Pedro)

Satélite₂= Madre(Tere,Sergio)

Hiperresolvente= Padre(Pedro,Sergio) Masviejo(Tere,Pedro)

El unificador es µ ={x/Tere, y/Pedro, z/Sergio}.

Un operador de refinamiento de resolución R_x, como es la hiperresolución, puede pensarse como una máquina inferencial que generaliza la resolución y que recibe como entrada un conjunto de cláusulas y da como salida toda la información que se pueda obtener de él mediante alguna inferencia basada en resolución.

Un operador de refinamiento de resolución R_x es completo si para cualquier conjunto de cláusulas S, S es no satisfacible si y sólo si R_x(S). Por ejemplo, el operador de hiperresolución es completo.

La idea para la prueba por refutación, basada en refinamientos de resolución (como el operador de hiperresolución), es la siguiente: dado un conjunto de cláusulas S, el cual queremos demostrar que no tiene modelo y un operador de refinamiento de resolución R_x que sea completo, calcular R_x(S); si la cláusula vacía pertenece a R_x(S), es decir, R_x(S), entonces S no puede tener modelo (es no satisfacible). Este tipo de resultados así como su decidibilidad efectiva ha sido estudiado con gran detalle dentro del razonamiento automático (véase por ejemplo [Miranda]). Por otra parte, si R_x(S), por la completud se sigue que S sí tiene modelo (es satisfacible).

Otra regla importante es la de paramodulación. La regla de paramodulación combina el reemplazo de variables con la sustitución de igualdades.

Denotamos como C[t] a una cláusula C donde hay presencias del término t. Usaremos t, r, s para denotar términos del lenguaje (con variables o sin variables). C puede tener igualdades o incluso puede ser una sola igualdad. Si es una sustitución que "unifica" a t y r, podemos formular la regla de paramodulación así:

C[t]

r = s

______

C[s]

"r = s" es llamado el paramodulador y s denota el resultado de aplicar la substitución al término s.

Si existe alguna substitución que unifique a t y a r, t = r. Lo que hace la paramodulación es instanciar la primera premisa como C[t], la segunda como r = s, y hacer la substitución de t por s. Cuando la substitución es vacua, la paramodulación se colapsa en la sustitución ordinaria de iguales, pero puede ir más allá y producir cláusulas que no podrían obtenerse por la sustitución ordinaria sin las instanciaciones permitidas en esta regla compleja.

He aquí un ejemplo: Sabemos que cualquier padre es más viejo que sus hijos. Simbolizando esto, tenemos que MásViejo(padre(x), x). Supongamos que el padre de Jaime se llama Rodolfo. Esto lo simbolizamos Padre(jaime) = rodolfo. Esta identidad es llamada el "paramodulador". Es obvio que podemos concluír que MásViejo(rodolfo, jaime). La conclusión se justifica con la substitución = {x/jaime}. A la conclusión la llamamos la cláusula paramodulada.

Otro ejemplo: Supongamos los axiomas de grupo y deduzcamos la ley de cancelación. Los axiomas de grupo son tres: asociatividad de la operación, la existencia de un neutro para la operación, llamado "e", y la existencia para cada x de un inverso para la operación llamado g(x). En el lenguaje formal,

1. (xy)z = x(yz)

2. xe = x

3. xg(x) = e

Por ejemplo, si la operación xy se entiende como x+y en el dominio de los números reales, el axioma 1 se cumple porque la suma es asociativa. En el axioma 2, e es el 0 (el elemento "neutro" del grupo). En el axioma 3, g(x) es -x (el "inverso" de x). Nótese que no podríamos aceptar los axiomas si la operación se entiende como x • y. Aunque el axioma 1 se sigue cumpliendo porque la multiplicación también es asociativa, y en el axioma 2 e puede ser el 1, el axioma 3 falla. Lo natural sería tomar g(x) como 1/x, pero g no estaría definida para 0: g(0) = 1/0 no está en el dominio de los números reales.

De los tres axiomas se deduce la ley de cancelación: (xy = zy) x=z. Por ejemplo, si x+y es igual a z+y, entonces x=z. Nótese que si x • y es igual a z • y, no se sigue que x=z. Aunque 4 • 0 es igual a 7 • 0, eso no hace que 4 = 7. La ley de cancelación es una propiedad importante.

La demostración puede verse como una serie de paramodulaciones. Añadimos a los tres axiomas la negación de la ley de cancelación y mostramos que lleva a una contradicción, es decir, a una cláusula vacía. La negación de la ley de cancelación consiste en afirmar que, para algunos objetos a, b y d, se cumple el antecedente pero no el consecuente. Simbólicamente:

4. ba = da

5. ¬(b = d)

Empezamos con la identidad trivial de que

(ba)g(a) = (ba)g(a)

Ahora paramodulamos el lado derecho de la igualdad con (4) y la substitución vacua ₁ = {} para obtener

(ba)g(a) = (da)g(a)

Esto puede ser paramodulado del lado izquierdo por el axioma 1 mediante la substitución ₂ = {x/b, y/a, z/ga}. Es fácil checar que obtenemos

b(ag(a)) = (da)g(a)

cuyo lado izquierdo se paramodula nuevamente con el axioma 3 mediante ₃ = {x/a} para dar

b(e) = (da)g(a).

Como e es el neutro, podemos paramodular con el axioma 2 mediante ₄ = {x/b} y tener

b = (da)g(a).

Cambiamos de lugar los paréntesis del lado derecho paramodulando con el axioma 1 y la substitución ₅ = {x/d, y/a, z/g(a)} y se produce

b = d(ag(a))

El axioma 3 paramodula el lado derecho con ₆ = {x/a} y rinde

b = d(e)

a lo que aplicamos el axioma 2 paramodulando con ₇ = {x/d} para conseguir

b = d.

Como esto es negado por 5, ¬(b = d), una simple resolución nos da la cláusula vacía que buscábamos.

1. Estrategias de inferencia

Además de buenas reglas para inferir, un demostrador automático necesita buenas estrategias para aplicar las reglas. A veces es necesario impedir que el demostrador pierda su tiempo haciendo inferencias que tienen poca probabilidad de llevarnos a la conclusión que buscamos. Normalmente hay demasiadas cosas que pueden ser inferidas, y demasiadas vías que desperdician recursos. Ejemplos de estrategias que restringen la búsqueda de una solución son:

Conectividad única (Singly Connectedness)

Conjunto de apoyo (Set of Support)

Dependencia pasiva (Passive List Dependency)

Filtro de Prueba (Proof-Checking Filter)

Generalización (Into Variable)

Instanciación (From Variable)

Reducción de peso máximo (Maximum Weight Reduction)

Subtautología (Subtautology)

Variables distintas (Distinct Variables)

Pero algunas estrategias puede dirigir la búsqueda, simplemente guiando al programa para que se enfoque sobre ciertas vías de solución. Junto con las estrategias clásicas de búsqueda de ir saturando niveles (level saturation), se han usado las siguientes estrategias directivas para deducción automática:

Favorecer cláusulas unitarias (Unit preference)

Los últimos serán los primeros (Last-in First-out)

Parte final (Tail)

Parte final recursiva (Recursive Tail)

Proporción (Ratio)

Saturación de nivel (Level Saturation)

Sugerencias (Hints)

El primer tipo de estrategias impiden ciertas vías de solución pero no nos dicen cuáles vías tomar. El segundo tipo encauzan la búsqueda pero no impiden que tomemos alguna vía si se han agotados todas las de mayor preferencia. Normalmente se usan juntas estrategias de ambos tipos. Incluso hay estrategias que pueden ser usadas tanto para restringir la búsqueda como para encauzarla. Por ejemplo,

Resonancia (Resonance)

Sopesar (Weighting)

Sin estrategias, el uso indiscriminado de las reglas tiene poca esperanza de resolver problemas difíciles. Todas estas estrategias han sido usadas en los Laboratorios Argonne (véase http://www-unix.mcs.anl.gov/AR/strategies.html), en programas como NIUTP/AURA (en los setentas y principios de los ochentas), LMA/ITP (en los ochentas), y Otter (hoy día). A continuación, las presentamos brevemente.

1. Lista prioritaria (Hot List)

Wos propuso sacar conclusiones de ciertas cláusulas antes de lo que normalmente se obtendrían. Esto puede asegurar que tengamos una conclusión cuya complejidad haría, posteriormente, que ya no se obtuviera, o que simplemente no está en ninguna de las vías que serían exploradas. Las cláusulas en la lista prioritaria son consideradas con cada nueva inferencia en vez de esperar a que estas nuevas inferencias sean consideradas.

1. Lista prioritaria dinámica (Dynamic Hot List)

Permite añadir, durante la ejecución del programa, nuevas cláusulas a la lista prioritaria dependiendo de que cumplan ciertas características.

1. Demodulación (Demodulation)

Usando reglas de reescritura (demoduladores) podemos simplificar expresiones como 0+(0+x) = x y convertirlas en 0+x = x, que es normalmente suficiente para obtener lo otro.

1. Conectividad única (Singly Connectedness)

Supongamos que tenemos las cláusulas unitarias A, B y C. Además sabemos que de la conjunción de A, B y C se deduce D. Con resolución binaria hay seis vías para concluír D. La estrategia de conectividad única desecha vías que llevan a la misma conclusión.

1. Conjunto de apoyo (Set of Support)

Esta estrategia restrictiva, propuesta por Wos, impide usar información general. Consiste en declarar un conjunto arbitrario de cláusulas como necesarias. No se permite ninguna inferencia que no las use. Por supuesto, lo que vaya obteniéndose pasará a formar parte del conjunto de apoyo. Lo tradicional es escoger como conjunto de apoyo inicial a las premisas del problema más la negación de la conclusión, para derivar una contradicción.

1. Dependencia pasiva (Passive List Dependency)

Se hace una lista de cláusulas unitarias que serán descartadas si aparecen como conclusiones.

1. Favorecer cláusulas unitarias (Unit preference)

Esta estrategia, propuesta por Wos, privilegia el uso de cláusulas unitarias con una sola literal, sin disyunciones.

1. Filtro de Prueba (Proof-Checking Filter)

Esta estrategia descarta las fórmulas cuya prueba no haya sido de ciertas maneras. Sirve para checar una prueba y descartar conclusiones por demodulación.

1. Instanciación (From Variable)

Esta estrategia restictiva, propuesta por Wos, impide instanciaciones.

1. Generalización (Into Variable)

Esta estrategia restictiva, propuesta por Wos, impide generalizaciones.

1. Los últimos serán los primeros (Last-in First-out)

También llamada "Últimas entradas, primeras salidas", esta estrategia es lo opuesto de la saturación por niveles. Se concentra en la última cláusula que ha aparecido y permite explorar exhaustivamente una vía de solución antes de pasar a la siguiente ("depth first"). El peligro es que nunca pasemos a la siguiente.

1. Parte final (Tail)

Esta estrategia consiste en favorecer las fórmulas que tengan un segundo argumento breve. Por ejemplo, equivalencias en las que el término a la derecha de la igualdad tiene menos símbolos. Eso puede ayudar a mantener sencillas las conclusiones de la paramodulación, por ejemplo.

1. Parte final recursiva (Recursive Tail)

Esta estrategia es como la de la parte final, pero buscando partes finales breves a cualquier nivel, aunque estén profundamente anidadas.

1. Proporción (Ratio)

Esta estrategia directiva, propuesta por McCune, privilegia la información vieja y poco compleja. Combina sopesar las cláusulas menos complejas con la saturación de niveles.

1. Reducción de peso máximo (Maximum Weight Reduction)

Reduce el nivel de complejidad que pueden tener las inferencias que se van obteniendo.

1. Resonancia (Resonance)

Esta estrategia, propuesta por Wos, puede restringir al programa haciéndolo ignorar conclusiones que no se ajusten apropiadamente a ciertos patrones a los que se llama "resonadores". También puede ser directiva al privilegiar fórmulas a las que se les ha otorgado prioridad; por ejemplo, si corresponden, una vez ignoradas las variables, a patrones que han sido exitosos en el pasado.

1. Saturación de nivel (Level Saturation)

También llamada "Primeras entradas, primeras salidas" esta técnica clásica usa cláusulas en su orden de llegada ("first come first serve" o "first-in first-out") avanzando en las diferentes vías simultaneamente ("breadth first"). Favorece avanzar en todas las vías abiertas hasta el momento sin quedarse atorado en sólo una de ellas.

1. Sopesar (Weighting)

Esta estrategia, propuesta por Overbeek, puede ser tanto directiva como restrictiva. Es directiva si simplemente privilegia el uso de cláusulas en que aparezcan ciertos términos arbitrariamente escogidos o a las que tengan menor complejidad. Es restrictiva al impedir usar cláusulas con ciertos términos o que rebasen un límite escogido de complejidad.

Puede calcularse la complejidad simplemente contando el número de símbolos en cada cláusula, pero hay medidas más sofisticadas de complejidad. Una vez decidida una medida de complejidad, podemos impedir el uso de cláusulas demasiado complicadas, o simplemente favorecer el uso de las menos complejas.

1. Subtautología (Subtautology)

Esta estrategia es restrictiva pues bloquea el uso de cláusulas que contengan un subtérmino propio tautológico. La idea es omitir información que peque de trivial.

1. Sugerencias (Hints)

Esta estrategia, propuesta por Veroff, sugiere conclusiones al preferir fórmulas que correspondan a ciertos patrones escogidos por el usuario, o que subsuman o sean subsumidas por esos patrones.

1. Variables distintas (Distinct Variables)

Esta estrategia restrictiva consiste en desechar cláusulas con más de cierto número arbitrario de variables distintas. Es otra forma de desechar expresiones demasiado largas.

1. Otros métodos

Además de las estrategias para dirigir y restringir la búsqueda, hay estrategias para facilitarla, previniendo lo que se necesitará o eliminando redundancia. Entre las estrategias de prevención ("Look-Ahead") están las Listas Prioritarias y las Listas Prioritarias Dinámicas. Entre las que buscan controlar la redundancia ("Redundancy-Control") están Demodulación y Chequeo de Subsunciones.

1. Lista prioritaria (Hot List)

Wos propuso sacar conclusiones de ciertas cláusulas antes de lo normal. Esto puede asegurarnos una conclusión cuya complejidad haría, posteriormente, que ya no se obtuviera, o que simplemente no está en ninguna de las vías que serían exploradas. Las cláusulas en la lista prioritaria son consideradas con cada nuevo resultado en vez de esperar a que a estos nuevos resultados les toque a su vez ser considerados.

1. Lista prioritaria dinámica (Dynamic Hot List)

Permite añadir, durante la ejecución del programa, nuevas cláusulas a la lista prioritaria dependiendo de que cumplan ciertas características.

1. Demodulación (Demodulation)

Usando reglas de reescritura (demoduladores) podemos simplificar expresiones como 0+(0+x) = x y convertirlas en otras como 0+x = x, que son normalmente suficiente para obtener lo primero.

1. Chequeo de Subsunciones (Subsumption Checking)

Si tenemos expresiones como 0+x =x y 0+a =a, la segunda fórmula está subsumida en la primera, porque la constante a es una instancia de la variable x. Esta estrategia elimina afirmaciones específicas innecesarias cuando tenemos afirmaciones generales que las contienen de manera obvia. La información descartada puede incluso ser la vieja, cuando encontramos información nueva más general (back subsumption).

1. Encadenamiento hacia adelante o hacia atrás

A partir de los datos que tenemos, es posible obtener inmediatamente conclusiones, o bien esperar hasta que haya una pregunta que contestar o una meta específica que alcanzar. En el primer caso, sobre los datos aplicamos reglas para extraer otra información implícita, avanzando hacia posibles conclusiones. Por ejemplo, cada que obtengamos el antecedente de un condicional aplicamos Modus Ponens y añadimos a nuestro banco de datos el consecuente. En el segundo caso, empezamos considerando el objetivo al que deseamos llegar y retrocedemos hacia la información que tenemos. Por ejemplo, si lo que buscamos es el consecuente en un condicional que ya tenemos, tratamos de obtener el antecedente para poder hacer Modus Ponens.

La ventaja de encadenar nuestras inferencias hacia adelante es que partimos de material que poseemos y todo lo que descubramos se incorpora a nuestra base de datos. La desventaja es que mientras más encontramos, más elementos tenemos para sacar más inferencias y el número de elementos tiende a crecer exponencialmente (geométricamente), como un abanico.

La ventaja de encadenar hacia atrás es que sabemos a dónde vamos, y la consideración de lo que buscamos tiende a evitar explorar avenidas innecesarias para nuestro problema. Sólo consideramos caminos que terminan en la solución. En el encadenamiento hacia atrás, es común tener como meta encontrar una instancia de algo (e. g., un vuelo de México a Toronto que salga el próximo viernes en la tarde). Por ello, no solamente buscamos probar que hay alguna instancia, sino ofrecer la substitución de variables que permita unificar con la meta: {[v, vuelo-208]}.

La desventaja de encadenar hacia atrás es que los pasos previos que vamos proponiendo pueden no estar garantizados por nuestros datos iniciales. Cualquier conclusión puede ser alcanzada a partir de infinitos estados iniciales distintos, así es que podríamos estar retrocediendo hacia lugares de los que no podemos partir, dados solamente nuestros datos iniciales.

Naturalmente, ambos métodos pueden combinarse para tratar de combinar sus ventajas. Avanzar un poco desde la información inicial, retroceder un poco desde la meta, e ir buscando que los dos caminos se encuentren en el medio.

Bibliografia

Aikins, Janice; Ballantyne, Michael; Bledsoe, W. W.; Doyle, Jon; Moore, Robert C.; Pattis, Richard; Rosenschein, Stanley J. "Automatic Deduction". 1982. The Handbook of Artificial Intelligence, vol. III, editado por Paul R. Cohen y Edward A. Feigenbaum. Addison-Wesley.

Amor, José Alfredo; Miranda Perea, Favio. 1997. "Demostración automática de teoremas y La Nutria". Aportaciones Matemáticas 20, pp. 159-179.

Ben-Ari, M. 1993. Mathematical Logic for Computer Science, Prentice Hall.

Bundy, A. 1983. The Computer Modelling of Mathematical Reasoning, Academic Press.

Chang, C.; Lee, R.C. Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.

Chang, Chin-Liang; Lee, Richard Char-Tung. 1987. Symbolic Logic and Mechanical Theorem Proving. Academic Press.

Charniak, Eugene; McDermott, Drew. 1987. "Logic and Deduction", en Introduction to Artificial Intelligence Addison-Wesley, pp. 319-392.

Clocksin, W. F.; Mellish, C. S. 1987. Programming in Prolog. Tercera edición, Springer-Verlag.

Davis, E. 1990. Representations of Commonsense Knowledge, Morgan Kaufmann.

Duffy, David. Principles of Automated Theorem Proving. John Wiley and Sons, 1991.

Gallier, J.H. 1986. Logic for Computer Science, Harper and Row.

Gardner, Martin. 1983. Logic Machines and Diagrams. Segunda edición, Harvester Press.

Gilmore, P.C.1960. "A Proof Method for Cuantification Theory". IBM J. Res. Develop. 4, 28-35.

Hopcroft, J.E. and Ullman, J.D. 1979. Introduction to Authomata Theory Languages, and Computation, Addison Wesley.

Kapur, D. (editor). Proceedings of the 11th International Conference on Automated Deduction (CADE-11). Saratoga Springs, NY, USA, Junio 15-18, 1992, Lecture Notes in AI 607, Springer-Verlag, 1992.

Kowalski, Robert. 1979. Logic for Problem Solving. North-Holland.

Leitsch, Alexander. 1997. The Resolution Calculus. Springer.

Lloyd, J. W. 1984. Foundations of Logic Programming. Springer-Verlag.

Miranda Perea, Favio. 1999. Fundamentos Lógicos del Programa de Razonamiento Automático OTTER, Tesis de Maestría en la Facultad de Ciencias de la UNAM.

Odifreddi, P. (ed). 1990. Logic and Computer Science, Academic Press.

Rich, Elaine. 1983. "Knowledge Representation". En Artificial Intelligence. McGraw-Hill, pp. 135-172.

Robinson, J. Alan. 1965. "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the Association for Computing Machinery. Enero, vol. 12, no. 1, pp. 23-41.

Robinson, J. Alan. 1989. "Resolution: Working Material for the Lectures". International Summer School on Logic, Algebra and Computation. Marktoberdorf, Alemania, julio 25-agosto 6, pp. 1-27.

Stachniak, Zbigniew. 1996. Resolution Proof Systems: An Algebraic Theory. Kluwer.

Winston, Patrick Henry. 1984. "Resolution Proofs". En Artificial Intelligence. Addison-Wesley, segunda edición, pp. 216-227.

Wos, Larry. 1998. "Programs that Offer Fast, Flawless, Logical Reasoning". Communications of the ACM, Junio, vol. 41, no. 6, pp. 87-95.

Wos, Larry; Overbeek, Ross; Lusk, Ewing; Boyle, Jim. 1984. Automated Reasoning: Introduction and Applications. Prentice Hall. Segunda edición, McGraw-Hill, 1992.

1. Wos [1998], p. 89.

2. Nacido el 23 de mayo de 1887 en Sandsvaer, Noruega, muerto el 23 de marzo de 1963 en Oslo, Noruega.

3. Algunas personas creerán que siempre que se dice que se alaba, se alaba; igual que parece que se hace una promesa solo con decir que se promete. Pero si alguien dice "Yo prometo" falta que nos diga qué promete. No hay promesa sin algo prometido. Sin decir qué se promete, la promesa está incompleta o inconclusa, y no logra ser realmente una promesa. Hay promesas incumplidas, pero no promesas inconclusas. Igualmente, toda alabanza debe referirse a los alabados. Una alabanza incompleta con respecto a este aspecto tan importante, no es alabanza. En la historia que contamos, no existe el grupo de los alabados (suponer que existe llevaría a una contradicción). Al no existir el grupo de quienes se alaba, lo dicho tiene sólo la apariencia de alabanza. Es imposible determinar qué se alabó. El cuento miente al calificar las palabras del moribundo como alabanza.

4. Una cláusula es negativa si todas sus literales son negativas, es positiva si todas sus literales son positivas. Es mixta en otro caso.