Regla de resolución

La regla de resolución es una regla de inferencia , ascendiendo al método de demostración de teoremas a través de la búsqueda de contradicciones; utilizado en lógica proposicional y lógica de primer orden . La regla de resolución, aplicada secuencialmente para una lista de resolventes, nos permite responder a la pregunta de si existe una contradicción en el conjunto original de expresiones lógicas. La regla de resolución fue propuesta en 1930 en la disertación doctoral de Jacques Herbrand para probar teoremas en sistemas formales de primer orden. La regla fue desarrollada por John Alan Robinson en 1965.

Los algoritmos de prueba de derivabilidad construidos sobre la base de este método se utilizan en muchos sistemas de inteligencia artificial y también son la base sobre la que se construye el lenguaje de programación lógica Prolog . $A \vdash B$

Cálculo proposicional

Sean y sean dos oraciones en el cálculo proposicional , y let , y , donde es una variable proposicional, y y son oraciones cualesquiera (en particular, tal vez vacías o que consistan en un solo literal). $C_{1}$ $C_{2}$ $C_{1}=P\lor C'_{1}$ $C_{2}=\lno P\lor C'_{2}$ $PAGS$ $C'_1$ $C'_2$

regla de inferencia

{\frac{C_{1},C_{2}}{C'_{1}\lor C'_{2}}}

llamada regla de resolución . [una]

Las oraciones C 1 y C 2 se llaman resolubles (o padre ), la oración es resolutiva y las fórmulas y son contra literales. En general, se toman dos expresiones en una regla de resolución y se genera una nueva expresión que contiene todos los literales de las dos expresiones originales, excepto dos literales mutuamente inversos. ${\displaystyle C'_{1}\lor C'_{2))$ $PAGS$ $\lno P$

Método de resolución

La demostración de teoremas se reduce a probar que alguna fórmula (la hipótesis del teorema) es consecuencia lógica de un conjunto de fórmulas (supuestos). Es decir, el teorema mismo se puede formular de la siguiente manera: "si es verdadero, entonces es verdadero y ". $GRAMO$ ${\displaystyle F_{1},\puntos,F_{k))$ ${\displaystyle F_{1},\puntos,F_{k))$ $GRAMO$

Para probar que una fórmula es una consecuencia lógica de un conjunto de fórmulas , se aplica el método de resolución de la siguiente manera. Primero, se compila un conjunto de fórmulas . Luego cada una de estas fórmulas se reduce a CNF (conjunción de disyuntivas) y los signos de conjunción se tachan en las fórmulas resultantes. Resulta un montón de disyuntivas . Y finalmente, la salida de una cláusula vacía de . Si la cláusula vacía se deriva de , entonces la fórmula es una consecuencia lógica de las fórmulas . Si no se puede deducir #, entonces no es una consecuencia lógica de las fórmulas . Este método de probar teoremas se llama método de resolución . $GRAMO$ ${\displaystyle F_{1},\puntos,F_{k))$ ${\displaystyle \{F_{1},\dots ,F_{k},\neg G\))$ $S$ $S$ $S$ $GRAMO$ ${\displaystyle F_{1},\puntos,F_{k))$ $S$ $GRAMO$ ${\displaystyle F_{1},\puntos,F_{k))$

Considere un ejemplo de un método de prueba por resolución. Digamos que tenemos las siguientes declaraciones:

"La manzana es roja y fragante". "Si la manzana es roja, entonces la manzana es deliciosa".

Probemos la afirmación "la manzana es sabrosa". Introduzcamos un conjunto de fórmulas que describen enunciados simples correspondientes a los enunciados anteriores. Dejar

X_{1}

- Manzana roja

X_{2}

- "Manzana aromática",

X_3

- Deliciosa manzana.

Luego, las declaraciones mismas se pueden escribir en forma de fórmulas complejas:

X_{1}\tierra X_{2}

- "La manzana es roja y fragante".

{\displaystyle X_{1}\rightarrow X_{3))

“Si la manzana es roja, entonces la manzana es sabrosa”.

Entonces el enunciado a demostrar se expresa mediante la fórmula . $X_3$

Entonces, demostremos que es una consecuencia lógica de y . Primero, componemos un conjunto de fórmulas con la negación del enunciado que se está probando; obtenemos $X_3$ ${\ estilo de visualización (X_ {1} \ tierra X_ {2})}$ ${\ estilo de visualización (X_ {1} \ a X_ {3})}$

\{(X_{1}\land X_{2}),(X_{1}\rightarrow X_{3}),\neg X_{3}\}.

Ahora traemos todas las fórmulas a la forma normal conjuntiva y tachamos las conjunciones. Obtenemos el siguiente conjunto de cláusulas:

\{X_{1},X_{2},(\neg X_{1}\vee X_{3}),\neg X_{3}\}.

A continuación, buscamos la derivación de una cláusula vacía. Aplicamos la regla de resolución a las cláusulas primera y tercera:

\{X_{1},X_{2},(\neg X_{1}\vee X_{3}),\neg X_{3},X_{3}\}.

Aplicamos la regla de resolución a las cláusulas cuarta y quinta:

\{X_{1},X_{2},(\neg X_{1}\vee X_{3}),\neg X_{3},X_{3},\#\}.

Así, se deduce una cláusula vacía, por lo tanto se refuta la expresión con la negación del enunciado, por lo tanto se prueba el enunciado mismo.

Completitud y compacidad del método

La regla de resolución tiene la propiedad de completitud en el sentido de que siempre se puede usar para deducir de una cláusula vacía # si el conjunto original de cláusulas es inconsistente. $S$ $S$

La relación de derivabilidad (debido a la finitud de la derivación) es compacta: si , entonces hay un subconjunto finito de , tal que . Por lo tanto, primero debemos probar que la relación de imposibilidad es compacta. $S\vdash\#$ $S' \subseteq S$ $S'\vdash\#$

Lema. Si cada subconjunto finito tiene una estimación satisfactoria, entonces hay una estimación satisfactoria para todo el conjunto de cláusulas . $S' \subseteq S$ $S$

Prueba. Suponga que hay cláusulas que usan un conjunto contable de variables proposicionales . Construyamos un árbol binario infinito, donde dos aristas emergen de cada vértice a una altura , etiquetadas con literales y respectivamente. Eliminamos de este árbol aquellos vértices, los literales a lo largo del camino a los que forman una estimación que contradice al menos una disyunción . $S$ $p_{1},\ldots,p_{k},\ldots$ $k$ $\neg p_{k+1}$ $p_{k+1}$ $S$

Para cada uno , considere un subconjunto finito que consta de cláusulas que no contienen variables . Por la condición del lema, existe tal estimación de las variables (o un camino al vértice al nivel del árbol podado) que cumple todas las disyunciones de . Esto significa que el árbol truncado es infinito (es decir, contiene un número infinito de vértices). Por el lema del camino infinito de Koenig, un árbol podado contiene una rama infinita. Esta rama corresponde a una evaluación de todas las variables , lo que hace que todas las cláusulas de . Que es lo que se requería. $k$ $S_{k}\subseteq S$ $p_{k+1}, p_{k+2}, \ldots$ ${\displaystyle p_{1},\ldots,p_{k))$ $k+1$ $S_k$ $p_{1},\ldots,p_{k},\ldots$ $S$

Teorema de completitud para el método de resolución en lógica proposicional

teorema _ Un conjunto de cláusulas S es inconsistente si y solo si hay una refutación en S (o de S ).

Prueba. La necesidad (corrección del método de resolución) es obvia, ya que la cláusula vacía no puede ser verdadera bajo ninguna evaluación. Demos una prueba de suficiencia. Por el lema de compacidad, basta con restringirnos al caso de un número finito de variables proposicionales. Realizamos la inducción sobre el número de variables proposicionales que aparecen en al menos una cláusula de . Sea verdadero el teorema de completitud para , demostremos su verdad para . En otras palabras, mostraremos que de cualquier conjunto contradictorio de cláusulas en las que aparecen variables proposicionales , se puede deducir una cláusula vacía. $norte$ $S$ ${\ estilo de visualización n = k}$ ${\ estilo de visualización n = k + 1}$ $S$ $p_{1},\ldots,p_{k+1}$

Elijamos cualquiera de las variables proposicionales, por ejemplo, . Construyamos dos conjuntos de cláusulas y . En el conjunto , ponemos aquellas cláusulas en las que no aparece el literal , y de cada una de esas cláusulas eliminamos el literal (si aparece allí). De manera similar, el conjunto contiene el resto de cláusulas que no contienen el literal después de la eliminación del literal (si ocurre en ellas). $k+1$ $p_{k+1}$ $S$ ${\displaystyle S_{k+1}^{+))$ $S_{k+1}^{-}$ ${\displaystyle S_{k+1}^{+))$ $S$ $\neg p_{k+1}$ $p_{k+1}$ $S_{k+1}^{-}$ $S$ $p_{k+1}$ $\neg p_{k+1}$

Se argumenta que cada uno de los conjuntos de cláusulas y es inconsistente, es decir, no tiene una estimación que satisfaga todas las cláusulas simultáneamente. Esto es cierto porque a partir de una estimación que satisface todas las cláusulas del conjunto simultáneamente, se puede construir una estimación que satisface todas las cláusulas del conjunto simultáneamente . Que esta evaluación cumple con todas las cláusulas omitidas al pasar de a es obvio, porque estas cláusulas contienen el literal . Las cláusulas restantes se cumplen bajo el supuesto de que la evaluación satisface todas las cláusulas del conjunto y, por lo tanto, todas las cláusulas extendidas (agregando el literal descartado ). De manera similar, a partir de una estimación que satisfaga todas las cláusulas del conjunto simultáneamente, se puede construir una estimación que satisfaga todas las cláusulas del conjunto simultáneamente . ${\displaystyle S_{k+1}^{+))$ $S_{k+1}^{-}$ ${\ estilo de visualización \ rho ^ {+))$ ${\displaystyle S_{k+1}^{+))$ $\rho ^{+}\taza [\rho (p_{k+1})=0]$ $S$ $S$ ${\displaystyle S_{k+1}^{+))$ $\neg p_{k+1}$ $S$ ${\ estilo de visualización \ rho ^ {+))$ ${\displaystyle S_{k+1}^{+))$ $p_{k+1}$ ${\ estilo de visualización \ rho ^ {-}}$ $S_{k+1}^{-}$ ${\ estilo de visualización \ rho ^ {-} \ taza [\ rho (p_ {k + 1}) = 1]}$ $S$

Por el supuesto de la inducción, a partir de conjuntos contradictorios de cláusulas y (puesto que en cada uno de ellos sólo aparecen variables proposicionales ), se obtienen conclusiones de una cláusula vacía. Si restauramos el literal omitido para las cláusulas establecidas en cada aparición de la salida de una cláusula vacía, entonces obtenemos la salida de una cláusula que consta de un único literal . De manera similar, de la derivación de una cláusula vacía de un conjunto inconsistente , obtenemos la derivación de una disyunción que consta de un solo literal . Queda por aplicar la regla de resolución una vez para obtener una cláusula vacía. QED ${\displaystyle S_{k+1}^{+))$ $S_{k+1}^{-}$ $k$ ${\displaystyle p_{1},\ldots,p_{k))$ $p_{k+1}$ ${\displaystyle S_{k+1}^{+))$ $p_{k+1}$ $S_{k+1}^{-}$ $\neg p_{k+1}$

Cálculo de predicados

Sean C 1 y C 2 dos oraciones en el cálculo de predicados.

regla de inferencia

{\frac {C_{1},C_{2}}{(C'_{1}\lor C'_{2})\sigma }}R

se llama regla de resolución en cálculo de predicados si en las oraciones C 1 y C 2 hay contraliterales unificados P 1 y P 2 , es decir , y , y las fórmulas atómicas P 1 y P 2 están unificadas por el unificador más común . ${\displaystyle C_{1}=P_{1}\lor C'_{1))$ $C_2 = \lno P_2 \lor C'_2$ $\sigma$

En este caso, la resolución de las sentencias C 1 y C 2 es la sentencia obtenida de la sentencia aplicando el unificador . [2] ${\ estilo de visualización (C'_{1}\lor C'_{2})\sigma}$ ${\displaystyle C'_{1}\lor C'_{2))$ $\sigma$

Sin embargo, debido a la indecidibilidad de la lógica de los predicados de primer orden para un conjunto de cláusulas satisfacibles (consistentes), un procedimiento basado en el principio de resolución puede ejecutarse indefinidamente. Por lo general, la resolución se usa en la programación lógica junto con el razonamiento directo o inverso. El método directo (de las premisas) de las premisas A, B deduce la conclusión B (la regla del modus ponens). La principal desventaja del método directo de razonamiento es su falta de dirección: las aplicaciones repetidas del método generalmente conducen a un fuerte aumento de conclusiones intermedias que no están relacionadas con la conclusión objetivo.

Se dirige el método inverso (desde la meta): de la conclusión deseada B y de las mismas premisas, se deriva una nueva conclusión secundaria A. Cada paso de la conclusión en este caso siempre está asociado con la meta establecida originalmente.

Una deficiencia significativa del principio de resolución radica en la formación en cada paso de la derivación de un conjunto de resolutivos: nuevas cláusulas, la mayoría de las cuales resultan superfluas. En este sentido, se han desarrollado diversas modificaciones del principio de resolución que utilizan estrategias de búsqueda más eficientes y diversas restricciones en la forma de las cláusulas iniciales.

Enlaces

↑ Chen Ch., Li R. Lógica matemática y demostración automática de teoremas , p. 77.
↑ Chen Ch., Li R. Lógica matemática y demostración automática de teoremas , p. 85.

Literatura

Chen Ch., Li R. Capítulo 5. Método de resolución // Lógica matemática y demostración automática de teoremas = Chin-Liang Chang; Richard Char-Tung Lee (1973). Demostración de lógica simbólica y teoremas mecánicos. Prensa Académica. - M. : "Nauka" , 1983. - S. 358.
Guts A. K. Capítulo 1.3. Método de Resolución // Lógica Matemática y Teoría de Algoritmos. - Omsk: Patrimonio. Diálogo-Siberia, 2003. - P. 108.
Nilson N. J. Principios de inteligencia artificial. - M. , 1985.
Mendelson E. Introducción a la lógica matemática. - M. , 1984.
Russell S., Norvig P. Inteligencia artificial: un enfoque moderno = Inteligencia artificial: un enfoque moderno. — M. : Williams, 2006.