Resolución (lógica)

En lógica matemática y demostración automática de teoremas , la resolución es una regla de inferencia que conduce a una técnica de demostración de teoremas completa para refutación en lógica proposicional y lógica de primer orden . Para la lógica proposicional, la aplicación sistemática de la regla de resolución actúa como un procedimiento de decisión para la insatisfacibilidad de fórmulas, resolviendo el problema de satisfacibilidad booleana (o su complemento) . Para la lógica de primer orden , la resolución puede utilizarse como base para un semialgoritmo del problema de insatisfacibilidad de la lógica de primer orden , proporcionando un método más práctico que el derivado del teorema de completitud de Gödel .

La regla de resolución se remonta a Davis y Putnam (1960); ^{[ 1 ]} sin embargo, su algoritmo requería probar todas las instancias básicas de la fórmula dada. Esta fuente de explosión combinatoria fue eliminada en 1965 por el algoritmo de unificación sintáctica de John Alan Robinson , que permitía instanciar la fórmula durante la prueba "a demanda" hasta donde fuera necesario para mantener la completitud de la refutación . ^{[ 2 ]}

La cláusula producida por una regla de resolución a veces se denomina resolvente .

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 a partir de 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 que sigue, se considera el complemento de ). La cláusula resultante contiene todos los literales que no tienen complementos. Formalmente: ${\displaystyle \lnot c}$${\displaystyle c}$

${\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

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

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 y son las premisas de la inferencia${\displaystyle \Gamma _{1}\cup \left\{\ell \right\}}$${\displaystyle \Gamma _{2}\cup \left\{{\overline {\ell }}\right\}}$
• ${\displaystyle \Gamma _{1}\cup \Gamma _{2}}$(la resolvente de las premisas) es su conclusión.
• El literal es el literal resuelto a la izquierda,${\displaystyle \ell }$
• El literal es el literal resuelto correcto,${\displaystyle {\overline {\ell }}}$
• ${\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 conjuntivamente.
• 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, da lugar al conjunto .${\ Displaystyle (A_ {1} \ lo A_ {2}) \ tierra (B_ {1} \ lor B_ {2} \ lor B_ {3}) \ tierra (C_ {1})}$${\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.

${\displaystyle {\frac {a\vee b,\quad \neg a\vee c}{b\vee c}}}$

En lenguaje sencillo: Supongamos que es falso. Para que la premisa sea verdadera, debe ser verdadera. O bien, supongamos que es verdadero. Para que la premisa sea verdadera, debe ser verdadera. Por lo tanto, independientemente de si es falso o verdadero , si ambas premisas se cumplen, entonces la conclusión es verdadera. ${\displaystyle a}$${\displaystyle a\vee b}$${\displaystyle b}$${\displaystyle a}$${\displaystyle \neg a\vee c}$${\displaystyle c}$${\displaystyle a}$${\displaystyle b\vee c}$

La regla de resolución se puede generalizar a la lógica de primer orden a: ^{[ 5 ]}

${\displaystyle {\frac {\Gamma _{1}\cup \left\{L_{1}\right\}\,\,\,\,\Gamma _{2}\cup \left\{L_{2}\right\}}{(\Gamma _{1}\cup \Gamma _{2})\phi }}\phi }$

donde es un unificador más general de y , y y no tienen variables comunes. ${\displaystyle \phi }$${\displaystyle L_{1}}$${\displaystyle {\overline {L_{2}}}}$${\displaystyle \Gamma _{1}}$${\displaystyle \Gamma _{2}}$

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

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 y son las premisas de la inferencia${\displaystyle P(x),Q(x)}$${\displaystyle \neg P(b)}$
• ${\displaystyle Q(b)}$(la resolvente de las premisas) es su conclusión.
• El literal es el literal resuelto a la izquierda,${\displaystyle P(x)}$
• El literal es el literal resuelto correcto,${\displaystyle \neg P(b)}$
• ${\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 en 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 factorizar 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}}}$

Se han ideado generalizaciones de la regla de resolución anterior que no requieren que las fórmulas originales estén en forma normal clausal . ^{[ 8 ] [ 9 ] [ 10 ] [ 11 ] [ 12 ] [ 13 ]}

Estas técnicas son útiles principalmente en la demostración interactiva de teoremas, donde es importante preservar la legibilidad humana de las fórmulas de resultados intermedios. Además, evitan la explosión combinatoria durante la transformación a forma de cláusula, ^{[ 10 ] : 98} y, en ocasiones, ahorran pasos de resolución. ^{[ 13 ] : 425}

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}}}$,

