**LITI**
Tableros Semánticos en Lógica Proposicional
En el tema anterior establecimos las bases sintácticas y semánticas que definen la Lógica Proposicional y la Lógica de Primer Orden y que serán de uso habitual a lo largo de todo el curso. En este capítulo comenzaremos a ahondar en los algoritmos de decisión más relevantes, presentando el primero de los que vamos a tratar a lo largo del temario, los **Tableros Semánticos**.
Introducción
------------
El método de los Tableros Semánticos proporciona un **algoritmo para la decisión de la satisfactibilidad de un conjunto de fórmulas sin necesidad de preprocesamiento de las fórmulas**.
Su forma de operar consiste en ir simplificando los conjuntos de fórmulas por medio de operaciones que mantienen la consistencia hasta llegar a conjuntos de literales (fórmulas que, esencialmente son variables proposicionales) cuya consistencia podemos decidir con facilidad. Además de proporcionar un mecanismo muy potente de decisión, veremos que, si el conjunto es consistente, el método informa acerca de los posibles modelos que tiene.
Además, este método se puede representar gráficamente de una forma muy sencilla y visual a través de árboles binarios que recogen todo el proceso del algoritmo.
Aunque nosotros vamos a estudiar su desarrollo para las lógicas LP y LPO, la versatilidad y sencillez del método, lo hace fácilmente adaptable a otras lógicas (descriptivas, modales, ...).
De forma un poco más concreta, el método de tableros semánticos (en adelante tableros) en LP basa su desarrollo en dos pasos fundamentales:
1. **Clasificación** de las fórmulas en dos tipos fundamentales:
* Tipo $\alpha$, que adoptan el comportamiento de conjunciones.
* Tipo $\beta$, que adoptan el comportamiento de disyunciones.
Aunque podrían verse como fórmulas $\alpha$, se distingue una tercera clase que engloba a aquellas fórmulas que se construyen por medio de la doble negación de otras.
2. **Reducción** de la satisfactibilidad de cada una de las fórmulas del conjunto a la satisfactibilidad de dos fórmulas más sencillas.
# Clasificación de fórmulas
## Fórmulas $dN$
Distinguimos esta clase aparte, ya que de este tipo de fórmulas se obtiene una única componente, en vez de 2 como veremos que ocurre para los casos $\alpha$ y $\beta$.
Esta categoría engloba únicamente a fórmulas de la forma $\neg \neg G$, de las que se deriva una sola componente, $G$ (esencialmente, la componente derivada, $G$, y la fórmula original, $\neg \neg G$, tienen la misma consistencia, algo que es trivial comprobar).
## Fórmulas $\alpha$
Esta categoría engloba a todas **aquellas fórmulas que se comportan como conjunciones** ($F : \alpha_1 \wedge \alpha_2$), y de las cuales se obtienen dos componentes ($\alpha_1$ y $\alpha_2$), de forma que la satisfactibilidad de $F$ se reduce a la satisfactibilidad simultánea de las componentes. Las construcciones que podemos clasificar como fórmulas $\alpha$ son:
| $\alpha$ | $\alpha_1$ | $\alpha_2$ |
|----------------------------|----------------------|----------------------|
| $F_1\wedge F_2$ | $F_1$ | $F_2$ |
| $\neg(F_1\vee F_2)$ | $\neg F_1$ | $\neg F_2$ |
| $\neg(F_1\rightarrow F_2)$ | $F_1$ | $\neg F_2$ |
| $F_1\leftrightarrow F_2$ | $F_1\rightarrow F_2$ | $F_2\rightarrow F_1$ |
## Fórmulas $\beta$
Esta categoría engloba a todas **aquellas fórmulas que se comportan como disyunciones** ($F : \alpha_1 \vee \alpha_2$), y de las cuales se obtienen dos componentes ($\beta_1$, $\beta_2$), de forma que la satisfactibilidad de la fórmula original se reduce a la satisfactibilidad de alguna de las componentes. Las construcciones que podemos clasificar como fórmulas $\beta$ son:
| $\beta$ | $\beta_1$ | $\beta_2$ |
|--------------------------------|----------------------------|----------------------------|
| $F_1\vee F_2$ | $F_1$ | $F_2$ |
| $\neg(F_1\wedge F_2)$ | $\neg F_1$ | $\neg F_2$ |
| $F_1\rightarrow F_2$ | $\neg F_1$ | $F_2$ |
| $\neg(F_1\leftrightarrow F_2)$ | $\neg(F_1\rightarrow F_2)$ | $\neg(F_2\rightarrow F_1)$ |
Obsérvese que las únicas fórmulas que no se pueden clasificar como ninguno de los tipos anteriores son, o bien las variables proposicionales, o bien las negaciones de variables proposicionales: $L= \{p, \neg p,q, \neg q, \dots \}$. A los elementos de este conjunto de fórmulas los llamaremos _literales_.
# Reglas de reducción en LP
Las **reglas de reducción** que veremos a continuación reducen la consistencia de un conjunto de fórmulas a la de otro conjunto formado por fórmulas más sencillas, y son aplicables a los distintos tipos de fórmulas que hemos identificado anteriormente:
!!!def:Regla $dN$
Si $(F = \neg \neg G) \in U$, entonces $U$ es satisfactible si y sólo si lo es $(U - \{F \}) \cup \{G \}$. Denotaremos la aplicación de esta regla sobre la fórmula $F$ de $U$como $dN(U,F)$.
!!!def:Regla $\alpha$
Si $F \in U$ es de tipo $\alpha$, entonces $U$ es satisfactible si y sólo si lo es $(U - \{F \}) \cup \{ \alpha_1, \alpha_2 \}$. Denotaremos la aplicación de esta regla sobre la fórmula $F$ de $U$ como $\alpha(U,F)$.
!!!def:Regla $\beta$
Si $F \in U$ es de tipo $\beta$, entonces $U$ es satisfactible si y sólo si lo es $(U - \{F \}) \cup \{ \beta_1 \}$ o lo es $(U - \{F \}) \cup \{ \beta_2 \}$. Denotaremos la aplicación de esta regla sobre la fórmula $F$ de $U$ como $\beta(U,F)$, donde $\beta(U,F)_1 = (U - \{F \}) \cup \{ \beta_1 \}$ y $\beta(U,F)_2 = (U - \{F \}) \cup \{ \beta_2 \}$.
# Algoritmo de Tableros en LP (Tableros completos)
El algoritmo siguiente determina el método automático a seguir por medio de la aplicación sucesiva de las reglas anteriores para llegar desde un conjunto $U$ inicial de fórmulas hasta conjuntos que ya no se pueden seguir simplificando (porque están formados únicamente por literales).
!!!def:Tablero Semántico
Un **tablero** para un conjunto de fórmulas $U = \{F_1, \ldots, F_n \}$ es un árbol, $T$, con nodos etiquetados con conjuntos de fórmulas, y que ha sido construido siguiendo el siguiente esquema:
1. La raíz de $T$ se etiqueta con el conjunto original $U_r = \{F_1, \ldots, F_n \}$.
2. En cada paso de construcción, si quedan hojas en $T$ no marcadas, se toma una de las hojas, $h$, con etiqueta $U_h$ y:
1. Si $U_h$ contiene una contradicción, esto es, dos fórmulas tal que una sea la negación de la otra, entonces marcar la **hoja** como **cerrada** ("╳").
2. Si no contiene contradicciones y $U_h$ está formada por literales, entonces marcar la **hoja** como **abierta** ("◯").
3. Si $U_h$ contiene alguna fórmula, $F$, de tipo $dN$ entonces añadir un nodo hijo de $U_h$ con etiqueta $U_m = dN(U_h, F)$.
4. Si $U_h$ contiene alguna fórmula, $F$, de tipo $\alpha$ entonces añadir un nodo hijo de $U_h$ con etiqueta $U_m = \alpha(U_h, F)$.
5. Si $U_h$ contiene alguna fórmula, $F$, de tipo $\beta$, entonces añadir dos hijos de $U_h$ con etiquetas $U_{m_1}= \beta(U_h, F)_1$ y $U_{m_2}= \beta(U_h, F)_2$.
Hemos dado el algoritmo en forma recursiva, y se puede probar fácilmente (por inducción) que en todos los casos el algoritmo termina ( aunque en el peor de los casos podría dar una cantidad exponencial de pasos). Al tablero producido al terminar el algoritmos se le denomina **tablero completo**, y se dice **cerrado** si todas las hojas son cerradas y **abierto** en otro caso (es decir, que haya alguna hoja abierta).
Además, el tablero construido no tiene porqué ser único, ya que en cada paso pueden aparecer varias opciones simultáneas, lo que construiría árboles distintos. El siguiente teorema nos dice que todos los posibles tableros que se pueden construir a partir de un conjunto inicial de fórmulas dan la misma información:
!!!note:Teorema de Corrección y Completitud
Dado un conjunto de fórmulas $U$ y un tablero $T$ (completo) para $U$:
1. **Corrección**. Si $T$ es cerrado, entonces $U$ es insatisfactible.
2. **Completitud**. Si $U$ es insatisfactible, entonces $T$ es cerrado.
A partir del teorema anterior concluimos que:
!!!note:Búsqueda de modelos
Un conjunto de fórmulas, $U$, admite un tablero completo abierto si y sólo si $U$ es consistente.
Así que, claramente, podemos usar este resultado para abordar el problema de la satisfactibilidad (y los relacionados).
Pero no solo nos indica si el conjunto es consistente o no, sino que cada una de las hojas abiertas $h$ (que, recordemos, están formadas por conjuntos de literales sin contradicciones) proporciona, al menos, un modelo (no necesariamente distinto) de $U$, ya que, si construimos a partir de $h$ la valoración:
$$ v_h(p) = \left \lbrace \begin{array}{ll}
v_h(p) = 1 & si \, p \in U_h \\
v_h(p) = 0 & si \, \neg p \in U_h \\
v_h(p) = 0 \, ó \, v_h(p) = 1 & e.o.c. \\
\end{array} \right. $$
Entonces, claramente, $v_h \models U$.
# Consecuencia lógica
Dada la relación (vista en el tema 1) entre consecuencia lógica e inconsistencia de conjuntos, recordemos:
!!!Recordatorio:Consecuencia Lógica
$U \models F \Leftrightarrow (U \cup \{ \neg F \})$ es inconsistente.
es sencillo dar un método para el problema de la consecuencia traduciéndolo a la obtención de un tablero cerrado de un cierto conjunto de fórmulas, de forma la respuesta será afirmativa (hay consecuencia lógica) si y sólo si el tablero (completo) es cerrado.
# Ejemplos
Los conceptos que hemos desarrollado previamente nos permiten trabajar completamente con el Método de Tableros Semánticos para su aplicación a la satisfactibilidad de conjuntos y el problema de la consecuencia. A continuación mostramos algunos ejemplos (en forma de ejercicios resueltos) con el fin de afianzar los conceptos vistos durante esta primera parte del tema:
!!!Tip:Ejemplo 1
Sea $F: p \wedge q \leftrightarrow \neg q \vee r$:
1. Construir un tablero completo para $F$ y otro para $\neg F$
2. Describir todos los modelos y contramodelos de la fórmula $F$
**_Solución_**
Tablero para $F$:
Tablero para $\neg F$:
De forma que los modelos de $F$ corresponden al conjunto de modelos dados por cada una de las hojas abiertas del tablero construido para $F$, y los contramodelos corresponderán al de los modelos dados para $\neg F$.
¡Cuidado! Las hojas abiertas proporcionan modelos, pero las cerradas **no** proporcionan contramodelos, de hecho son inconsistentes.
Los 2 modelos que obtenemos de las hojas corresponden a:
$$\{ \neg r,q, \neg p \}, \ \{p,q,r \}$$
| $p$ | $q$ | $r$ |
|-----|-----|-----|
| 0 | 1 | 0 |
| 1 | 1 | 1 |
De igual modo, los contramodelos de $F$ corresponden a los modelos de $\neg F$. Extrayendo directamente los modelos de las hojas abierta del árbol obtenemos:
$$\{p,q, \neg r \}, \ \{ \neg q, \neg p \}, \ \{ \neg q \}, \ \{r, \neg p \}, \{r, \neg q \}$$
Obsérvese que en los conjuntos de literales el número de modelos que describen para una fórmula es $2^{i}$ (donde $i$ es el número de símbolos proposicionales que no aparecen en el conjunto y sí aparecen en la fórmula), ya que, por cada variable que no aparece en el conjunto tenemos 2 opciones.
En el caso de $F$ es fácil contar 2 modelos porque los conjuntos de literales son completos y distintos (así que cada conjunto da un solo modelo y son distintos entre sí). Sin embargo, en el caso de $\neg F$ es fácil observar que hay conjuntos de literales que proporcionan los mismos modelos, por lo que dar los modelos de esta forma no es lo más adecuado. Como $F$ usa 3 variables proposicionales, el número total de modelos es $2^3=8$, ya que $F$ tiene 2 modelos, debería haber 6 contramodelos, pero las hojas de su árbol parecen indicar 1+2+4+2+2 = 11 modelos.
Es fácil observar que no son realmente modelos distintos, ya que, por ejemplo, $\{ \neg q \}$ proporciona varios modelos que ya están expresados en otros conjuntos de literales. No basta con quedarse con los conjuntos de literales más generales (por ejemplo, quitando $\{ \neg q, \neg p \}$ y $\{r, \neg q \}$ porque ya está $\{ \neg q \}$):
$$\{r, \neg p \}, \ \{ \neg q \}, \ \{p,q, \neg r \}$$
Ya que ahora siguen saliendo 2+4+1=7 modelos, porque la intersección entre los modelos que proporcionan los conjuntos de literales sigue siendo no vacía, en concreto, el modelo $\{ \neg p, \neg q, r \}$ pertenece al primer y al segundo conjunto de modelos, por tanto al hacer la suma, éste lo hemos contado 2 veces.
En conclusión, la forma más correcta y segura de dar los modelos y contramodelos es explicitándolos. En este caso, los contramodelos de $F$ (modelos de $\neg F$) serían:
| $p$ | $q$ | $r$ |
|-----|-----|-----|
| 0 | 0 | 0 |
| 1 | 0 | 0 |
| 0 | 0 | 1 |
| 1 | 0 | 1 |
| 0 | 1 | 1 |
| 1 | 1 | 0 |
Con lo que se acaba el problema propuesto.
!!!Tip:Ejemplo 2
Responde, de forma razonada, a las siguientes cuestiones usando tableros semánticos:
1. Es $(p \vee q \rightarrow r) \wedge (t \rightarrow \neg r) \wedge \neg( \neg t \rightarrow q)$ satisfactible?
2. ¿Es $(p \vee q \rightarrow r) \rightarrow ( \neg r \rightarrow \neg p)$ una tautología?
3. ¿$\{p \rightarrow q, q \rightarrow r \} \models p \rightarrow r$?
**_Solución_**
1. Según el Teorema de Compacidad y Completitud, un conjunto de fórmulas es consistente si y sólo si posee un tablero abierto. De manera que si tomamos $\{(p \vee q \rightarrow r) , (t \rightarrow \neg r) , \neg( \neg t \rightarrow q) \}$, (nótese que si este conjunto es consistente entonces las tres fórmulas lo son simultáneamente, luego $F$ lo es también). Un tablero correspondería a:
Como el tablero es abierto (tiene alguna hoja abierta), este conjunto tiene modelos, y $F$ también, luego $F$ es satisfactible.
2. Teniendo en cuenta que se tiene que una fórmula es tautología si y sólo si su negación es insatisfactible, entonces para probar que $F = (p \vee q \rightarrow r) \rightarrow ( \neg r \rightarrow \neg p)$ es tautología, basta comprobar que el tablero para $\neg F$ es cerrado (no tiene ninguna hoja abierta):
De forma que, en efecto, $\neg F$ es insatisfactible, luego $F$ es tautología.
3. Como se tiene que: $M \models F \Leftrightarrow M \cup { \neg F}$ es insatisfactible, entonces para comprobar si se da la consecuencia lógica basta comprobar que el tablero correspondiente a $\{p \rightarrow q, q \rightarrow r, \neg (p \rightarrow r) \}$ es cerrado (observa que hemos añadido la negación de lo que queremos probar). De forma que:
O, equivalentemente, el conjunto de fórmulas anterior no posee modelos, es insatisfactible, y por tanto sí se da la consecuencia lógica.