1 Lógica matemática.

Dado que el Lenguaje Natural, aunque es potente, resulta muy ambiguo, nos interesa encontrar un lenguaje más sencillo, sin ambigüedades que nos permita realizar razonamientos y generalizaciones. Por ello, es necesario introducirnos en la formalización del Cálculo Proposicional, que, aunque no cuenta con toda la potencia necesaria para describir el mundo, es válido como primera aproximación. También veremos algunos conceptos del Cálculo de Predicados y, por supuesto, nos centraremos en definir y ver cómo funciona el Método de Resolución.

[ÍNDICE]

Para comprender los principios de la lógica matemática en el campo del Cálculo Proposicional, necesitamos conocer una serie de conceptos básicos que se describen a continuación:

• Átomo: También llamado Fórmula Atómica o Enunciado Simple. Permite la formalización de una frase declarativa que no se puede descomponer en frases más simples. Para denotar átomos se utilizan las letras p, q, r, etc.
• Conectiva: Operador que permite construir sentencias compuestas a partir de átomos. Las principales conectivas lógicas son: Ø , Ù , Ú , ® .
• Enunciado: También llamado Fórmula. Es una expresión realizada con átomos y conectivas lógicas, siguiendo unas determinadas normas. Para denotar enunciados se utilizan las letras A, B, C, etc.
• Deducción: Consiste en una lista de enunciados que, o bien son dados previamente, en este caso se llaman Premisas, o bien se han obtenido de enunciados anteriores mediante la utilización de un conjunto finito de reglas denominadas Reglas de Inferencia.

Dada una serie de premisas, a través de las reglas de inferencia, podemos llegar a un enunciado que podemos denominar enunciado Conclusión. El conjunto de pasos para llegar a este enunciado a partir de las premisas usando dichas reglas de inferencia, compone un algoritmo general que permite automatizar el proceso de demostración. De esta forma, obtenemos un demostrador automático de teoremas que es, justamente, en lo que consiste la máquina PROLOG.

Aunque mediante la Lógica Proposicional podemos describir muchas situaciones, existen otras imposibles de representar. Necesitamos introducirnos, además, en la Lógica de Predicados. Podemos considerar la Lógica Proposicional como un subconjunto de la Lógica de Predicados o de Primer Orden. Por tanto, a las definiciones anteriores, hemos de añadir otras nuevas que nos permitan comprender los métodos que se explicarán en apartados posteriores.