donde denota una fórmula arbitraria. Aquí y denotan fórmulas que contienen como subfórmula. se construye reemplazando cada ocurrencia de en por . De manera similar, se construye reemplazando cada ocurrencia de en por . Se pretende simplificar la resolvente utilizando reglas como , etc. Para evitar generar resolventes triviales inútiles, la regla se aplica solo cuando tiene al menos una ocurrencia "negativa" y "positiva" ^{[ 14 ]} en y , respectivamente. Murray ha demostrado que esta regla es completa si se aumenta con reglas de transformación lógica apropiadas. ^{[ 10 ] : 103} ${\displaystyle p}$${\displaystyle F[p]}$${\displaystyle G[p]}$${\displaystyle p}$${\displaystyle F[{\textit {true}}]}$${\displaystyle p}$${\displaystyle F[p]}$${\displaystyle {\textit {true}}}$${\displaystyle G[{\textit {false}}]}$${\displaystyle p}$${\displaystyle G[p]}$${\displaystyle {\textit {false}}}$${\displaystyle F[{\textit {true}}]\lor G[{\textit {false}}]}$${\displaystyle q\land {\textit {true}}\implies q}$${\displaystyle p}$${\displaystyle F}$${\displaystyle G}$

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 indican la polaridad de sus ocurrencias. Mientras que y se construyen como antes, la fórmula se obtiene reemplazando cada ocurrencia positiva de en con y cada ocurrencia negativa con . 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 sean los únicos conectores utilizados en las fórmulas. ^{[ 12 ] : 398–400} ${\displaystyle p}$${\displaystyle G[{\textit {true}}]}$${\displaystyle G[{\textit {false}}]}$${\displaystyle F[G[{\textit {true}}],\lnot G[{\textit {false}}]]}$${\displaystyle p}$${\displaystyle F}$${\displaystyle G[{\textit {true}}]}$${\displaystyle G[{\textit {false}}]}$${\displaystyle \land ,\lor ,\rightarrow ,\lnot }$

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 se reemplaza varias veces por un mayor y/o . ^{[ 12 ] : 398} ${\displaystyle p}$${\displaystyle G[{\textit {true}}]}$${\displaystyle G[{\textit {false}}]}$

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árense (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 fórmula no atómica en el paso (12). Utilizando las reglas de Murray, se obtuvo la fórmula semánticamente equivalente como (7), sin embargo, no se pudo utilizar como debido a su forma sintáctica.${\displaystyle p}$${\displaystyle a\rightarrow e}$${\displaystyle e\lor \lnot a\lor \lnot a}$${\displaystyle p}$

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

La regla de Traugott se generaliza para permitir varias subfórmulas distintas por pares de y de , siempre que tengan un unificador más general común, digamos . La resolvente generalizada se obtiene después de aplicar a las fórmulas madre, 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 completamente general; ^{[ 12 ] : 401} no está claro si su regla seguiría siendo completa si se restringiera a y . ^{[ 16 ]}${\displaystyle p_{1},\ldots ,p_{m}}$${\displaystyle F}$${\displaystyle p_{m+1},\ldots ,p_{n}}$${\displaystyle G}$${\displaystyle p_{1},\ldots ,p_{n}}$${\displaystyle \phi }$${\displaystyle \phi }$${\displaystyle p_{1}=\cdots =p_{m}}$${\displaystyle p_{m+1}=\cdots =p_{n}}$

La paramodulación es una técnica relacionada para razonar sobre conjuntos de cláusulas donde el símbolo predicado es la igualdad. Genera todas las versiones "iguales" de las cláusulas, excepto las identidades reflexivas. La operación de paramodulación toma una afirmación de la cláusula, que debe contener un literal de igualdad. Luego busca una entrada en la cláusula con un subtérmino que se unifica con un lado de la igualdad. El subtérmino se reemplaza por el otro lado de la igualdad. El objetivo general de la paramodulación es reducir el sistema a átomos, reduciendo el tamaño de los términos al sustituir. ^{[ 17 ]}

• CARINE
• GKC
• Nutria
• Proverbio 9
• SARCO
• ESPAS
• Vampiro
• Probador en línea de Logictools

• Desprendimiento condensado  : una versión anterior de la resolución
• Programación lógica inductiva
• Resolución inversa
• Programación lógica
• Método de cuadros analíticos
• Resolución SLD

• Robinson , J. Alan (1965). "Una lógica orientada a máquinas basada en el principio de resolución" . Journal of the ACM . 12 (1): 23– 41. doi : 10.1145/321250.321253 . S2CID  14389185 .
• Leitsch, Alexander (1997). El cálculo de resolución . Textos en informática teórica. Una serie de EATCS. ​​Springer . ISBN 978-3-642-60605-2.
• Gallier, Jean H. (1986). Lógica para la informática: Fundamentos de la demostración automática de teoremas . Harper & Row .
• Lee, Chin-Liang Chang, Richard Char-Tung (1987). Lógica simbólica y demostración mecánica de teoremas . Academic Press. ISBN 0-12-170350-9.{{cite book}}: CS1 maint: multiple names: authors list (link)

• Alex Sakharov. "Principio de resolución" . MathWorld .
• Alex Sakharov. "Resolución" . MathWorld .