**IAIC** Introducción a la Lógica De la Lógica Proposicional a la Lógica de Primer Orden En este tema vamos a intentar dar un curso acelerado (aceleradísimo) de **Lógica Proposicional** y **Lógica de Primer Orden** y veremos de qué forma se pueden automatizar algunos de los problemas más habituales que se presentan dentro de ellas. Debido a que es un curso acelerado, no se debe buscar aquí una formalización exhaustiva acerca del tema, sino una aproximación intuitiva a cuáles son sus fundamentos, los problemas que resuelve, y algunos de los algoritmos más habituales para automatizar sus soluciones. Si el lector sabe algo de lógica lo más probable es que estas notas no le sirvan de mucho y que encuentre muchas carencias (e incluso alguna *mentira piadosa*, aunque preferimos llamarlas *atajos*), pero el objetivo que perseguimos aquí es acercar de forma ligera toda una rama fundamental de las matemáticas a alumnos que apenas han tenido contacto con la lógica formal. !!!note Para una visión más completa de la lógica, se puede visitar el material del curso [Lógica Informática](http://www.cs.us.es/cursos/liti/) que se imparte en diversos grados de la E.T.S. Ingeniería Informática de la Universidad de Sevilla, así como las referencias bibliográficas que se pueden encontrar en ellos. Estas notas son un resumen (una poda algo torpe) del contenido de esos cursos. # Lógica ¿Qué son la Lógica Proposicional y la Lógica de Primer Orden? Antes de responder a esta pregunta, vamos a definir un poco el contexto en el que nos moveremos: qué es la lógica en general. !!!def: Lógica La **Lógica** es la rama del conocimiento que se encarga de estudiar las formas en que se pueden inferir verdades de una forma válida. La visión matemática de la Lógica (lo que se llama **Lógica Matemática**) añade toda la capa de formalismo necesaria para disponer de un lenguaje adecuado y de los métodos precisos para que este estudio tenga un soporte de validez universal. En este sentido, se pueden dar diversos formalismos para afrontar este gran problema de la inferencia válida, y la **Lógica Proposicional** fue, posiblemente, el primer intento serio al que se dio forma, por allá en tiempos de la famosa Grecia Clásica. Pese a su indudable utilidad, debido a las limitaciones que presentaba (y de las que hablaremos más adelante) los matemáticos ampliaron esta Lógica inicial para incluir mayor capacidad expresiva, lo que se formalizaría en la **Lógica de Primer Orden**. Todos estos sistemas intentan, de una u otra forma, enfrentarse al problema de poder *asegurar cuándo, dada una base de conocimientos que se suponen ciertos, podemos confirmar que una afirmación es necesariamente cierta*... de forma coloquial, cuándo podemos deducir que una cierta afirmación se deduce de los hechos observados (o supuestos). En particular, se enfrentan a este problema definiendo: 1. De qué forma se pueden representar los hechos y afirmaciones; es decir, proporcionando un lenguaje formal. 2. Qué entendemos por *afirmación cierta*. 3. Qué reglas podemos utilizar para garantizar la corrección de las deducciones que seamos capaces de obtener. # Lógica Proposicional ## Sintaxis y Semántica !!!def: Lógica Proposicional En el caso de la **Lógica Proposicional** (**LP**), las expresiones que podemos escribir con su lenguaje pueden tener dos posibles valoraciones o evaluaciones: **verdad** o **mentira** (que, habitualmente, notaremos respectivamente por $V|F$, $T|F$, o $1|0$), y permiten usar los siguientes símbolos para poder expresar las afirmaciones del mundo: 1. Un conjunto infinito (pero numerable) de símbolos, que llamaremos **variables proposicionales**: $p$, $q$, $r$, $s$, ..., $p_1$, $p_2$,... 2. Una serie de conectivas que permiten combinar esos símbolos de forma adecuada: $\neg$, $\vee$, $\wedge$, $\rightarrow$ y $\leftrightarrow$, que se corresponden, respectivamente, con la **negación** (*no*...), **disyunción** (...*o*...), **conjunción** (...*y*...), **implicación** (*si ... entonces...*), y **doble implicación** (...*si y sólo si*...). 3. Un par de **símbolos auxiliares**, $($ y $)$, para facilitar la escritura de las expresiones.  Igual que en cualquier otro lenguaje, no vamos a admitir como correcta cualquier combinación de los símbolos anteriores, y llamaremos **fórmulas** a aquellas expresiones que sí sean correctas en nuestro sistema. !!!tip Por ejemplo: $(p \rightarrow q) \vee (\neg q \wedge r)$ es una fórmula correcta, mientras que $p \neg \wedge q$ no lo es. Se puede dar una definición formal de qué es una fórmula (es decir, una expresión que está correctamente escrita) y qué no lo es, pero con la idea intuitiva es suficiente para este curso acelerado. Basta tener en cuenta que una expresión es una fórmula si se puede construir usando las conectivas anteriores junto con las variables proposicionales. De esta forma, las variables proposicionales representarán las afirmaciones atómicas del mundo real (o el que estamos formalizando), es decir, aquellas afirmaciones que no pueden ser descompuestas en afirmaciones más pequeñas; y las fórmulas no atómicas representarán afirmaciones compuestas. De igual forma, podemos definir formalmente cuándo una fórmula es una subfórmula de otra. El significado de las conectivas es el esperado en el lenguaje natural, aunque para determinar sin lugar a dudas su significado es habitual dar las tablas de verdad de las conectivas en función de la veracidad de las variables (o subfórmulas) que intervienen: | $p$ | $q$ | $\neg\ p$ | $\neg\ q$ | $p\land q$ | $p\lor q$ | $p\rightarrow q$ | $p\leftrightarrow q$ | | ---- | ---- | --------- | --------- | ---------- | --------- | ---------------- | -------------------- | | $1$ | $1$ | $0$ | $0$ | $1$ | $1$ | $1$ | $1$ | | $1$ | $0$ | $0$ | $1$ | $0$ | $1$ | $0$ | $0$ | | $0$ | $1$ | $1$ | $0$ | $0$ | $1$ | $1$ | $0$ | | $0$ | $0$ | $1$ | $1$ | $0$ | $0$ | $1$ | $1$ | Observa que las variables proposicionales no tienen un valor fijo de verdad, sino que, como su nombre indica, son variables que pueden tomar cualquiera de los dos valores posibles. Cuando tenemos una fórmula y prefijamos los valores de las variables que intervienen en ella, decimos que tenemos una **valoración**, **asignación**, o **interpretación**. Aplicando de forma iterada las reglas de la tabla anterior sobre la construcción de una fórmula, se puede obtener el valor de verdad de la fórmula compuesta. !!!tip Por ejemplo, si la valoración $v$ asigna $v(p)=v(q)=1,\ v(r)=v(s)=0$, entonces el valor de $\neg(\neg(p\lor q)\lor (\neg r\lor s))$ es $1$, ya que:  !!!note A pesar de que la Lógica Proposicional presenta claras limitaciones expresivas y no puede reflejar fielmente muchas de las afirmaciones que podemos hacer en sistemas un poco más ricos, suele ser más que suficiente para muchísimos problemas de la vida real, por lo que sigue siendo útil en campos como el de la Inteligencia Artificial. Además, muchos de los métodos que se utilizan en lógicas más potentes (como la **Lógica de Primer Orden**, la **Lógica Modal**, la **Lógica Difusa**, etc.) son extensiones de los métodos que se han definido para la Lógica Proposicional, por lo que su estudio en profundidad está más que justificado. ## Deducción Una vez que hemos explicitado el lenguaje que usamos para formalizar las afirmaciones, y fijado lo que entendemos por su significado (de verdad o falsedad), es el momento de formalizar qué entendemos por **inferir correctamente**: !!!def:Satisfactibilidad Algunas definiciones necesarias para el tratamiento de la inferencia son: * Dada una valoración, $v$, diremos que una fórmula, $F$, es **válida** en $v$ si el valor de verdad de $F$ con esa valoración es $1$, $v(F)=1$, y lo notaremos $v\models F$. * Decimos que $F$ es una **Tautología** si siempre es válida, sea cual sea la valoración considerada. * Decimos que es **Insatisfactible** (o una **Contradicción**) cuando nunca es válida, y decimos que es **Satisfactible** si es válida al menos una vez. Los mismos conceptos se pueden aplicar a conjuntos de fórmulas, y no solo a fórmulas aisladas (en este caso, un conjunto de fórmulas es satisfactible si existe una valoración que hace simultáneamente válidas a todas las fórmulas del conjunto). !!!Tip Por ejemplo, la fórmula $p\vee \neg p$ es una tautología, mientras que la fórmula $p\rightarrow q$ es satisfactible porque existen valoraciones que la hacen válida, pero no es tautología porque no lo hacen todas. !!!note Además, **tenemos un método automático para saber si una fórmula es satisfactible**, **tautología** o **insatisfactible**, basta hacer la tabla de verdad de la fórmula y verificar si en el resultado hay algún $1$, si todos son $1$, o si todos son $0$ (respectivamente). El problema evidente es que es un proceso muy laborioso hacer la tabla de verdad de la fórmula cuando el número de variables que intervienen es alto (algo que suele ocurrir en los problemas del mundo real que son interesantes), ya que si tenemos $n$ variables en la fórmula, necesitaremos una tabla de verdad con $2^n$ casos distintos. Aunque no profundizaremos en demasía, es obligatorio decir aquí que el problema de saber si una fórmula es satisfactible (que se denomina **SAT**) cae dentro de los que se denominan problemas **NP**,... esencialmente, aquellos problemas para los que se conoce solución, pero es tan mala desde el punto de vista de los recursos que necesitamos para resolverlos (en tiempo o en espacio) que son **intratables** desde un punto de vista práctico cuando el tamaño del problema (el tamaño de la fórmula) es grande. Es más, no solo es NP, sino que además es **NP-completo**, lo que significa que está entre los más complejos de los más complejos. Cuidado que no estamos diciendo que no tengan solución más sencilla, sino que ahora mismo no se conoce una solución sencilla, solo soluciones malas (la impresión general es que no existen esas soluciones buenas para este tipo de problemas, aunque todavía no hemos sido capaces de probarlo). Por ello, las soluciones que veremos más adelante relacionadas con SAT conseguirán facilitar la solución en algunos casos, pero nunca serán suficientemente buenas en todos los casos como para considerarlas óptimas. Ahora ya podemos decir qué entendemos por consecuencia lógica que, como veremos, y la intuición dice, está íntimamente relacionado con la idea de implicación: !!!def:Consecuencia Lógica *Diremos que una fórmula, $F$, es **consecuencia lógica** de un conjunto de fórmulas, $U=\{F_1,\dots,F_n\}$, y lo notaremos por $U\models F$, si se verifica que la fórmula $F_1\wedge \dots \wedge F_n \rightarrow F$ es una tautología.* !!!note: Reducción al absurdo Como hemos dicho, la idea fundamental es la intuición de que la consecuencia lógica se relaciona, obviamente, con la implicación. Pero además, se puede probar (aunque no lo haremos) que *la definición anterior es equivalente a decir que el conjunto $\{F_1,\dots,F_n,\neg F\}$ es insatisfactible (una contradicción)*, que viene a reflejar el método habitual de probar que algo es consecuencia lógica por medio de la **reducción al absurdo** (si suponemos lo contrario, llegamos a una contradicción). Al reducir la consecuencia lógica a comprobar una tautología o una satisfactibilidad, los métodos que tengamos para estos problemas podrán ser aplicados directamente para poder resolver el problema de la inferencia. Por tanto, ya tenemos un método, el de las tablas de verdad, para resolverlo, pero es un método demasiado primitivo e ineficiente para lo que buscamos, así que en lo que sigue nos centraremos en buscar algunos otros métodos más elegantes, y sobre todo que nos proporcionen un mayor control para adaptarnos a las características particulares de la fórmula. ## Formas Clausales Los métodos que vamos a ver aquí se podrán aplicar a fórmulas que estén escritas de una cierta forma, que se llama **forma clausal**. Para ello, necesitamos previamente el concepto de **literal**, que simplemente será una variable proposicional o la negación de una variable proposicional (por ejemplo, $p$, $\neg p$, ...). En general, si tenemos que $L$ es un literal, notaremos por $L^c$ al literal contrario (es decir, si $L=p$, entonces $L^c=\neg p$, pero si $L=\neg p$, entonces $L^c= p$). !!!def:Forma Clausal Una fórmula se dice que está en **forma clausal** (también llamada **Forma Normal Conjuntiva**) si es conjunción de disyunciones de literales, es decir: $$F = (L_{11}\vee \dots \vee L_{1n_1}) \wedge (L_{21}\vee \dots \vee L_{2n_2}) \wedge \dots \wedge (L_{m1}\vee \dots \vee L_{mn_m})$$ donde los $L_{ij}$ son literales. !!!Tip Por ejemplo: $(p \lor q \lor \neg r) \land (\neg p \lor \neg q) \land (q\lor r)$ Lo interesante es que se puede probar que cualquier fórmula se puede convertir en otra equivalente (es decir, que *dice* lo mismo, que tiene la misma tabla de verdad) expresada en forma clausal (o forma normal conjuntiva), por lo que los métodos que veamos a continuación se pueden aplicar a cualquier fórmula, siempre y cuando se transforme previamente a esta forma. En realidad, debido a que la fórmula se ha expresado como una conjunción de disyunciones, podemos considerar que estamos trabajando con un conjunto de $m$ disyunciones, a cada disyunción se le llama **cláusula**. Por ello, podemos hablar de la forma clausal de una fórmula o de un conjunto de fórmulas, que pasaría a ser: $$F = \left\{\{L_{11},\dots, L_{1n_1}\},\ \{L_{21},\dots,L_{2n_2}\},\dots,\{L_{m1},\dots,L_{mn_m}\}\right\} $$ Aunque no lo vamos a usar, también se puede escribir cualquier fórmula en **Forma Normal Disyuntiva**, es decir como una disyunción de conjunciones. !!!def:Leyes de Transformación Las leyes habituales que nos permiten transformar una fórmula cualquiera en una equivalente en **Forma Normal Conjuntiva** o **Forma Normal Disyuntiva** son: 1. Eliminar los bicondicionales usando la equivalencia:$$A\leftrightarrow B \equiv (A\rightarrow B)\wedge (B\rightarrow A)$$ 2. Eliminar los condicionales usando la equivalencia: $$A\rightarrow B \equiv \neg A \vee B$$ 3. Interiorizar las negaciones usando las equivalencias: $$\neg (A\wedge B) \equiv \neg A \vee \neg B$$ $$\neg (A\vee B) \equiv \neg A \wedge \neg B$$ $$\neg \neg A \equiv A$$ 4. Interiorizar las disyunciones usando la equivalencia (para obtener FNC): $$A\vee(B\wedge C) \equiv (A\vee B)\wedge (A\vee C)$$ 5. Interiorizar las conjunciones usando la equivalencia (para obtener FND): $$A\wedge(B\vee C) \equiv (A\wedge B)\vee (A\wedge C)$$ ## DPLL **DPLL** es un algoritmo para decidir la satisfactibilidad de una fórmula (o conjunto de fórmulas) a partir de su forma clausal. Fue propuesto en 1960 por Davis y Putnam, y posteriormente refinado en 1962 por Davis, Logemann y Loveland (de ahí el nombre completo del algoritmo, DPLL). Este algoritmo es la base de la mayoría de los programas que resuelven el problema SAT y que se usan en entornos profesionales. !!!def: DPLL El **algoritmo DPLL** consta de dos partes bien diferenciadas que se van alternando en caso de necesidad: 1. **Propagación de unidades**, simplifica el conjunto de cláusulas sobre el que se trabaja. Si existe alguna cláusula unitaria, se elige una de ellas, $L$, y se aplican consecutivamente las dos reglas siguientes (y se repite mientras queden cláusulas unitarias): 1. **Subsunción unitaria**. Se eliminan todas las cláusulas que contengan el literal $L$ (incluida la propia cláusula $L$). 2. **Resolución unidad**. Se elimina el literal complementario, $L^c$ de todas las cláusulas en las que aparezca. 2. **División**, si no hay unidades que propagar en el conjunto actual, $S$, se elige un literal $L$ que aparezca en una de las cláusulas que permanecen y se consideran por separado los conjuntos de cláusulas: $S\cup \{L\}$ y $S\cup \{L^c\}$. A continuación aplicamos recursivamente el procedimiento a ambos conjuntos (que ya tienen las cláusulas unitarias que acabamos de introducir). El algoritmo va ramificando el proceso y cada rama puede ser una solución al problema de la satisfactibilidad. Si en una rama aparece una contradicción (una cláusula unitaria y su cláusula complementaria de forma simultánea), esa rama no proporciona una solución, pero podría haber otra rama que sí lo hiciera. Si en una rama no aparece una contradicción, esa rama proporciona una valoración que hace satisfactible la forma clausal original. Si todas las ramas son contradictorias, la forma clausal original es una contradicción. Además, si consideramos todas las posibles ramas qu genera el algoritmo, obtenemos todos los posibles modelos de la fórmula. !!!Tip Veamos un ejemplo de cómo aplicar este algoritmo:  En el ejemplo anterior, la rama derecha proporciona un modelo ($p=0,\ q=0,\ r=1$), por lo que la fórmula es satisfactible; mientras que las ramas izquierdas llegan a contradicción (ya que requieren que sean simultáneamente ciertas $r$ y $\neg r$) y no proporcionan modelos. Como al menos una rama proporciona modelos, la fórmula original es satisfactible. Si ninguna rama proporcionara modelos (en todas llegaríamos a una contradicción), entonces la fórmula sería insatisfactible. Como la fórmula tiene $3$ variables, podría llegar a tener $2^3=8$ modelos distintos, pero solo tiene $1$, por lo que no es tautología. En cierta forma, este algoritmo es como el método habitual para resolver un sudoku, si tenemos ya algunos números seguros, su conocimiento se propaga a través del sudoku y nos permite asegurar más posiciones, y si llegamos a un callejón sin salida lo más normal es hacer suposiciones acerca de alguna de las casillas, valorando cómo evoluciona el puzzle para cada uno de sus posibles valores. !!!note:Aplicación a la Consecuencia Lógica En resumen, si queremos resolver el problema de saber si una cierta fórmula es consecuencia lógica (la podemos deducir) de un conjunto de fórmulas (hipótesis), formalmente, $\{F_1,\dots,F_n\}\models F$, los pasos a seguir serían: 1. Convertimos el problema en **verificar si $\{F_1,\dots,F_n,\neg F\}$ es satisfactible o no**, es decir, si somos capaces de encontrar un modelo para esas fórmulas o no. 2. **Pasamos cada una de esas fórmulas a forma clausal** (FNC) aplicando las reglas habituales para ello (ley distributiva, asociativa, de Morgan, etc). Podemos hacerlo por separado para cada fórmula y después simplemente consideramos el conjunto de todas las cláusulas obtenidas por todas las fórmulas: $\{C_1,\dots,C_m\}$. 3. **Aplicamos DPLL** al conjunto de cláusulas obtenido. 4. **Si encontramos un modelo** (con **DPLL**, una de las ramas obtiene una solución que no es contradicción), **entonces la consecuencia lógica NO es cierta**, $F$ no se deduce de $\{F_1,\dots,F_n\}$ (no significa que $F$ no sea cierta, sino que no es consecuencia de las demás). 5. **Si no encontramos un modelo** (con **DPLL**, todas las ramas llegan a una contradicción), **entonces la consecuencia lógica SÍ es cierta**, $F$ se deduce de las demás. ## Sobre la automatización Aunque en general los algoritmos que existen para obtener nuevos resultados matemáticos no son automatizables (es decir, no se pueden programar en una máquina), el caso de la lógica proposicional, con todas sus limitaciones, sí que se puede automatizar. Ya vimos que el método más directo, y el más incómodo, para ello es el de la creación de la tabla de verdad. Pero hemos visto otro algoritmo que es fácilmente implementable (apenas usando algunas estructuras de listas o similares) y que puede resultar más recomendable en caso de querer disponer de una implementación práctica. A pesar de todo, no debemos olvidar que el problema que está detrás es **SAT**, y que es un problema **NP**-completo, por tanto no debemos poner nuestras esperanzas en conseguir algoritmos que rebajen el problema de la inferencia (ni siquiera en la Lógica Proposicional) y que lo convierta en un problema tratable para todos los casos, y nos conformamos con obtener métodos que sean suficientemente buenos como para poder atacar problemas con gran número de variables en muchos casos. # Lógica de Primer Orden Pese a las virtudes que ofrece un sistema de representación y razonamiento formal como la Lógica Proposicional (LP), esta puede no ser apropiada para expresar ciertos tipos de conocimiento. Por ejemplo, una sentencia tan sencilla como: