LÓGICA MATEMATICA.
Dado que el Lenguaje Natural, aunque es potente, resulta muy ambiguo, nos interesa encontrar un lenguaje mas sencillo, sin ambigüedades que nos permita realizar razonamientos y generalizaciones. Por ello, es necesario introducirnos en la formalización del Calculo Proposicional, que, aunque no cuenta con toda la potencia necesaria para describir el mundo, es valido como primera aproximación. También veremos algunos conceptos delCalculo de Predicados y, por supuesto, nos centraremos en definir y ver cómo funciona el Método de Resolución.
Conceptos basicos.
Para comprender los principios de la lógica matematica en el campo del Calculo Proposicional, necesitamos conocer una serie de conceptos basicos que se describen a continuación:

* Atomo: 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 mas simples. Para denotar atomos se utilizan las letras p,q, r, etc.
* Conectiva: Operador que permite construir sentencias compuestas a partir de atomos. Las principales conectivas lógicas son: Ø , Ù , Ú , ® .
* Enunciado: También llamado Fórmula. Es una expresión realizada con atomos 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 sellaman 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 automatico de teoremas que es, justamente, en lo que consiste la maquina PROLOG.
Aunque mediante la Lógica Proposicional podemos describir muchas situaciones, existen otras imposibles de representar. Necesitamos introducirnos, ademas, 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 explicaran en apartados posteriores.
* Símbolos: Existen varios tipos:
* Individuales o Constantes: Representan valores concretos. C=.
* Variables: Se pueden sustituir por constantes. V=.
* Funciones: Aplicación que asocia una serie de constantes con otra constante. F=.
* Predicados: Función de resultado Verdadero o Falso. Pred=.
* 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 t1, t2  tn son términos, entonces f (t1, t2,,, tn) 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 t1, t2  tn son términos, entonces R (t1, t2,,, tn) es una fórmula.
Ejemplo: |
f(a, x) Ù Ø g(x), ' x (g(x) Ú a) ® [f(a, v) ÙP(b Ú c)] |
 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.
