Claúsulas y resolución

En la práctica resulta incómodo operar con un sistema deductivo formal en que las expresiones lógicas utilizadas tienen formas muy variadas y se debe elegir entre muchas reglas de deducción aplicables en cada paso.

Esta situación se puede mejorar notablemente restringiendo el tipo de las expresiones lógicas a un formato más simple de operar. En particular, la forma de cláusula sólo utiliza los conectivos ¬ (negación) y  (disyunción), y sólo requiere de una regla de deducción, llamada regla de resolución.

Veremos que al restringir un sistema deductivo de esta manera no se pierde generalidad porque existe un mecanismo de normalización que permite plantear cualquier problema lógico mediante cláusulas. 

Cláusulas

Una cláusula es una fórmula lógica constituida por una disyunción de literales en que cada literal Li es una fórmula atómica negada (literal negativo) o no negada (literal positivo).

El orden en que aparecen los literales no es relevante, y se puede por lo tanto representar la misma cláusula como un conjunto de literales:

En el caso particular en que este conjunto es vacío, la cláusula se denomina cláusula vacía y se simboliza por . 

Resolución

La regla de resolución binaria permite derivar una nueva cláusula (el resolvente) a partir de dos cláusulas padres. En su forma más simple, se define mediante el siguiente esquema, cuya validez puede verificarse utilizando una tabla de verdad: Para aplicarla, es necesario que las cláusulas padres contengan un literal que manifieste la misma fórmula atómica (P en el esquema), pero en forma positiva en un padre y negativa en el otro. Este literal es eliminado en el resolvente, obteniéndose la disyunción del resto de los literales de las cláusulas padres. El esquema general de la regla es: Nótese que la regla de resolución produce un resolvente más grande o del mismo tamaño que la más grande de las cláusulas padres, excepto si una de las cláusulas padres contiene sólo un literal. 

Demostración por resolución de contradicción

Una manera de demostrar formalmente un teorema es encontrar una cadena de derivaciones cuyo último elemento es el teorema buscado. Sin embargo, existe otra manera de enfrentar el problema:
  1. suponer lo contrario de lo que se desea demostrar
  2. probar que esa suposición es contradictoria.
Si suponiendo algo se llega a una contradicción, lo contrario de ese algo debe ser verdadero. Este es un principio muy utilizado en matemática en lo que se llama demostración por el absurdo. Se basa en la siguiente propiedad: Es decir, si A es consecuencia lógica de , entonces no existe ninguna interpretación en que se verifiquen simultáneamente todas las fórmulas de  y ¬A.

Cuando se opera con cláusulas y la regla de resolución, las contradicciones se detectan cuando se llega a un resolvente vacío (). Esto resulta evidente si se considera que la única manera de producir un resolvente vacío es tomando dos cláusulas padres de un sólo un literal, positivo en un caso, negativo en el otro.

La ventaja de la demostración por resolución de contradicción, o demostración por refutación, es que la orientación del proceso se mantiene invariable, independientemente del problema lógico abordado: llegar a una contradicción. Concretamente, en el caso de operar con cláusulas, el objetivo es encontrar resolventes cada vez más pequeños hasta llegar a un resolvente vacío. Se puede demostrar que para lograr este objetivo basta la regla de resolución (la regla de resolución es completa para la refutación). 

Normalización a forma clausal

Para aplicar el método de demostración por refutación utilizando la regla de resolución binaria, es necesario que todas las fórmulas lógicas involucradas en el problema se puedan reescribir en forma de cláusulas semánticamente equivalentes. Esta normalización se puede llevar a cabo utilizando un algoritmo de transformación que consta de los siguientes pasos:
  1. se elimina el conectivo  utilizando la identidad lógica (AB) = (¬AB)
  2. Se reduce el alcance de los conectivos ¬ aplicados a fórmulas no atómicas traspasándolo al interior de dichas fórmulas. Se utilizan las siguientes identidades lógicas:
  3. Se estandarizan los nombres de variables colocándole nombres distintos a variables asociadas con cuantificadores distintos.
  4. Se eliminan los cuantificadores existenciales mediante un proceso llamado skolemización que consiste en reemplazar las variables cuantificadas existencialmente por:
  5. Se mueven todos los cuantificadores universales al principio de la fórmula. Esto se puede hacer porque previamente se estandarizaron los nombres de las variables.
Al cumplirse la etapa 5 del algoritmo, se dice que la fórmula resultante está en forma normal prenex porque todos los cuantificadores aparecen al principio como un prefijo (prefix) seguido del la expresión o matriz (matrix).

