Resolución (lógica)

La regla de resolución en lógica proposicional es una única regla de inferencia válida que produce una nueva cláusula implícita por dos cláusulas que contienen literales complementarios. Un literal es una variable proposicional o la negación de una variable proposicional. Se dice que dos literales son complementarios si uno es la negación del otro (en lo siguiente, ${\displaystyle \lnot c}$se considera el complemento de${\displaystyle c}$). La cláusula resultante contiene todos los literales que no tienen complementos. Formalmente:

${\displaystyle {\frac {a_{1}\lor a_{2}\lor \cdots \lor c,\quad b_{1}\lor b_{2}\lor \cdots \lor \neg c}{a_{1}\lor a_{2}\lor \cdots \lor b_{1}\lor b_{2}\lor \cdots }}}$

dónde

todo${\displaystyle a_{i}}$,${\displaystyle b_{i}}$, y${\displaystyle c}$son literales,

La línea divisoria representa " implica ".

Lo anterior también puede escribirse como:

${\displaystyle {\frac {(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow c,\quad c\rightarrow (b_{1}\lor b_{2}\lor \cdots )}{(\neg a_{1}\land \neg a_{2}\land \cdots )\rightarrow (b_{1}\lor b_{2}\lor \cdots )}}}$

O esquemáticamente como:

${\displaystyle {\frac {\Gamma _{1}\cup \left\{\ell \right\}\,\,\,\,\Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}{\Gamma _{1}\cup \Gamma _{2}}}|\ell |}$

Disponemos de la siguiente terminología:

• Las cláusulas${\displaystyle \Gamma _{1}\cup \left\{\ell \right\}}$ y${\displaystyle \Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}$son las premisas de la inferencia
• ${\displaystyle \Gamma _{1}\cup \Gamma _{2}}$(la resolvente de las premisas) es su conclusión.
• El literal${\displaystyle \ell }$es la izquierda resuelta literal,
• El literal${\displaystyle {\overline {\ell }}}$es el literal resuelto correcto,
• ${\displaystyle |\ell |}$es el átomo resuelto o pivote.

La cláusula resultante de la regla de resolución se denomina resolvente de las dos cláusulas de entrada. Es el principio de consenso aplicado a las cláusulas en lugar de a los términos. ^{[ 3 ]}

Cuando las dos cláusulas contienen más de un par de literales complementarios, la regla de resolución se puede aplicar (de forma independiente) para cada uno de esos pares; sin embargo, el resultado siempre es una tautología .

El modus ponens puede considerarse un caso especial de resolución (de una cláusula de un literal y de una cláusula de dos literales).

${\displaystyle {\frac {p\rightarrow q,\quad p}{q}}}$

es equivalente a

${\displaystyle {\frac {\lnot p\lor q,\quad p}{q}}}$

Cuando se combina con un algoritmo de búsqueda completo , la regla de resolución proporciona un algoritmo sólido y completo para decidir la satisfacibilidad de una fórmula proposicional y, por extensión, la validez de una oración bajo un conjunto de axiomas.

Esta técnica de resolución utiliza la prueba por contradicción y se basa en el hecho de que cualquier oración en lógica proposicional puede transformarse en una oración equivalente en forma normal conjuntiva . ^{[ 4 ]} Los pasos son los siguientes.

• Todas las oraciones en la base de conocimiento y la negación de la oración que se va a probar (la conjetura ) están conectadas de forma conjuntiva.
• La oración resultante se transforma en una forma normal conjuntiva donde los conjuntivos se consideran elementos en un conjunto, S , de cláusulas. ^{[ 4 ]}
  • Por ejemplo, ${\ Displaystyle (A_ {1} \ lor A_ {2}) \ tierra (B_ {1} \ lor B_ {2} \ lor B_ {3}) \ tierra (C_ {1})}$da lugar al conjunto${\displaystyle S=\{A_{1}\lor A_{2},B_{1}\lor B_{2}\lor B_{3},C_{1}\}}$.
• La regla de resolución se aplica a todos los pares posibles de cláusulas que contienen literales complementarios. Tras cada aplicación de la regla de resolución, la oración resultante se simplifica eliminando los literales repetidos. Si la cláusula contiene literales complementarios, se descarta (por ser una tautología). Si no los contiene, y si aún no está presente en el conjunto de cláusulas S , se añade a S y se considera para inferencias de resolución posteriores.
• Si después de aplicar una regla de resolución se obtiene la cláusula vacía , la fórmula original es insatisfacible (o contradictoria ) y, por lo tanto, se puede concluir que la conjetura inicial se deduce de los axiomas.
• Si, por otro lado, no se puede derivar la cláusula vacía y no se puede aplicar la regla de resolución para derivar más cláusulas nuevas, la conjetura no es un teorema de la base de conocimiento original.

Un ejemplo de este algoritmo es el algoritmo original de Davis-Putnam , que posteriormente se perfeccionó hasta convertirse en el algoritmo DPLL , el cual eliminó la necesidad de una representación explícita de las resolventes.

Esta descripción de la técnica de resolución utiliza un conjunto S como estructura de datos subyacente para representar las derivaciones de resolución. Las listas , los árboles y los grafos acíclicos dirigidos son otras alternativas posibles y comunes. Las representaciones en árbol son más fieles al hecho de que la regla de resolución es binaria. Junto con una notación de secuencia para las cláusulas, una representación en árbol también deja claro cómo la regla de resolución se relaciona con un caso especial de la regla de corte , restringido a fórmulas de corte atómicas. Sin embargo, las representaciones en árbol no son tan compactas como las representaciones en conjunto o lista, porque muestran explícitamente subderivaciones redundantes de cláusulas que se utilizan más de una vez en la derivación de la cláusula vacía. Las representaciones en grafo pueden ser tan compactas en el número de cláusulas como las representaciones en lista y también almacenan información estructural sobre qué cláusulas se resolvieron para derivar cada resolvente.

Las cláusulas${\displaystyle P(x),Q(x)}$y${\displaystyle \neg P(b)}$puede aplicar esta regla con${\displaystyle [b/x]}$como unificador.

Aquí x es una variable y b es una constante.

${\displaystyle {\frac {P(x),Q(x)\,\,\,\,\neg P(b)}{Q(b)}}[b/x]}$

Aquí vemos que

• Las cláusulas${\displaystyle P(x),Q(x)}$ y${\displaystyle \neg P(b)}$son las premisas de la inferencia
• ${\displaystyle Q(b)}$(la resolvente de las premisas) es su conclusión.
• El literal${\displaystyle P(x)}$es la izquierda resuelta literal,
• El literal${\displaystyle \neg P(b)}$es el literal resuelto correcto,
• ${\displaystyle P}$es el átomo resuelto o pivote.
• ${\displaystyle [b/x]}$es el unificador más general de los literales resueltos.

En la lógica de primer orden, la resolución condensa los silogismos tradicionales de la inferencia lógica en una sola regla.

Para comprender cómo funciona la resolución, considere el siguiente ejemplo de silogismo de lógica de términos :

Todos los griegos son europeos.

Homero es griego.

Por lo tanto, Homero es europeo.

O, de forma más general:

${\displaystyle \forall xP(x)\Rightarrow Q(x)}$

${\displaystyle P(a)}$

Por lo tanto,${\displaystyle Q(a)}$

Para reformular el razonamiento utilizando la técnica de resolución, primero las cláusulas deben convertirse a la forma normal conjuntiva (FNC). En esta forma, toda cuantificación se vuelve implícita: los cuantificadores universales sobre las variables ( X , Y , ...) simplemente se omiten como entendidos, mientras que las variables cuantificadas existencialmente se reemplazan por funciones de Skolem .

${\displaystyle \neg P(x)\vee Q(x)}$

${\displaystyle P(a)}$

Por lo tanto,${\displaystyle Q(a)}$

Entonces, la pregunta es: ¿cómo deduce la técnica de resolución la última cláusula a partir de las dos primeras? La regla es simple:

• Encuentra dos cláusulas que contengan el mismo predicado, donde este se niega en una cláusula pero no en la otra.
• Realiza una unificación de los dos predicados. (Si la unificación falla, has elegido mal los predicados. Vuelve al paso anterior e inténtalo de nuevo).
• Si alguna variable no ligada que estaba ligada en los predicados unificados también aparece en otros predicados de las dos cláusulas, reemplácela también allí con sus valores ligados (términos).
• Descartar los predicados unificados y combinar los restantes de las dos cláusulas en una nueva cláusula, unidas también por el operador "∨".

Para aplicar esta regla al ejemplo anterior, encontramos que el predicado P aparece en forma negativa.

¬ P ( X )

en la primera cláusula y en forma no negada

P ( a )

En la segunda cláusula, X es una variable no ligada, mientras que a es un valor ligado (término). La unificación de ambos produce la sustitución.

X ↦ a

Si descartamos los predicados unificados y aplicamos esta sustitución a los predicados restantes (solo Q ( X ), en este caso), obtenemos la siguiente conclusión:

Q ( a )

Como otro ejemplo, consideremos la forma silogística.

Todos los cretenses son isleños.

Todos los isleños son mentirosos.

Por lo tanto, todos los cretenses son mentirosos.

O, de forma más general,

∀ X P ( X ) → Q ( X )

∀ X Q ( X ) → R ( X )

Por lo tanto, ∀ X P ( X ) → R ( X )

En la forma normal conjuntiva (FNC), los antecedentes se convierten en:

¬ P ( X ) ∨ Q ( X )

¬ Q ( Y ) ∨ R ( Y )

(La variable de la segunda cláusula fue renombrada para dejar claro que las variables de diferentes cláusulas son distintas).

Ahora bien, unificar Q ( X ) en la primera cláusula con ¬Q ( Y ) en la segunda cláusula significa que X e Y se convierten en la misma variable. Sustituyendo esto en las cláusulas restantes y combinándolas se obtiene la conclusión:

¬ P ( X ) ∨ R ( X )

La regla de resolución, tal como la define Robinson, también incorpora la factorización, que unifica dos literales en la misma cláusula, antes o durante la aplicación de la resolución definida anteriormente. La regla de inferencia resultante es refutable ^{[ 6 ]} , ya que un conjunto de cláusulas es insatisfacible si y solo si existe una derivación de la cláusula vacía utilizando únicamente la resolución, mejorada mediante la factorización.

Un ejemplo de un conjunto de cláusulas insatisfacibles para el cual se necesita factorización para derivar la cláusula vacía es:

${\displaystyle {\begin{array}{rlcl}(1):&P(u)&\lor &P(f(u))\\(2):&\lnot P(v)&\lor &P(f(w))\\(3):&\lnot P(x)&\lor &\lnot P(f(x))\\\end{array}}}$

Dado que cada cláusula consta de dos literales, también lo hace cada resolvente posible. Por lo tanto, mediante resolución sin factorización, nunca se puede obtener la cláusula vacía. Usando factorización, se puede obtener, por ejemplo, de la siguiente manera: ^{[ 7 ]}

${\displaystyle {\begin{array}{rll}(4):&P(u)\lor P(f(w))&{\text{by resolving (1) and (2), with }}v=f(u)\\(5):&P(f(w))&{\text{by factoring (4), with }}u=f(w)\\(6):&\lnot P(f(f(w')))&{\text{by resolving (5) and (3), with }}w=w',x=f(w')\\(7):&{\text{false}}&{\text{by resolving (5) and (6), with }}w=f(w')\\\end{array}}}$

Para la lógica proposicional, Murray ^{[ 9 ] : 18} y Manna y Waldinger ^{[ 10 ] : 98} utilizan la regla

${\displaystyle {\begin{array}{c}F[p]\;\;\;\;\;\;\;\;\;\;G[p]\\\hline F[{\textit {true}}]\lor G[{\textit {false}}]\\\end{array}}}$,

dónde${\displaystyle p}$denota una fórmula arbitraria. Aquí${\displaystyle F[p]}$y${\displaystyle G[p]}$denotan fórmulas que contienen${\displaystyle p}$como una subfórmula.${\displaystyle F[{\textit {true}}]}$se construye reemplazando cada ocurrencia de${\displaystyle p}$en${\displaystyle F[p]}$por${\displaystyle {\textit {true}}}$. Similarmente,${\displaystyle G[{\textit {false}}]}$se construye reemplazando cada ocurrencia de${\displaystyle p}$en${\displaystyle G[p]}$por${\displaystyle {\textit {false}}}$. La resolución${\displaystyle F[{\textit {true}}]\lor G[{\textit {false}}]}$está diseñado para simplificarse utilizando reglas como${\displaystyle q\land {\textit {true}}\implies q}$, etc. Para evitar generar resolventes triviales inútiles, la regla se aplica solo cuando${\displaystyle p}$tiene al menos una ocurrencia "negativa" y "positiva" ^{[ 14 ] en}${\displaystyle F}$y${\displaystyle G}$respectivamente. Murray ha demostrado que esta regla es completa si se amplía con reglas de transformación lógica apropiadas. ^{[ 10 ] : 103}

Traugott utiliza una regla que puede expresarse de manera similar como

${\displaystyle {\begin{array}{c}F[p^{+},p^{-}]\;\;\;\;\;\;\;\;G[p]\\\hline F[G[{\textit {true}}],\lnot G[{\textit {false}}]]\\\end{array}}}$,

donde los exponentes de${\displaystyle p}$indican la polaridad de sus ocurrencias. Mientras${\displaystyle G[{\textit {true}}]}$y${\displaystyle G[{\textit {false}}]}$se construyen como antes, la fórmula${\displaystyle F[G[{\textit {true}}],\lnot G[{\textit {false}}]]}$se obtiene reemplazando cada ocurrencia positiva de${\displaystyle p}$en${\displaystyle F}$con${\displaystyle G[{\textit {true}}]}$y cada ocurrencia negativa con${\displaystyle G[{\textit {false}}]}$. De forma similar al enfoque de Murray, se deben aplicar transformaciones simplificadoras apropiadas a la resolvente. Traugott demostró que su regla es completa, siempre que${\displaystyle \land ,\lor ,\rightarrow ,\lnot }$son los únicos conectores utilizados en las fórmulas. ^{[ 12 ] : 398–400}

La resolvente de Traugott es más fuerte que la de Murray. ^{[ 12 ] : 395} Además, no introduce nuevos conjuntores binarios, evitando así una tendencia hacia la forma clausal en la resolución repetida. Sin embargo, las fórmulas pueden alargarse cuando un pequeño${\displaystyle p}$se reemplaza varias veces con uno más grande${\displaystyle G[{\textit {true}}]}$y/o${\displaystyle G[{\textit {false}}]}$. ^{[ 12 ] : 398}

Como ejemplo, partiendo de las suposiciones dadas por el usuario

${\displaystyle {\begin{array}{rccc}(1):&a&\rightarrow &b\land c\\(2):&c&\rightarrow &d\\(3):&b\land d&\rightarrow &e\\(4):&\lnot (a&\rightarrow &e)\\\end{array}}}$

La regla de Murray se puede utilizar de la siguiente manera para inferir una contradicción: ^{[ 15 ]}

${\displaystyle {\begin{array}{rrclccl}(5):&({\textit {true}}\rightarrow d)&\lor &(a\rightarrow b\land {\textit {false}})&\implies &d\lor \lnot a&{\mbox{from (2) and (1), with }}p=c\\(6):&(b\land {\textit {true}}\rightarrow e)&\lor &({\textit {false}}\lor \lnot a)&\implies &(b\rightarrow e)\lor \lnot a&{\mbox{from (3) and (5), with }}p=d\\(7):&(({\textit {true}}\rightarrow e)\lor \lnot a)&\lor &(a\rightarrow {\textit {false}}\land c)&\implies &e\lor \lnot a\lor \lnot a&{\mbox{from (6) and (1), with }}p=b\\(8):&(e\lor \lnot {\textit {true}}\lor \lnot {\textit {true}})&\lor &\lnot ({\textit {false}}\rightarrow e)&\implies &e&{\mbox{from (7) and (4), with }}p=a\\(9):&\lnot (a\rightarrow {\textit {true}})&\lor &{\textit {false}}&\implies &{\textit {false}}&{\mbox{from (4) and (8), with }}p=e\\\end{array}}}$

Para el mismo propósito, la regla de Traugott puede utilizarse de la siguiente manera  : ^{[ 12 ] : 397}

${\displaystyle {\begin{array}{rcccl}(10):&a\rightarrow b\land ({\textit {true}}\rightarrow d)&\implies &a\rightarrow b\land d&{\mbox{from (1) and (2), with }}p=c\\(11):&a\rightarrow ({\textit {true}}\rightarrow e)&\implies &a\rightarrow e&{\mbox{from (10) and (3), with }}p=(b\land d)\\(12):&\lnot {\textit {true}}&\implies &{\textit {false}}&{\mbox{from (11) and (4), with }}p=(a\rightarrow e)\\\end{array}}}$

Al comparar ambas deducciones, se pueden observar los siguientes problemas:

• La regla de Traugott puede producir una resolvente más precisa: compárese (5) y (10), que resuelven (1) y (2) en${\displaystyle p=c}$.
• La regla de Murray introdujo 3 nuevos símbolos de disyunción: en (5), (6) y (7), mientras que la regla de Traugott no introdujo ningún símbolo nuevo; en este sentido, las fórmulas intermedias de Traugott se asemejan más al estilo del usuario que las de Murray.
• Debido a este último problema, la regla de Traugott puede aprovechar la implicación en la suposición (4), utilizando como${\displaystyle p}$la fórmula no atómica${\displaystyle a\rightarrow e}$en el paso (12). Usando las reglas de Murray, la fórmula semánticamente equivalente${\displaystyle e\lor \lnot a\lor \lnot a}$se obtuvo como (7), sin embargo no se pudo utilizar como${\displaystyle p}$debido a su forma sintáctica.

Para la lógica de predicados de primer orden, la regla de Murray se generaliza para permitir subfórmulas distintas, pero unificables.${\displaystyle p_{1}}$y${\displaystyle p_{2}}$de${\displaystyle F}$y${\displaystyle G}$, respectivamente. Si${\displaystyle \phi }$es el unificador más general de${\displaystyle p_{1}}$y${\displaystyle p_{2}}$, entonces la resolvente generalizada es${\displaystyle F\phi [{\textit {true}}]\lor G\phi [{\textit {false}}]}$. Si bien la regla sigue siendo válida si se requiere una sustitución más especial${\displaystyle \phi }$Si se utiliza, no se necesitan tales aplicaciones de reglas para lograr la completitud.

La regla de Traugott se generaliza para permitir varias subfórmulas distintas por pares.${\displaystyle p_{1},\ldots ,p_{m}}$de${\displaystyle F}$y${\displaystyle p_{m+1},\ldots ,p_{n}}$de${\displaystyle G}$, mientras${\displaystyle p_{1},\ldots ,p_{n}}$tener un unificador común más general, por ejemplo${\displaystyle \phi }$. La resolvente generalizada se obtiene después de aplicar${\displaystyle \phi }$a las fórmulas principales, haciendo así aplicable la versión proposicional. La prueba de completitud de Traugott se basa en la suposición de que se utiliza esta regla totalmente general; ^{[ 12 ] : 401} no está claro si su regla seguiría siendo completa si se restringiera a${\displaystyle p_{1}=\cdots =p_{m}}$y${\displaystyle p_{m+1}=\cdots =p_{n}}$. ^{[ 16 ]}