Ejemplo:
[' x (g(x) Ú a) ® (f(a, v) Ù P(b Ú c))] Ú Ø (f(a, x) Ù Øg(z)) |
Sentencias: Se definen como fórmulas en las que ninguna de las variables que la componen tiene una o mas 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 esta inmediatamente después de un símbolo ' ó $ .
2. La variable x esta en el radio de acción de un cuantificador ' x ó $ x
El radio de acción de uncuantificador 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.
Ejemplos: |
' x (f(x) Ú g(z)). El cuantificador abarca a f(x) y g(z).' x h(x) Ú f(a, v, x). El cuantificador abarca sólo a h(x). |
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.
Ejemplo: |
' x [P(g(x)) Ú R(a)] ® [f(a, v) Ù Q(b Ú c)] |
 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=. De dicha definición podemos concluir dos cosas:
* Sólo son validas 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.
*

Ec 1
Resolución y unificación. Métodos.
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 sintactico donde sólonos 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 facil representar hechos del mundo real mediante la lógica proposicional y mediante la lógica de predicados. Ademas 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 maquina 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, esdecir, 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: sistematica, 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 clausulas 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.

Conversión a forma clausal.
El proceso de conversión a forma clausal consiste en transformar las sentencias y fórmulas en clausulas, cuya principal característica, al nivel de representación, es la ausencia casi total de símbolos de relación. En una clausula sólo apareceran disyunciones 'Ú '.
De esta manera, el primer paso sera 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 clausulas. Así, podemos definir una clausula, mas 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 transformaremosa Funciones de Skolem.
3. Finalmente llegaremos a una representación en Forma de Clausulas.

Forma Prenexa
Una fórmula esta en Forma Normal Prenexa si es de la forma: Q1x1QnxnY donde Y es una fórmula desprovista de cuantificadores y escrita como conjunción de disyunciones, Q1,,Qn Î  y x1,, xn son variables.
Ejemplos: |
' x ' y $ z ' v [(R(x) Ú T(y)) Ù Q(v, z)]' x $ y (R(x, y) Ù Q(b, z))' x P(x, y) |
 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 ambito 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.
Ejemplos: |
' x P(x) Ú ' x Q(x) º ' y P(y) Ú ' x Q(x)' x [P(x) Ú Q(x)] Ù ' y R(y) Ú Q(x) º ' z[P(z) Ú Q(z)] Ù ' y R(y) Ú Q(x) |
 Mover todos los cuantificadores a la izquierda de la fórmula sin cambiar su orden relativo.
Ejemplos: |
' x P(x) Ú ' x Q(x)' y ' x [P(y) Ú Q(x)](' x R(x) Ú ' y T(y)) Ù $ z ' v Q(v Ú z)' x ' y $ z' v [(R(x) Ú T(y)) Ù Q(v Ú z)] |
 
Funciones de Skolem
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 Skolemelimina los cuantificadores existenciales.
Partimos de una fórmula: Q1x1QnxnY. 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 Qr un cuantificador existencial:
* Si no hay ningún cuantificador universal antes de Qrxr, elegir una nueva constante c distinta de todas las que aparecen en Y, y reemplazar cada ocurrencia de xr en Y por c. Borrar Qrxr del prefijo de la fórmula.
* Si Qs1, Qs2  Qsk son los cuantificadores universales que aparecen antes de Qrxr, tomar un nuevo símbolo de función f distinto a todos los que aparecen en Y y reemplazar cada ocurrencia de xr porf(xs1,xs2,,xsk). Borrar Qrxr del prefijo de la fórmula.
Ejemplos: |
1. Supongamos que tenemos:' x ' y $ z [(R(x) Ú P(y)) Ù Q(b, z)]nos queda como' x ' y [(R(x) Ú P(y)) Ù Q(b, f(x, y))] 2. Supongamos la siguiente sentencia:$ x ' y $ w [R(a,w) Ú P(y) Ú P(f(x))]sustituimos x por c (caso 1): ' y $ w [R(a, w) Ú P(y) ÚP(f(c))]sustituimos w por g(y) (caso 2): ' y [R(a, g(y)) Ú P(y) ÚP(f(c))] |
 
* Representación en forma de clausulas: El último paso sera convertir las funciones de Skolem a clausulas. Tenemos las fórmulas cuantificadas universalmente, entonces podemos eliminar todos los prefijos, de tal manera que la fórmula resultante esta 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 clausula: (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 clausula.
Ejemplo: |
Vamos a partir de la sentencia:' x [(R(x) Ú C(x, a)) Ù [O(x, b) Ú ($ y($ z O(y, z) ® L(x,y)))]]Paso 1: Eliminamos los símbolos de implicación:' x [(R(x) Ú C(x, a)) Ù [O(x, b) Ú ($ y(Ø $ z O(y, z) Ú L(x,y)))]]Paso 2: Reducimos el ambito de las negaciones:' x [(R(x) Ú C(x, a)) Ù [O(x, b) Ú ($ y(' z Ø O(y, z) Ú L(x,y)))]]Paso 3: En este caso no es necesario normalizar las variables de los cuantificadores por lo tanto pasamos al paso siguientePaso 4: Movemos los cuantificadores a laizquierda:' x $ y ' z [(R(x) Ú C(x, a)) Ù (O(x, b) Ú (Ø O(y, z) Ú L(x,y)))]Paso 5: Eliminamos los cuantificadores existenciales:' x ' z [(R(x) Ú C(x, a)) Ù (O(x, b) Ú (Ø O(s(x), z) Ú L(x, s(x))))]Paso 6: Eliminamos todos los cuantificadores: [(R(x) Ú C(x, a)) Ù (O(x, b) Ú (Ø O(s(x), z) Ú L(x, s(x))))]Paso 7: Separar una clausula por cada conjunción:(R(x) Ú C(x, a))(O(x, b) Ú (Ø O(s(x), z) Ú L(x, s(x)))) |

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 basica 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 encuestión. Por decirlo de una manera sencilla, las sustituciones se van arrastrando a lo largo del proceso de unificación.
Ejemplo: |
Vamos a unificar P(x, x) con P(y, z): * Primera sustitución: (y/x)Resultado: P(y, y) P(y, z) * Segunda sustitución: (z/y)Resultado: P(z, z) P (z, z)La sustitución resultante es la composición de las sustituciones: s = |
 
Describamos a continuación los pasos basicos del algoritmo de unificación:
Tomamos como entrada dos clausulas, R y S.
1. Si R = S entonces R y S son unificables.
2. Si no, localizar el símbolo mas 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 t1, t2 los términos en los que difieren.
1. Si ninguno de los dos (t1, t2) es una variable, entonces las clausulas no son unificables. Tampoco lo seran si siendo uno de ellos una variable, esta presente en las variables del otro.
2. Si t1 es una variable x y no esta entre las variables del otro t2, entonces haremos la sustitución: s =
3. Volver al paso 1.
A partir del algoritmo de unificación podemos extraer las siguientes conclusiones
a. Podemos señalar como unificables todas aquellas clausulas que no coincidan en su predicado y número de argumentos.
b. Antes de intentar la unificación debemos asegurarnos que no existenvariables comunes en ambas clausulas.
c. Debemos recordar siempre las condiciones que debe reunir una sustitución y que ésta debe ser única.
Ejemplo: |
Unificación de las sentencias R (x, f(g(x)), a) y R (b, y, z)Términos desiguales Sustitución Resultado t1 = x t2 = b x/b - R(b, f(g(b)), a) , R(b, y, z) t1 = f(g(b)) t2 = y y/f(g(b)) - R(b, f(g(b)), a), R(b, f(g(b)), z) t1 = a t2 = z z/a - R(b, f(g(b)), a) , R(b, f(g(b)), a)Las dos clausulas son unificables y la sustitución resultante es: s = |
 
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.