El algoritmo de normalización prosigue así:

  1. Se eliminan todos los cuantificadores universales. Esto es posible porque las únicas variables que quedan están cuantificadas universalmente y no hay conflictos de nombre, por lo tanto no es necesario explicitar los cuantificadores ni su alcance. Por omisión, todas las variables están cuantificadas universalmente.
  2. Se desarrolla la expresión resultante distribuyendo  sobre para convertirla en una conjunción de disyunciones. La distribución se apoya en la siguiente identidad lógica:
  3. Cada elemento de la conjunción resultante se convierte en una cláusula independiente constituida por una disyunción de fórmulas atómicas negadas o no negadas.
  4. El último paso es estandarizar de nuevo las variables poniéndole nombres distintos a variables que se encuentren en cláusulas distintas

Ejemplo de normalización a forma clausal

Se tiene la fórmula: Los pasos del proceso de normalización son:
  1. eliminación de  :

    2. x (¬(hombre (x) mujer (x)) ( y progenitor (x, y)creado (x)))
  2. reducción de ¬ :

    3. x ((¬hombre (x) ¬mujer (x)) ( y progenitor (x, y)creado (x)))
  3. estandarización de variables:

    4. no cambia
  4. skolemización:

    5. x ((¬hombre (x) ¬mujer (x)) (progenitor (x, f (x))creado (x)))
  5. mover cuantificadores al principio:

    6. no cambia
  6. eliminación de cuantificadores:

    7. ((¬hombre (x) ¬mujer (x)) (progenitor (x, f (x))creado (x)))
  7. distribución de  sobre  :

    8. ((¬hombre (x) (progenitor (x, f (x))creado (x)))
    ((¬mujer (x) (progenitor (x, f (x))creado (x)))
  8. separación de la conjunción:

    9. clausula 1: ¬hombre (x)progenitor (x, f (x))creado (x)
    clausula 2: ¬mujer (x)progenitor (x, f (x))creado (x)
  9. estandarización de variables:

    10. clausula 1: ¬hombre (x)progenitor (x, f (x))creado (x)
    clausula 2: ¬mujer (y)progenitor (y, f (y))creado (y)

Ejemplo de resolución por refutación (lógica proposicional)

Planteamiento del problema
fórmulas lógicas cláusulas
Base de conocimiento ():
  1. perro-fido
  2. perro-fido  animal-fido
  3. animal-fido  mortal-fido
 Base de conocimiento:
  1. perro-fido
  2. ¬perro-fido  animal-fido
  3. ¬animal-fido  mortal-fido
Por demostrar: mortal-fido
Negación de hipótesis: 4. ¬mortal-fido
Solución
padre 1 padre 2 resolvente
(4) ¬mortal-fido (3) ¬animal-fido mortal-fido (5) ¬animal-fido
(5) ¬animal-fido (2) ¬perro-fido animal-fido (6) ¬perro-fido
(6) ¬perro-fido (1) perro-fido (contradicción)

Resolución con unificación

En lógica proposicional, los literales de una cláusula son símbolos proposicionales negados o no negados. Para aplicar la regla de resolución se requiere que ambas cláusulas padres involucradas contengan un literal cuyo símbolo proposicional sea idéntico, pero que aparezca negado en una y no negado en la otra.

En lógica de predicados, los literales contienen una fórmula atómica (un símbolo de predicado con sus argumentos). La regla de resolución se puede aplicar cuando ambas cláusulas padres contienen un literal, positivo en una y negativo en la otra, que manifiesta la misma fórmula atómica. Sin embargo, si las fórmulas atómicas que se intenta asimilar no son idénticas pero contienen variables que al ser convenientemente substituidas producen el mismo resultado, la regla de resolución también se puede aplicar después de hacer esta substitución. El proceso de encontrar una asignación de variables que cumpla con este requerimiento se llama unificación. 

Unificación

La unificación es un proceso que consiste en encontrar una asignación de variables que haga idénticas a las fórmulas que se desea unificar. Su resultado, el unificador, se expresa como un conjunto de pares substitución/variable para cada una de las variables asignadas (este conjunto recibe también el nombre de substitución). El valor de substitución para una variable puede ser cualquier término del lenguaje lógico utilizado (exceptuando términos con la misma variable). Por ejemplo, se pueden unificar las fórmulas utilizando el unificador { juan / X, hermano(Y) / Z }.

También se podría utilizar la substitución { juan / X, hermano(pedro) / Z, pedro / Y }, pero aquí se introduce una asignación suplementaria que no es necesaria para unificar. Para evitar introducir substituciones arbitrarias, se utiliza el unificador más general, es decir, el que minimiza las restricciones impuestas a los valores de las variables (en este caso concreto, Y puede tomar cualquier valor).

La unicación es una operación sintáctica.
Por ejemplo, no se puede unificar padre(X, hermano(Y)) con padre(pedro, julio) porque no hay ninguna substitución de variables que haga sintácticamente iguales a hermano(Y) y julio. 

Composición de substituciones

La aplicación de una substitución s a una fórmula F se escribe F s y entrega como resultado una nueva fórmula en que las variables asignadas han sido reemplazadas por sus respectivos valores. Por ejemplo: Si F = padre(pedro, Z) se obtiene el mismo resultado (ya que s es el unificador de ambas fórmulas).

Dos substituciones s1 y s2 se pueden aplicar succesivamente con el mismo efecto que una substitución única equivalente s que corresponde a la composición de s1 y s2:

Si los valores de substitución de s2 no hacen referencia a las variables asignadas en s1, se puede calcular la composición s de la siguiente manera:

Algoritmo de unificación

Existe un algoritmo recursivo que entrega como resultado el unificador más general de dos fórmulas lógicas, o, si no se pueden unificar, una indicación de falla. El algoritmo se escribe de la siguiente manera:

Regla de resolución con unificación

Cuando se opera en lógica de predicados (con variables) la regla de unificación se expresa de la siguiente manera: Para aplicar la regla se requiere que los términos identificados (PA y PB) sean unificables. El unificador u se aplica al resolvente.

Si se está utilizando la regla de resolución en una demostración por refutación, las asignaciones de variables encontradas al terminar el proceso corresponden a un caso particular en que la consulta negada no se cumple, es decir, a un caso particular en que la consulta original se cumple.

Viendo al problema planteado como una ecuación lógica, lo que se obtiene es una solución particular. Haciendo un uso adecuado de mecanismos de backtracking se pueden obtener todas las demás soluciones del problema. Este es el principio fundamental de la programación lógica. 

Ejemplo de resolución por refutación (lógica de predicados)

Planteamiento del problema
fórmulas lógicas cláusulas
Base de conocimiento:
  1. perro (fido)
  2. X (perro (X) animal (X))
  3. Y (animal (Y) mortal (Y))
Base de conocimiento:
  1. perro (fido)
  2. ¬perro (X)  animal (X)
  3. ¬animal (Y)  mortal (Y)
Por demostrar:  Z mortal (Z)
Negación:  Z ¬mortal (Z)
Negación de hipótesis: 4. ¬mortal (Z)
Solución
padre 1 padre 2 unificador resolvente
(4) ¬mortal (Z) (3) ¬animal (Y) mortal (Y) { Y / Z } (5) ¬animal (Y)
(5) ¬animal (Y) (2) ¬perro (X) animal (X) { X / Y } (6) ¬perro (X)
(6) ¬perro (X) (1) perro (fido) { fido / X } (contradicción)

La consulta se cumple para Z = Y = X = fido.

Como respuesta sólo interesa desplegar el valor de las variables de la consulta. En este caso concreto, la respuesta es Z = fido. 

Estrategias de resolución

Para automatizar el proceso de resolución por refutación se requiere precisar una manera de proceder que garantice llegar a una contradicción si el conjunto de cláusulas es inconsistente. Las estrategias que cumplen con este requisito son llamadas estrategias completas.

Un ejemplo de estrategia completa es hacer una búsqueda en amplitud que explora todas las posibilidades en paralelo. Inicialmente se aparean las cláusulas del conjunto original de todas las maneras posibles y se genera un conjunto de resolventes que corresponden a los casos en que se pudo aplicar la regla de resolución. En una segunda etapa, estas nuevas cláusulas generadas se aparean entre ellas y con las cláusulas originales y se genera otro nuevo conjunto de resolventes con los cuales se vuelve a repetir la operación y así succesivamente hasta encontrar un resolvente vacío. En cada etapa se aparean las nuevas cláusulas generadas en la etapa anterior con todas las cláusulas generadas hasta la etapa y las cláusulas originales.

La estrategia de búsqueda en amplitud puede tornarse rápidamente inmanejable dada la cantidad siempre creciente de cláusulas generadas. Una manera de controlar esta proliferación sin perdida de generalidad (manteniendo la propiedad de ser una estrategia completa) se logra restringiendo los apareamientos entre cláusulas sólo a aquellos pares en que por lo menos una de las cláusulas involucradas sea derivada de la negación de la consulta original. Esto se basa en la intuición de que si existe una contradicción, necesariamente debe provenir de la consulta negada, ya que una buena teoría del dominio modelado no puede ser inconsistente.

En problemas grandes, las estrategias completas suelen ser demasiado exhaustivas para obtener un resultado en un tiempo prudente y se hace por lo tanto necesario introducir heurísticas que permitan orientar el proceso de resolución. Estas heurísticas sacrifican la seguridad de encontrar la solución para acelerar el cálculo (las estrategias heurísticas generalmente no son completas). Las heurísticas más utilizadas son:

  1. Preferir resolver con cláusulas de un solo literal. Es la única manera de obtener un resolvente más pequeño que las cláusulas padres, camino obligado para llegar a un resolvente vacío.
  2. Resolver la consulta negada con algún axioma, repetir la operación para el resolvente obtenido y así succesivamente hasta llegar a un resolvente vacío. En cada etapa se resuelve la cláusula más recientemente generada con algún axioma original.

Cláusulas de Horn

La normalización a cláusulas y el uso de demostración por resolución de contradicción facilitan la solución automática de los problemas planteados mediante lógica. Sin embargo, existen muchas maneras de llevar a cabo una demostración, lo que implica elegir una estrategia cuya efectividad puede depender del problema abordado.

Una manera de simplificar este proceso de demostración es restringiendo el tipo de cláusulas con la cual se opera, tratando de mantener una forma intuitivamente interpretable para un programador humano (para que sea posible plantear directamente los problemas en ese formato) y que permita la aplicación de un algoritmo de resolución más facil de implementar.

Las cláusulas de Horn satisfacen ambos requerimientos y están en la base de la mayoría de los sistemas de programación lógica, en particular de PROLOG. Una claúsula de Horn es una cláusula con a lo más un literal positivo, es decir:

Una propiedad importante de las cláusulas de Horn es que al resolver dos cláusulas de Horn se obtiene como resolvente otra cláusula de Horn. Esto garantiza que siempre se estará operando con el mismo formato durante el proceso de demostración.

Interpretación intuitiva de cláusulas de Horn

Una cláusula de la forma corresponde a una expresión lógica más fácil de leer como lo que se suele escribir de la siguiente manera Las cláusulas con este formato son llamadas reglas. Desde un punto de vista declarativo, una regla especifica la definición de una relación (P) en función de otras relaciones (Q1, Q2, ... Qn). Desde un punto de vista procedural, P se interpreta com un objetivo por cumplir que se descompone en Q1, Q2, ... Qn subobjetivos, los cuales a su vez pueden admitir una descomposición basada en reglas.

Las cláusulas que se reducen a un solo literal positivo son llamadas hechos y se escriben

Un hecho corresponde a la definición de una relación elemental.

Las cláusulas que sólo contienen literales negativos

corresponden a objetivos que se deben satisfacer, es decir, a una consulta por resolver. Nótese que la cláusula es la negación de la consulta original, por lo tanto los cuantificadores universales implícitos en la cláusula corresponden a cuantificadores existenciales en la consulta original.

Construir una teoría del universo mediante cláusulas de Horn equivale a definir relaciones relevantes, lo que puede hacerse recursivamente y especificando varias reglas o hechos por cada relación. Por ejemplo:

Las consultas pueden verse como ecuaciones lógicas cuyas variables son las incógnitas por despejar. 

Algoritmo de resolución con cláusulas de Horn

La consulta negada siempre se expresa mediante una cláusula que sólo contiene literales negativos: Las únicas contradicciones que es posible derivar mediante resolución deben originarse a partir de esta consulta negada, ya que la teoría del universo no puede ser inconsistente. Para aplicar resolución se debe identificar entre las reglas (o hechos) pertenecientes a la teoría del universo, una regla de la forma tal que la cabeza Q de la regla sea unificable con algún subobjetivo Qi de la consulta. Si u es el unificador más general para Q y Qi, entonces el resolvente de la regla es la cláusula que conserva la misma forma que la consulta negada y constituye un nuevo objetivo por satisfacer.

El algoritmo de resolución consiste entonces en iterar la aplicación de la regla de resolución mientras el objetivo resultante no sea vacío. Nunca se resuelven las reglas o hechos de la teoría del universo entre sí. Siempre participa la cláusula de consulta o una cláusula derivada de ella.

La expresión anterior del algoritmo de resolución es no determinística. Para implementarlo en una máquina secuencial se requiere precisar un orden de evaluación, lo que se puede lograr mediante los siguientes criterios:

  1. Satisfacer siempre primero el primer subobjetivo de la consulta, luego el primer subobjetivo de la cláusula resultante, y así succesivamente.
  2. Ordenar las reglas y hechos de la teoría del universo y elegir siempre la primera regla unificable para resolver. Cada vez que se utiliza una regla o un hecho, se reemplazan sus variables por variables frescas creadas dinámicamente.
  3. Cuando ya no se puede seguir resolviendo, volver al último punto de decisión y elegir la siguiente regla para resolver. Esto constituye un backtracking que permite recorrer todas las soluciones posibles (siempre que no haya recursiones infinitas).
Estos son los criterios definidos en el lenguaje de programación lógica PROLOG. Además, cada vez que se obtiene un resolvente vacío, se imprimen los valores asociados a las variables de la consulta, componiendo todas las unificaciones que fueron necesarias para llegar a ese resultado.