Sistemas Deductivos Proposicionales
En temas anteriores hemos visto algunos algoritmos para resolver el problema de la deducción, por ejemplo, por medio de Tableros Semánticos o DPLL, todos ellos basados en el hecho de que: $$\Sigma\models A \Leftrightarrow \Sigma \cup \{\neg A\}\mbox{ es insatisfactible}$$
Sin embargo, esta forma (que sería algo parecido a hacer una reducción al absurdo) no es la más habitual (ni más clásica) de abordar el problema de la deducción. En muchas áreas (por ejemplo, matemáticas, sitio por excelencia de la deducción formal) es más normal acudir al concepto de demostración: se parte de un conjunto de enunciados básico, $\Sigma$, que actúa como conjunto de axiomas (o hipótesis), y que asumimos como ciertos inicialmente, y un enunciado $\phi$ será consecuencia de $\Sigma$ si podemos obtener una demostración de $\phi$ a partir de $\Sigma$, es decir, una sucesión de enunciados intermedios, deducibles unos a partir de otros, desde $\Sigma$ hasta $\phi$. En este caso, en matemáticas, por ejemplo, es común decir que $\phi$ es un teorema en $\Sigma$.
Este procedimiento se formaliza por medio de lo que se conoce como un Sistema Deductivo, que proporciona las herramientas necesarias para poder construir demostraciones de una manera correcta y formal.
Un sistema deductivo, ${\mathbf T}$, (o teoría proposicional) consta de:
- Un conjunto, $Ax({\mathbf T})$, de fórmulas proposicionales que llamamos axiomas de ${\mathbf T}$.
- Reglas de inferencia de la forma:
$$\frac{A_1,\dots,A_n}{A}$$
donde $A_1,\dots,A_n,A$ son fórmulas proposicionales. Las fórmulas $A_1,\dots,A_n$ se denominan premisas de la regla, y la fórmula $A$ es la conclusión de la regla.
Los axiomas representan la base de conocimientos del sistema deductivo, mientras que las reglas permiten obtener nuevas fórmulas a partir de las anteriores.
Si $\{A_1,\dots, A_n\}\subseteq \Sigma$, aplicar la regla $\frac{A_1,\dots,A_n}{A}$ en $\Sigma$ da como resultado $\Sigma\cup\{A\}$.
Muy comúnmente, se usan las reglas como patrones, es decir, dando libertad al uso de fórmulas genéricas, y no reglas que actúan sobre la aparición de fórmulas concretas, como muestra el siguiente ejemplo.
Ejemplo: Sistema deductivo
- $Ax({\mathbf T})=\{p,\, q,\, p\land q\rightarrow (\neg s\lor p\rightarrow r)\}$
- Reglas de inferencia ($A$ y $B$ fórmulas cualesquiera):
donde las reglas actúan a modo de patrones. Por ejemplo, $I_\wedge$ indica que puedes unir por medio de una conjunción cualesquiera dos fórmulas que tengas en tu conjunto (se llama introducción de la conjunción), $I_\vee$ hace algo similar con la disyunción (introducción de la disyunción), $C_\vee$ asegura que el conjunto de fórmulas que se vaya construyendo sea cerrado bajo la conmutación de la disyunción y, finalmente, $MP$ nos permite aplicar la regla de Modus Ponens a nuestro conjunto de fórmulas, de manera que podemos deducir la consecuencia de una implicación bajo la presencia del antecedente.
Con este proceso constructivo ya podemos definir formalmente qué entendemos por una demostración y un teorema en nuestro sistema deductivo:
Definición. Una demostración en ${\mathbf T}$ es una sucesión de fórmulas proposicionales $A_1,\dots, A_k$, donde cada una de ellas, o bien es un axioma de ${\mathbf T}$, o bien se obtiene a partir de fórmulas anteriores de la sucesión mediante la aplicación de una regla de inferencia.
Definición. Una fórmula $A$ es un teorema de ${\mathbf T}$, $\vdash_{\mathbf T} A$, si existe una demostración en ${\mathbf T}$, $A_1,\dots, A_k$, tal que $A=A_k$. La sucesión $A_1,\dots,A_k$ se denomina una demostración de $A$ en ${\mathbf T}$.
Ejemplo: Demostración: En el sistema deductivo del ejemplo anterior, la siguiente sucesión es una demostración de $r$ en ${\mathbf T}$ ($\vdash_{\mathbf T} r$):
Aunque un sistema deductivo introduce una noción de prueba formal, no proporciona ningún procedimiento efectivo para generar demostraciones de las fórmulas que deseamos probar.
Un sistema de razonamiento proporciona, además de un sistema deductivo, un procedimiento de demostración, que implementa una estrategia de búsqueda de demostraciones.
En general, no podemos encontrar estrategias que sean efectivas para todos los sistemas deductivos, y habrá que buscar estrategias que funcionen solo para casos particulares. Ilustraremos un ejemplo de estrategia eficiente en el caso del encadenamiento con cláusulas de Horn.
Encadenamiento con cláusulas de Horn
Una cláusula de Horn es una disyunción de literales que contiene a lo sumo un literal positivo. Por ejemplo, son cláusulas de Horn: $\lnot p\lor \lnot q\lor r$, $\lnot p\lor\lnot r$, $p$.
Una cláusula de Horn positiva es una cláusula que contiene exactamente un literal positivo:
-
Si contiene otros literales negativos se denomina regla. Por ejemplo: $\lnot p\lor \lnot q\lor r$.
- La regla $\lnot p\lor \lnot q\lor r$ se escribe como $$\underbrace{p\land q}_{cuerpo}\rightarrow \underbrace{r}_{cabeza}$$
-
Si sólo contiene el literal positivo se denomina hecho. Por ejemplo: $q$.
Consideraremos el siguiente sistema deductivo, $EA(\Sigma)$, para trabajar con cláusulas de Horn positivas:
- Axiomas: Un conjunto finito, $\Sigma$, de cláusulas de Horn positivas.
- Reglas de inferencia: Si $A$ y $B$ son conjunciones de literales, entonces: $$\begin{array}{llcll} I_\land: & \displaystyle{\frac{A,\, B}{A\land B} } &\hbox{ } & MP: & \displaystyle{\frac{A,\, A\rightarrow B}{B} } \\ \end{array}$$
Teorema. Se tiene que, para todo hecho, $H$: $\Sigma\models H\quad \Leftrightarrow \quad \vdash_{\small EA(\Sigma)} H$
Ejemplo: deducción en $EA(\Sigma)$
$$ \Sigma=\{P\rightarrow Q,\,L\land M\rightarrow P,\,B\land L\rightarrow M,\, A\land P\rightarrow L,\, A\land B\rightarrow L,\, A,\, B\}$$
Veamos que $\vdash_{\small EA(\Sigma)} Q$:
Además, podemos diseñar un par de algoritmos de decisión eficientes para demostrar hechos en $EA(\Sigma)$, que se denominan encadenamiento hacia adelante y encadenamiento hacia atrás.
Encadenamiento hacia adelante
-
Entrada:
- Un hecho: $H$.
- Una enumeración, $R_1,\dots,R_n$, de los elementos de $\Sigma$.
-
Salida:
- SI, si $\vdash_{\small EA(\Sigma)}H$.
- NO, en caso contrario.
Inicialmente, $C$ es el conjunto de todos los hechos que pertenecen a $\Sigma$, $j=1$, $i=0$.
-
Si $H\in C$, paramos y devolvemos SI.
-
Si $j\leq n$ y todos los literales del cuerpo de $R_j$ están en $C$, entonces:
- Si la cabeza de $j$ no está en $C$, la añadimos a $C$, hacemos $j=j+1$, $i=1$ y volvemos a 1.
- Si la cabeza de $j$ está en $C$, hacemos $j=j+1$ y volvemos a 2.
-
Si $j\leq n$ y algún literal del cuerpo de $R_j$ no está en $C$, entonces hacemos $j=j+1$ y volvemos a 2.
-
Si $j>n$ y $i=1$, hacemos $j=1$ y $i=0$ y volvemos a 2.
-
Si $j>n$ y $i=0$, paramos y devolvemos NO.
Ejemplo: encadenamiento hacia adelante
Veamos que $\vdash_{\small EA(\Sigma)} Q$:
Encadenamiento hacia atrás
-
Entrada:
- Un hecho $H$.
- Una enumeración $R_1,\dots,R_n$ de los elementos de $\Sigma$.
-
Salida:
- SI, si $\vdash_{\small EB(\Sigma)}H$.
- NO, en caso contrario.
Inicialmente, $G=[H]$ (lista de objetivos pendientes) y $j=1$.
-
Si $j\leq n$ y $G=[\,]$ , paramos y devolvemos SI.
-
Si $j\leq n$ y $G \neq [\, ]$, denotamos por $E$ el primer elemento de $G$ y actualizamos $j$ y $G$ como sigue:
- Si $E$ es la cabeza de $R_j$, actualizamos $G$ sustituyendo el primer elemento, $E$, por la sucesión de los literales del cuerpo de $R_j$, hacemos $j=1$ y volvemos a 1.
- Si la cabeza de $R_j$ no es $E$, hacemos $j=j+1$ y volvemos a 2.
-
Si $j>n$ y $G=[H]$, paramos y devolvemos NO.
-
Si $j>n$, $G\neq [H]$ y $E$ es el primer elemento de $G$, damos a $G$ y $j$ sus valores anteriores a la aplicación de la regla que, según 2.1, introdujo el literal $E$ en $G$. Hacemos $j=j+1$ y volvemos a 2.
Ejemplo: encadenamiento hacia atrás
Veamos que $\vdash_{\small {\bf EB}(\Sigma)} Q$:
$$ \begin{array}{c|c} {\bf Objetivos} & {\bf Reglas\ usadas} \\ \hline Q & \\ \hline P & P\rightarrow Q \\ \hline L,\, M & L\land M\rightarrow P \\ \hline A,\, B,\, M & A\land B\rightarrow L \\ \hline B,\, M & A \\ \hline M & B \\ \hline B,\,L & B\land L\rightarrow M \\ \hline L & B \\ \hline A,\, B & A\land B\rightarrow L \\ \hline B & A \\ \hline - & B \end{array} $$