Algoritmo de Resolución
El procedimiento de resolución consiste en un proceso iterativo en el cual comparamos (resolvemos), dos clausulas llamadas clausulas padres y producimos una nueva clausula que se ha inferido (deducido), de ellas. Por tanto, lo que hacemos es combinar las clausulas padres para dar lugar a una nueva clausula, en la que podemos simplificar alguno de sus términos.
Por ejemplo, supongamos que tenemos las clausulas 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 clausulas 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 debera ser verdadera, pues hemos seguido puntualmente todas las propiedades de la lógica de primer orden.
La resolución opera tomando dos clausulas tales que cada una contenga un mismo literal, en una clausula en forma positiva y en la otra en forma negativa. El resolvente se obtiene combinando todos los literales de las clausulas padres y eliminando aquellos que se cancelan.
Si la clausula resultante es la clausula 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 clausulas. 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 clausula 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 clausulas (clausulaspadres) que contengan un literal común pero con signos contrarios y unificamos esos dos literales.
2. Las resolvemos juntas. La clausula resultante llamada resolvente, sera la disyunción de los literales de las dos clausulas padres, una vez realizadas las sustituciones apropiadas. El par de literales L y Ø L, que provienen de cada una de las clausulas padres, se pueden eliminar de la resolvente.
3. Si la resolvente es la clausula vacía, es que se ha encontrado una contradicción. Si no, añadimos la resolvente al conjunto de clausulas disponibles.
El algoritmo que acabamos de ver esta 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 estan 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 clausulas de mayor tamaño, es decir, las que poseen mayor número de literales.
* La clausula resolvente se añade al conjunto de clausulas disponible y, en teoría, se puede continuar el proceso tomando dos clausulas 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 clausula resultante.
* De igual forma, aunque no existe ninguna limitación en cuanto al número de veces que se puedeusar una clausula para resolver, se recomienda probar primero a no usar dos veces la misma clausula antes de usar todas las clausulas disponibles.
* Si es posible llegar a la clausula vacía resolviendo únicamente con las clausulas del conjunto inicial sin usar en ningún momento la o las clausulas provenientes de la hipótesis, es porque existe una inconsistencia dentro del conjunto inicial de clausulas. Ésta puede ser una forma de detectar errores en el diseño de la base de conocimiento.
* Si en la clausula 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 clausulas en el proceso de resolución. En la mayoría de los casos basta con usar algunas de las clausulas de la base de conocimiento y alguna o algunas de las clausulas proveniente de la hipótesis.
Ejemplo: |
A partir de la base de conocimiento siguiente, compuesta por 5 clausulas, aplicar resolución para demostrar que la hipótesis V(z) es cierta:P(x) Ú Q(c, x) Ú Ø S(y, x) y P(a) Ú Ø R(z) Ú S(b, a) y Ø Q(z, a) Ú V(a) y R(x) Ú V(y) yØ P(y) Ú Q(x, y)Ya tenemos las proposiciones en forma de clausulas, luego sólo nos falta agregar la hipótesis, transformarla en clausula y añadirla al conjunto de sentencias anterior:V(z) negada nos queda Ø V(z).(Como vemos esta en forma de clausula).Dado que las sustituciones afectan a todas las ocurrencias de la variable que se pretende sustituir en toda la base de conocimientos, si queremos que dicha sustitución afecte a muchas ocurrencias de una variable podemos intentar renombrarlas. Pero para evitar tener todas las variables renombradas y, por tanto, evitar la complicación del procedimiento, estableceremos un uso especial de las sustituciones. Sólo afectaran a las clausulas padres en el momento de la resolución, y a la clausula resolvente, quedando el resto inalteradas.Comenzamos el proceso por las clausulas de mayor tamaño:P(x) Ú Q(c, x) Ú Ø S(y, x) y P(a) Ú Ø R(z) Ú S(b, a) con la sustitución s = nos queda:P(x) Ú Q(c, x) Ú Ø S(y, x) Ú P(a) Ú Ø R(z) Ú S(b, a) = P(a) Ú Q(c, a) Ú Ø R(z).Combinamos la resolvente con Ø P(y) Ú Q(x, y) con la sustitución s = nos queda:P(a) Ú Q(c, a) Ú Ø R(z) Ú Ø P(y) Ú Q(x, y) = Q(c, a) Ú Ø R(z) Ú Q(x, a).Aplicamos a la resolvente la sustitución s = y nos queda:Q(c, a) Ú Ø R(z).Combinamos la resolvente con Ø Q(z, a) Ú V(a) con la sustitución s = nos queda:Q(c, a) Ú Ø R(z) Ú Ø Q(z, a) Ú V(a) = Ø R(c) Ú V(a).Combinamos la resolvente con R(x) Ú V(y) con la sustitución s = nos queda:Ø R(c) Ú V(a) Ú R(x) Ú V(y) = V(a) Ú V(y).Aplicamos la sustitución s = y nos queda V(a) que podemos combinar con Ø V(z) obteniendo la clausula vacía. |