• Símbolos: Existen varios tipos:
• Individuales o Constantes: Representan valores concretos. C={a, b, c, d, e}.
• Variables: Se pueden sustituir por constantes. V={x, y, z, v, w}.
• Funciones: Aplicación que asocia una serie de constantes con otra constante. F={f, g, h}.
• Predicados: Función de resultado Verdadero o Falso. Pred={P, Q, R}.
• Relaciones: Representan relaciones o cuantificaciones. Rel={Ù , Ú , ® , « , Ø , " , $ }
• Signos de puntuación: Permiten agrupar o separar otros símbolos. Pun={(, ), ,, [, ]}
• Términos: Se pueden definir de varias maneras. A continuación se exponen las distintas formas de definición de términos:
• Una constante: a, c.
• Una variable: x, z.
• Si f es un símbolo de función y t₁, t₂,..., t_n son términos, entonces f (t₁, t₂,,..., t_n) es un término, por ejemplo g(a, f(x)).
• Fórmulas: Se definen como:
• Si R es un símbolo de relación y t₁, t₂,..., t_n son términos, entonces R (t₁, t₂,,..., t_n) es una fórmula.

• Si A y B son dos fórmulas y R es un símbolo de relación, entonces R(A, B) también es una fórmula.

• Sentencias: Se definen como fórmulas en las que ninguna de las variables que la componen tiene una o más ocurrencias libres, o sea, todas las variables de la fórmula son ligadas. Es necesario que definamos, por tanto, lo que son variables libres y ligadas.

• Una ocurrencia de una variable x es ligada en una fórmula si y sólo si se da una de las siguientes condiciones:

1. La variable x está inmediatamente después de un símbolo " ó $ .
2. La variable x está en el radio de acción de un cuantificador " x ó $ x.

• El radio de acción de un cuantificador en una fórmula abarca al término inmediatamente siguiente, haciéndose imprescindible el uso de paréntesis para aumentar su radio de acción.

• Una variable es libre en una fórmula si no tiene ninguna ocurrencia ligada en la misma. En el siguiente ejemplo, la variables v es libre, puesto que no tiene ninguna ocurrencia ligada. Sin embargo, la x presenta una ocurrencia ligada, ya que g(x) cae dentro del radio de acción del cuantificador " x.

• Sustituciones: Dado el conjunto de variables V y el conjunto de términos Term, una sustitución se define como la aplicación que se muestra en la Ec 1 y se suele denotar como s={x₁/t₁,...,x_n/t_n}. De dicha definición podemos concluir dos cosas:
• Sólo son válidas aquellas sustituciones que transforman una variable en una constante, en otra variable o en una función, es decir, en términos.
• La sustitución de una variable afecta a todas las ocurrencias de la misma.

[ÍNDICE]

La Deducción Natural consiste en un sistema de reglas de inferencia que permite construir deducciones, es decir, a partir de "algo" podemos deducir o "llegar a" "otra cosa", hasta que encontramos una conclusión. Se trata de un método puramente sintáctico donde sólo nos ocupamos de la manipulación de símbolos. Es un método interesante para construir demostraciones, sin embargo es difícilmente mecanizable.

Por otro lado, como hemos visto, es fácil representar hechos del mundo real mediante la lógica proposicional y mediante la lógica de predicados. Además mediante la lógica de predicados podemos representar el conocimiento que tenemos sobre un cierto mundo finito poniéndolo en forma de sentencias y disponemos de un mecanismo para razonar con ese conocimiento. Sin embargo, lo que para el ser humano resulta trivial, deducir una sentencia a partir de otra, para la máquina puede llegar a ser computacionalmente muy costoso e, incluso, inviable. Los estudios, por tanto, se han centrado en conseguir un método de demostración que se puede ejecutar en un tiempo finito, y que en dicho tiempo, de forma eficiente, nos proporcione una solución acertada.

El Método de Resolución [Robinson, 1965], es un intento de mecanizar el proceso de deducción natural de esa forma eficiente. Las demostraciones se consiguen utilizando el método refutativo (reducción al absurdo), es decir lo que intentamos es encontrar contradicciones. Para probar una sentencia nos basta con demostrar que su negación nos lleva a una contradicción con las sentencias conocidas (es insatisfactible). Si la negación de una sentencia entra en contradicción con los hechos de nuestra base de conocimiento es porque lo contrario, es decir, la sentencia original era verdadera y se puede deducir lógicamente de las sentencias que componen dicha base de conocimientos.

Existen distintas Estrategias de Resolución: sistemática, con conjunto soporte, unitaria, primaria y lineal.

En este apartado formularemos detalladamente el método de Resolución por Refutación Lineal. Para ello, es necesario conocer el proceso de conversión a forma clausal, ya que las cláusulas con las que se trabaja en esta técnica deben tener una forma específica. Por otro lado, hemos de definir también el proceso o algoritmo de Unificación, paso imprescindible en este método de Resolución.

[ÍNDICE]

Conversión a forma clausal.

El proceso de conversión a forma clausal consiste en transformar las sentencias y fórmulas en cláusulas, cuya principal característica, al nivel de representación, es la ausencia casi total de símbolos de relación. En una cláusula sólo aparecerán disyunciones "Ú ".

De esta manera, el primer paso será transformar todas las sentencias a una forma canónica llamada forma normal conjuntiva [Davis y Putnam, 1960], a partir de la cual obtendremos el conjunto de cláusulas. Así, podemos definir una cláusula, más formalmente, como una fórmula en forma normalizada conjuntiva que no tiene ninguna conectiva. Esta transformación la vamos a realizar en varios pasos:

1. Primero pasaremos las sentencias a Forma Normal Prenexa.
2. En el siguiente paso las transformaremos a Funciones de Skolem.
3. Finalmente llegaremos a una representación en Forma de Cláusulas.

[ÍNDICE]

Una fórmula está en Forma Normal Prenexa si es de la forma: Q₁x₁...Q_nx_nY donde Y es una fórmula desprovista de cuantificadores y escrita como conjunción de disyunciones, Q_1,...,Q_n Î {" , $ } y x₁,..., x_n son variables.

Tenemos nuestro conocimiento en forma de sentencias, formadas por símbolos de relación, variables, constantes, cuantificadores, todos mezclados. Para transformar una fórmula a Forma Normal Prenexa seguiremos el siguiente algoritmo:

• Eliminar todos los símbolos de equivalencia (« ), sustituyéndolos por una implicación a la derecha y una implicación a la izquierda: P« Q = (P® Q) Ù (Q® P)
• Eliminar todas las implicaciones (® ), sabiendo que (a ® b) es equivalente a (Ø a Ú b).
• Reducir el ámbito de las negaciones (Ø ), a un único término, usando las siguientes propiedades:
• Ø (Ø p)=p
• Leyes de Morgan: Ø (a Ú b)= Ø a Ù Ø b y Ø (a Ù b)= Ø a Ú Ø b
• Ø " x P(x) = $ x Ø P(x)
• Ø $ x P(x) =" x Ø P(x)
• Normalizar las variables de los cuantificadores, de forma que cada uno esté ligado con una única variable. Para ello podemos, incluso, renombrar las variables.

• Mover todos los cuantificadores a la izquierda de la fórmula sin cambiar su orden relativo.

[ÍNDICE]

El siguiente paso es convertir las fórmulas de Forma Normal Prenexa a Fórmulas de Skolem, que se caracterizan por no estar cuantificadas existencialmente. Por tanto, el algoritmo de transformación a forma de Skolem elimina los cuantificadores existenciales.

Partimos de una fórmula: Q₁x₁...Q_nx_nY. Se recorre la fórmula en forma prenexa de izquierda a derecha y se eliminan los cuantificadores existenciales según los dos casos siguientes:

• Sea Q_r un cuantificador existencial:
• Si no hay ningún cuantificador universal antes de Q_rx_r, elegir una nueva constante c distinta de todas las que aparecen en Y, y reemplazar cada ocurrencia de x_r en Y por c. Borrar Q_rx_r del prefijo de la fórmula.
• Si Q_s1, Q_s2,…, Q_sk son los cuantificadores universales que aparecen antes de Q_rx_r, tomar un nuevo símbolo de función f distinto a todos los que aparecen en Y y reemplazar cada ocurrencia de x_r por f(x_s1,x_s2,...,x_sk). Borrar Q_rx_r del prefijo de la fórmula.

• Representación en forma de cláusulas: El último paso será convertir las funciones de Skolem a cláusulas. Tenemos las fórmulas cuantificadas universalmente, entonces podemos eliminar todos los prefijos, de tal manera que la fórmula resultante está en forma de conjunción de disyunciones (forma normal conjuntiva): (a Ú b Ú c) Ù (d Ú e) Ù (j Ú l Ú m). Finalmente, por cada conjunción obtenemos una cláusula: (a Ú b Ú c), (d Ú e) y (j Ú l Ú m).

Todos los pasos que hemos visto podemos resumirlos en el siguiente algoritmo, que es justamente el algoritmo general de conversión a forma clausal:

1. Convertir la fórmula a Forma Normal Prenexa.
2. Transformarla a Forma de Skolem.
3. Pasar a Forma Normal Conjuntiva.
4. Separar cada conjunción en una cláusula.

[ÍNDICE]

Algoritmo de Unificación.

Podemos definir la Unificación como un procedimiento de emparejamiento que compara dos literales y descubre si existe un conjunto de sustituciones que los haga idénticos. La idea básica de la unificación es muy sencilla. Para unificar dos literales vamos recorriéndolos de izquierda a derecha. En primer lugar se comprueba si los predicados coinciden. Si es así, seguimos adelante; si no es que no son unificables. Si el predicado concuerda, comenzamos a comparar los argumentos. Si el primero de ellos coincide en ambos literales, continuamos con el siguiente... y así hasta completar todos los argumentos. Como resulta obvio, ambos literales deben tener el mismo número de argumentos.

Para conseguir que cada argumento de un literal sea coincidente con su homólogo en el otro literal, debemos buscar una sustitución que nos permita emparejarlos. La única condición que debe reunir esta sustitución es que ha de aplicarse a todo el literal, es decir, que la sustitución afecta a todo el literal, y no sólo al argumento en cuestión. Por decirlo de una manera sencilla, las sustituciones se van arrastrando a lo largo del proceso de unificación.

Describamos a continuación los pasos básicos del algoritmo de unificación:

Tomamos como entrada dos cláusulas, R y S.

1. Si R = S entonces R y S son unificables.
2. Si no, localizar el símbolo más a la izquierda de R que se diferencia de su homólogo en S

1. Si es el primero (predicado), entonces R y S no son unificables.
2. Si es uno de los argumentos, entonces sean t₁, t₂ los términos en los que difieren.

1. Si ninguno de los dos (t₁, t₂) es una variable, entonces las cláusulas no son unificables. Tampoco lo serán si siendo uno de ellos una variable, está presente en las variables del otro.
2. Si t₁ es una variable x y no está entre las variables del otro t₂, entonces haremos la sustitución: s = {x/t₂}

3. Volver al paso 1.

A partir del algoritmo de unificación podemos extraer las siguientes conclusiones:

1. Podemos señalar como unificables todas aquellas cláusulas que no coincidan en su predicado y número de argumentos.
2. Antes de intentar la unificación debemos asegurarnos que no existen variables comunes en ambas cláusulas.
3. Debemos recordar siempre las condiciones que debe reunir una sustitución y que ésta debe ser única.

Una vez que hemos comprendido como funciona el algoritmo de unificación y cómo debemos especificar adecuadamente las sentencias para llevar a cabo el algoritmo de resolución por refutación, vamos a describir los pasos del mismo detenidamente.

[ÍNDICE]

El procedimiento de resolución consiste en un proceso iterativo en el cual comparamos (resolvemos), dos cláusulas llamadas cláusulas padres y producimos una nueva cláusula que se ha inferido (deducido), de ellas. Por tanto, lo que hacemos es combinar las cláusulas padres para dar lugar a una nueva cláusula, en la que podemos simplificar alguno de sus términos.

Por ejemplo, supongamos que tenemos las cláusulas siguientes (ambas verdaderas):

• invierno Ú verano (es invierno o es verano).
• Ø invierno Ú frío (hace frío o no es invierno).

Aplicando resolución, podemos combinar ambas cláusulas y obtener:

• invierno Ú verano Ú Ø invierno Ú frío.

Ahora podemos hacer una simplificación, ya que (invierno Ù Ø invierno) es una tautología, con lo que nos queda:

• verano Ú frío (es verano o hace frío).

Que también deberá ser verdadera, pues hemos seguido puntualmente todas las propiedades de la lógica de primer orden.

La resolución opera tomando dos cláusulas tales que cada una contenga un mismo literal, en una cláusula en forma positiva y en la otra en forma negativa. El resolvente se obtiene combinando todos los literales de las cláusulas padres y eliminando aquellos que se cancelan.

Si la cláusula resultante es la cláusula vacía (€), entonces es que hemos llegado a una contradicción.

Como observamos el proceso de resolución parece sencillo. Podemos resumirlo formalmente en los pasos siguientes, basados en el algoritmo de resolución lineal:

Vamos a partir de un conjunto de cláusulas. Nuestro objetivo es probar una sentencia mediante la demostración de que su negación nos lleva a una contradicción con las sentencias conocidas (es insatisfacible):

1. Convertimos todas las proposiciones a forma clausal.
2. Negamos la proposición que queremos demostrar y convertimos el resultado a forma clausal añadiendo la cláusula resultante al conjunto obtenido en el paso anterior.
3. Hasta que se encuentre una contradicción o no se pueda seguir avanzando, repetimos lo siguiente:

1. Seleccionamos dos cláusulas (cláusulas padres) que contengan un literal común pero con signos contrarios y unificamos esos dos literales.
2. Las resolvemos juntas. La cláusula resultante llamada resolvente, será la disyunción de los literales de las dos cláusulas padres, una vez realizadas las sustituciones apropiadas. El par de literales L y Ø L, que provienen de cada una de las cláusulas padres, se pueden eliminar de la resolvente.
3. Si la resolvente es la cláusula vacía, es que se ha encontrado una contradicción. Si no, añadimos la resolvente al conjunto de cláusulas disponibles.

El algoritmo que acabamos de ver está definido de una forma muy general. Sin embargo, para su uso cotidiano se pueden hacer una serie de sugerencias que, si bien en la mayoría de los casos no están basadas en aserciones infalibles, pueden facilitar el proceso general de resolución:

• Aunque no sea un criterio estricto, suele dar buenos resultados comenzar a resolver por las cláusulas de mayor tamaño, es decir, las que poseen mayor número de literales.
• La cláusula resolvente se añade al conjunto de cláusulas disponible y, en teoría, se puede continuar el proceso tomando dos cláusulas padre cualesquiera. Sin embargo, al igual que en el caso anterior, suele dar buen resultado continuar el proceso de resolución a partir de la nueva cláusula resultante.
• De igual forma, aunque no existe ninguna limitación en cuanto al número de veces que se puede usar una cláusula para resolver, se recomienda probar primero a no usar dos veces la misma cláusula antes de usar todas las cláusulas disponibles.
• Si es posible llegar a la cláusula vacía resolviendo únicamente con las cláusulas del conjunto inicial sin usar en ningún momento la o las cláusulas provenientes de la hipótesis, es porque existe una inconsistencia dentro del conjunto inicial de cláusulas. Ésta puede ser una forma de detectar errores en el diseño de la base de conocimiento.
• Si en la cláusula resolvente existen dos literales iguales, ésta se puede simplificar eliminando uno de los dos literales. Puede ser necesaria una sustitución previa a fin de que esos literales sean unificables y, por tanto, completamente iguales.
• No es necesario usar todas las cláusulas en el proceso de resolución. En la mayoría de los casos basta con usar algunas de las cláusulas de la base de conocimiento y alguna o algunas de las cláusulas proveniente de la hipótesis.

[ÍNDICE]