Source: https://www.docsity.com/es/apuntes-logica-y-estructuras-discretas/750938/
Timestamp: 2018-07-22 08:29:51+00:00

Document:
Apuntes Lógica y Estructuras Discretas - Docsity
Apuntes Sistemas de Gestión de Bases de Datos
andoni_moreno_villar 21 de agosto de 2016
Apuntes Lógica y Estructuras Discretas, Apuntes de Sistemas de Gestión de Bases de Datos
Sistemas de Gestión de Bases de Datos,Informática
Pre-visualización3 pages / 49
LPROP.doc
Para cualquier consulta o sugenrencia, puede ponerse en contacto con los autores en: labra@lsi.uniovi.es ó anaisabel@lsi.uniovi.es
Ana I. Fernández M. Octubre, 1998
Introducción...............................................................................................................1 1. Lenguaje de la Lógica Proposicional......................................................................3
1.1. Alfabeto de la Lógica Proposicional......................................................3 1.2. Sintaxis de la Lógica Proposicional.......................................................3 1.3. Semántica de la Lógica Proposicional...................................................4
2. Equivalencia lógica ................................................................................................6 3. Consecuencia Lógica.............................................................................................7 4. Técnicas Semánticas de Estudio de Validez Proposicional......................................8
4.1. Tablas de Verdad ................................................................................8 4.2. Árboles Semánticos .............................................................................8 4.3. Demostraciones por Contradicción.......................................................9 4.4. Resolución Proposicional....................................................................10
4.4.1. Formas Normales .............................................................10 4.4.2. Algoritmo de Resolución Proposicional..............................12 4.4.3. Estrategias de resolución...................................................16
4.4.3.1. Estrategias de Borrado.....................................16 4.4.3.1.1. Eliminación de cláusulas con literales puros.........16 4.4.3.1.2. Eliminación de tautologías..................................16 4.4.3.1.3. Eliminación de Subsunciones..............................17
4.4.3.2. Resolución unitaria ...........................................17 4.4.3.3. Resolución de Entrada .....................................18 4.4.3.4. Resolución Lineal.............................................18 4.4.3.5. Resolución Ordenada.......................................19
5. Teoría de la Prueba: Deducción Natural...............................................................22 6. Aplicación al diseño de Circuitos: Álgebra de Boole ............................................26
6.1. Introducción.......................................................................................26 6.2. Definición de álgebra de Boole y Teoremas ........................................26 6.3. Puertas Lógicas..................................................................................31 6.4. Funciones Booleanas..........................................................................31
6.4.1. Formas Canónicas ............................................................32 Transformación en forma canónica .................................33
6.4.2. Simplificación de funciones lógicas.....................................35 Método de Karnaugh.....................................................36 Funciones incompletas ...................................................39
7. Ejercicios ............................................................................................................40 8. Soluciones...........................................................................................................45 Bibliografía...............................................................................................................48 Indice.......................................................................................................................49
Nombre de la conectivaRepresentaciónEjemplos de frases en las que aparece
Negación ¬p no p es falso p
Conjunción p q∧ p y qp pero q
p sin embargo qp no obstante qp a pesar de q
Disyunción p q∨ o p o q o ambos al menos p o q
p q→ si p entonces q p sólo si q
q si p q cuando p
q es necesario para p para p es necesario q p es suficiente para q para q es suficiente p no p a menos que q
p q↔ p es necesario y suficiente para q p si y sólo si q
Constantes: V F Variables o letras proposicionales: p, q, r, ... Símbolos de Conectivas: ¬ ∧ ∨ → ↔ Signos de puntuación: ( )
1.- Las constantes V (Verdadero) y F (Falso) pertenecen a LPROP 2. Las letras de proposición p,q,r,.. pertenecen a LPROP
3. Si A y B pertenecen a LPROP entonces ( ) , ( ), ( ), ( ), ( ) , ( )¬ ¬ ∧ ∨ → ↔A B A B A B A B A B pertenecen a LPROP
La teoría semántica de la lógica proposicional trata de atribuir significados (Verdadero o Falso) a las distintas fórmulas del lenguaje. Dichos significados dependen del contexto particular en el que se utilice la fórmula. Cada contexto se denomina Interpretación.
{ }V F, a cada una de las letras proposicionales de F. El valor de una proposición p bajo una interpretación I se denota como V pI ( ) .
Definición 2: Dada una fórmula F y una interpretación I, el valor de F bajo I(denotado por V FI ( ) ) es:
° Si F está formada por una proposición p, entonces V F V pI I( ) ( )=
° Si F es de la forma ¬G entonces V F si V G
si V GI I
° Si F es de la forma G H∧ entonces V F si V G V H
I I I( ) ( ) ( )
° Si F es de la forma G H∨ entonces V F si V G V H
° Si F es de la forma G H→ entonces V F si V G V H
° Si F es de la forma G H↔ entonces V F si V G V H
Ejemplo 1: Sea la fórmula ( )F p q q p= → ↔ ¬ ∨ ¬ y la interpretación I que asigna ( )V pI = F y ( )V qI = V
Definición 3: Una interpretación I es un modelo para una fórmula F si V FI ( ) = V
Válida ó Tautología: Todas las interpretaciones son un modelo (Para toda interpretación I, V FI ( ) = V )
Satisfacible: Alguna interpretación es un modelo (Existe una interpretación I tal que V FI ( ) = V )
Insatisfacible: Ninguna interpretación es un modelo (No existe una interpretación I tal que V FI ( ) = V )
Teorema 1: Una fórmula F es válida si y sólo si su negación ¬F es insatisfacible. Dem: F es válida
⇔ { Def. válida} ∀I VI(F)= V
⇔ { Def. Interpretación ¬ } ∀I VI(¬F) = F
⇔ { Def. Insat. } ¬F es Insatisfacible
Definición 4: Se dice que dos fórmulas A y B son equivalentes lógicamente (se denota por A B≡ ó A B⇔ ) si para toda interpretación I, se cumple que V A V BI I( ) ( )=
Teorema 2: A ≡ B si y sólo si la fórmula A↔B es válida Dem: A≡B
⇔ { Def. ≡ } ∀I VI(A) = VI(B)
⇔ { Def. Interpretación ↔ } ∀I VI(A↔B) = V
⇔ { Def. Válida } A↔B es válida
El teorema anterior reduce la demostración de equivalencia entre fórmulas a la demostración de validez de una fórmula. A continuación se presenta una tabla con una serie de equivalencias de uso común y de fácil demostración
Supresión de Implicación: A B A B→ ≡ ¬ ∨ Contraposición: A → B ≡ ¬B → ¬ A Supresión de Doble Implicación: ( ) ( )A B A B B A↔ ≡ → ∧ → Absorción ( )A B A A∧ ∨ ≡ ( )A B A A∨ ∧ ≡
A ∧ ≡F F A ∨ ≡V V Elemento neutro A A∧ ≡V A A∨ ≡F
E. Complementario Contradicción A A∧ ¬ ≡ F
Medio Excluido A A∨ ¬ ≡ V
Idempotencia A A A∧ ≡ A A A∨ ≡ Commutativa A B B A∨ ≡ ∨ A B B A∧ ≡ ∧ Asociativa ( ) ( )A B C A B C∧ ∧ ≡ ∧ ∧ ( ) ( )A B C A B C∨ ∨ ≡ ∨ ∨ Distributiva ( ) ( ) ( )A B C A B A C∨ ∧ ≡ ∨ ∧ ∨ ( ) ( ) ( )A B C A B A C∧ ∨ ≡ ∧ ∨ ∧ De Morgan ( )¬ ∨ ≡ ¬ ∧ ¬A B A B ( )¬ ∧ ≡ ¬ ∨ ¬A B A B
Doble Negación (Involución)
¬¬ ≡A A
Dem: A es válida ⇔ { Def. Válida } ∀I VI(A) = V
⇔ {Si A≡B entonces ∀I VI(A) = VI(B), Leibniz } ∀I VI(B) = V ⇔ { Def. Válida } B es válida
Con el teorema anterior, si se sabe que X es válida, para demostrar que Z es válida se podrá utilizar el formato: X
≡ {...} Y ≡ {...} Z
Definición 5: Sea C un conjunto de fórmulas { }P P Pn1 2, ,L y sea Q una fórmula. Se dice que Q es consecuencia lógica del conjunto C de premisas (se denotará C Q⇒ ) si toda interpretación que es un modelo de C es también un modelo de Q .
Es decir, si para toda interpretación I se cumple que si V P V P V PI I I n( ) ( ) ( )1 2= = = =L V entonces V QI ( ) = V (Intuitivamente, se podría considerar cada interpretación como un "posible mundo". De esa forma, decir que Q es consecuencia lógica de unas premisas es equivalente a pensar que Q toma valor V en cualquier mu ndo en el que las premisas tomen valor V ).
Una estructura de la forma { }P P P Qn1 2, ,L ⇒ se denomina razonamiento. Donde { }P P Pn1 2, ,L es el conjunto de premisas y Q, la conclusión.
Teorema 4: { }P P P Qn1 2, ,L ⇒ es correcto si y sólo si P P P Qn1 2∧ ∧ ∧ →L es válida Dem: {P1, P2, ...Pn} ⇒ Q es correcto
⇔ { Def. Razonamiento } ∀I Si V I (P1) = V I (P2) = ... = V I (Pn) = V entonces V I (Q) = V
⇔ { Def. Interpretación de conjunción } ∀I Si V I (P1 ∧ P2 ∧ ...∧ Pn) = V entonces V I (Q) = V
⇔ { Def. Interpretación de Implicación } ∀I V I (P1 ∧ P2 ∧ ...∧ Pn → Q) = V
⇔ { Def. Válida } P1 ∧ P2 ∧ ...∧ Pn → Q es válida
p q p→q ↔ ¬p∨q F F V F V V V F V V V V
El número de posibles interpretaciones de una fórmula F es 2n donde n es el número de variables proposicionales de F. Por tanto, este método tiene una complejidad exponencial que complica su utilización para fórmulas complejas
2.- Si es posible asignar a F un valor { }V F, se etiqueta el nodo con dicho valor y se finaliza el tratamiento del nodo actual.
- Se Construyen dos ramas, una correspondiente a p interpretado con valor V (identificada como p) y la otra correspondiente a p con valor F (identificada como ¬p ).
Ejemplo 2: Dada la fórmula (p→q) →(¬p→¬q). Seleccionando los literales por orden alfabético, se obtiene el árbol semántico:
¬qq V
1.- Se supone que existe una interpretación I tal que VI(F) = F y se intentan calcular los diversos valores de la fórmula.
2.- Si se llega a una contradicción: Entonces: ¬∃I VI(F) = F ⇒ ∀I VI(F) = V ⇒ F es válida En Caso Contrario: ∃I VI(F) = F ⇒ F no es válida
43421 321
43421 43421
qpqp )( ∧¬→¬∨¬
44444 344444 21 321 321
44 344 21 321321
VV ↔→↔∧↔
CACBBA ↔→↔∧↔
Definición 9: Una fórmula F es una conjunción si es de la forma F F Fn1 2∧ ∧ ∧L n≥0
Definición 10: Una fórmula F es una disyunción si es de la forma F F Fn1 2∨ ∨ ∨L n≥0
Definición 11: Un literal es una proposición ( )p o una proposición negada ( )¬p . Definición 12: Una fórmula F está en Forma Normal Conjuntiva (FNC) si es una conjunción de la forma
F F Fn1 2∧ ∧ ∧L donde cada Fi es una disyunción de literales. Se representa como ∧ ∨  
 = =i
F1∨F2∨ ...∨Fn donde cada Fi es una conjunción de literales. Se representa como ∨ ∧  
Teorema 5: Toda fórmula de la lógica de proposiciones puede ser transformada en una fórmula lógicamente equivalente a ella en Forma Normal Conjuntiva (Disyuntiva).
Dem: La demostración consiste en indicar los pasos del algoritmo de transformación a forma normal
conjuntiva. Puesto que estos pasos mantienen la equivalencia y dado que la equivalencia cumple la propiedad transitiva (ejemplo 4), la fórmula resultante es equivalente a la fórmula original. Para demostrar formalmente que el algoritmo termina, se requiere el estudio de sistemas de re-escritura de términos que puede consultarse en [Abramsky, 92]. Los pasos de transformación son:
1. Eliminar conectiva ↔. A↔B≡(A→B)∧ (B→A) 2. Eliminar conectiva →. A B A B→ ≡ ¬ ∨ 3. Introducir negaciones hasta que afecten a literales mediante las leyes de Morgan. ( )¬ ∧ ≡ ¬ ∨ ¬A B A B ( )¬ ∨ ≡ ¬ ∧ ¬A B A B 4. Eliminar negaciones múltiples. ¬¬ ≡A A 5. Aplicar propiedades distributivas para eliminar las posibles conjunciones (disyunciones) dentro
de disyunciones (conjunciones) obteniendo Forma Normal Conjuntiva (Disyuntiva). ( ) ( ) ( )A B C A B A C∧ ∨ ≡ ∧ ∨ ∧ ( ) ( ) ( )A B C A B A C∨ ∧ ≡ ∨ ∧ ∨ Puesto que las fórmulas resultantes de aplicar cada uno de los pasos anteriores mantienen la
En muchas ocasiones se añaden otros tres pasos que simplifican la fórmula resultante: 6. Eliminar conjunciones/disyunciones con un literal y su opuesto.
(p∧ ¬p ∧ X) ∨ Y ≡ Y (p∨ ¬p ∨ X) ∧Y ≡ Y
7. Eliminar literales repetidos p ∧ p ≡ p p ∨ p ≡ p
8. Eliminar subsunciones. Una subsunción se produce cuando una conjunción (o disyunción) C está incluida en otra D. En dicho caso se elimina la cláusula D
Ejemplo 8: Para transformar la fórmula ¬(p→q)↔p∨r a Forma Normal Conjuntiva, se pueden emplear los siguientes pasos:
La transformación de una fórmula en Forma Normal Conjuntiva a Forma Clausal es inmediata sustituyendo las conectivas ∧ por comas y englobando las disyunciones entre llaves. Ejemplo 9: La fórmula ( ) ( ) ( )¬ ∨ ∧ ¬ ∨ ∨ ¬ ∧p q p q r p en Forma Normal Conjuntiva equivale a { }¬ ∨ ¬ ∨ ∨ ¬p q p q r p, , en Forma Clausal Definición 16: Una cláusula sin literales se denomina cláusula vacía, se representa por ð y su valor es siempre Falso.
Definición 17: Una cláusula que tiene a lo sumo un literal positivo, se denomina cláusula Horn. Una cláusula Horn será de la forma: A B B Bn∨ ¬ ∨ ¬ ∨ ∨¬1 2 L .
Formalizando, la primera frase sería: G P E∨ ∨ y la segunda: G F V G F V→ ∨ ≡ ¬ ∨ ∨
La regla de resolución inferirá: P E F V∨ ∨ ∨
Definición 18: Dadas dos cláusulas C1 y C2 tales que exista un literal l de forma que l C∈ 1 y ¬ ∈l C2 , se denomina resolvente de C1 y C2 respecto a l a la cláusula:
{ }( ) { }( )R C C C l C ll ( ),1 2 1 2= − ∪ − ¬ . Se dice que C1 y C2 son cláusulas resolubles .
Teorema 6 (Consistencia de la regla de resolución): El resolvente de dos cláusulas es consecuencia lógica de ellas. Es decir { } ( )C C R C C1 2 1 2, ,⇒ Dem: Se demuestra por contradicción:
Sea C l l l l m1 11 12 1= ∨ ∨ ∨ ∨L y C l l l l n2 21 22 2= ¬ ∨ ∨ ∨ ∨L .
El resolvente de C1 y C2 respecto a l será R C C l l l l l ll m n( , )1 2 11 12 1 21 22 2= ∨ ∨ ∨ ∨ ∨ ∨ ∨L L
Por el teorema 2, probar que { } ( )C C R C C1 2 1 2, ,⇒ es equivalente a probar que ( )C C R C C1 2 1 2∧ → , es válida. Supóngase que existe una interpretación que la hace Falsa, la asignación de valores será:
{ l l l l l l l l l lm n m nV F F
∨ ∨ ∨ ∧ ¬ ∨ ∨ ∨ → ∨ ∨ ∨ ∨ ∨11 1 21 2 11 1 21 2L 1 244 344
1 244 344 1 244 344
1 2444444 3444444
L L 1 24444 34444
1 244444444444 3444444444444
Puesto que se llega a una contradicción, la fórmula no puede ser Falsa y será siempre verdadera, es decir, la fórmula es Válida. n
Teorema 7: Dadas dos cláusulas C1 y C2 pertenecientes a un conjunto C y resolubles respecto un literal l, entonces: ( )21 , CCRCC l∪≡ .
Dem: Recordando que un conjunto de cláusulas equivale a forma normal conjuntiva, ( )21 , CCRC l∪ es lo mismo que ( )21 , CCRC l∧ . La demostración es:
( )21 , CCRC l∧
Teorema 8: Si el resolvente de dos cláusulas C1 y C2 pertenecientes a un conjunto C es la cláusula vacía, entonces C es insatisfacible. Dem: ( ) =21 , CCRl ð
≡ { Teorema 7, Leibniz } C ≡ C ∧ ð ≡ { Def. ð ≡ F } C ≡ C ∧ F
≡ { El. Neutro, C ∧ F ≡ F } C ≡ F ≡ { Def. Interpretación ≡ }
∀I VI(C) = VI(F)
≡ { Def. Interpretación: VI(F) = F } ∀I VI(C) = F
≡ { Def. Insatisfacible } C es insatisfacible
1.- Buscar dos cláusulas C C C1 2, ∈ tales que exista un literal l que cumple que l C∈ 1 y ¬ ∈l C2
3.- Calcular R C Cl ( , )1 2 y añadirlo al conjunto C
4.- Si R C Cl ( , )1 2 = ❒ entonces SALIR indicando que C es insatisfacible.
3.- Si no se encuentran: SALIR indicando que Cnoes insatisfacible.
Ejemplo 11: Sea C el siguiente conjunto de cláusulas { }p p q r p q r, , ,¬ ∨ ¬ ¬ ∨ ¬ ∨ , se puede demostrar que C es insatisfacible por resolución. Para ello:
- Se resuelve la tercera cláusula (¬ r ) con la cuarta (¬ ∨ ¬ ∨p q r ), obteniendo ¬ ∨ ¬p q .
- Se resuelve ahora la cláusula anterior con la segunda cláusula (¬ ∨p q ) obteniendo: ¬p
Teorema 9: Un razonamiento de la forma P P P Qn1 2, , ,L ⇒ es correcto si y sólo si el conjunto de
cláusulas { }P P P Qc c nc c1 2, , ,L ¬ es insatisfacible. Cada Pi c es el resultado de transformar la premisa Pi a forma clausal y ¬Qc es el resultado de transformar la negación de la conclusión a forma clausal.
Dem: QPPP n ⇒,,, 21 L
QPPP n →∧∧∧ L21 es válida
¬( QPPP n →∧∧∧ L21 ) es insatisfacible
{ }P P P Qc c nc c1 2, , ,L ¬ es insatisfacible Ejemplo 12: Para estudiar si el razonamiento { }p q r s p s p q∧ → ∧ → ¬ ⇒ ¬ ∨ ¬, es correcto por resolución, es necesario transformar cada premisa a forma clausal y añadir el resultado de transformar la negación de la conclusión a forma clausal. El conjunto obtenido sería
{ }¬ ∨ ¬ ∨ ¬ ∨¬ ∨ ¬ ∨ ¬p q r p q s p s p q, , , , . Aplicando el algoritmo de resolución: - Se resuelve la segunda cláusula (¬ ∨ ¬ ∨p q s ) con la tercera (¬ ∨ ¬p s), obteniendo ¬ ∨ ¬p q
Ejemplo 13: Sea el conjunto de cláusulas { }C p p q r p q r= ¬ ∨ ¬ ¬ ∨ ¬ ∨, , , , para construir el árbol semántico para C se recuerda que un conjunto de cláusulas equivale a una fórmula en Forma Normal Conjuntiva, en este caso, ( ) ( ) ( )p p q r p q r∧ ¬ ∨ ∧ ¬ ∧ ¬ ∨ ¬ ∨ . En la siguiente figura se muestra el árbol semántico correspondiente marcando la cláusula falsificada en los nodos de fallo. El árbol semántico será:
( )¬ ∨p q
( )¬ ∨ ¬ ∨p q r( )¬r
Dem: Puesto que el árbol de fallo es finito y las ramas se desarrollan de dos en dos, necesariamente tendremos un último nodo desarrollado con dos hijos. n
p = V ( )¬
F (C )j
- Puesto que el nodo i no falsificó C j y lo único que cambia en el nodo j respecto a i es el valor de p, la cláusula C j debe contener el literal ¬ p (complementado para que sea Falso).
- Por la misma razón anterior, la cláusula Ck debe contener el literal p (sin complementar para que sea Falso)
Por tanto C j y Ck son resolubles respecto a p. El esquema será:
C p resto C R C C resto C resto Cj j
k k p j k j k
= ¬ ∨
= ∨ _
_ ( , ) _ _
En el nodo j, C j toma valor Falso, por tanto resto C j_ tomará también valor Falso, como resto C j_ no contiene el literal p también tomarán valor Falso en el nodo i. De la misma forma, resto Ck_ tomará valor Falso en el nodo i. Por tanto, R C C resto C resto Cp j k j k( , ) _ _= ∨ tomará valor Falso en el nodo i, es decir, el nodo i, es un nodo de fallo para el resolvente de C j y Ck
En ocasiones, puede ocurrir que el resolvente sea falsificado también por alguno de los padres del nodo de inferencia, como ejemplo, considérese el conjunto de cláusulas { }p p q r p r, , ,¬ ∨ ¬ ¬ ∨ , el árbol semántico, junto con los resolventes sería:
( )¬ ∨p r
( )¬p
( )¬ rF F
El resolvente de los nodos 6 y 7 es (¬ p ) que falsifica al nodo 4 pero también falsifica a su antecesor, el
nodo 2. n
Ejemplo 14: El conjunto { }C p q r p s q s p q r= ¬ ∨ ¬ ∨ ¬ ∨ ¬ ∨ ¬, , , , , es insatisfacible, sin embargo, para demostrarlo, se puede ignorar la segunda y la tercera cláusula, puesto que ambas contienen el literal puro s.
Ejemplo 15: La cláusula p q r p∨ ¬ ∨ ∨ ¬ es una tautología.
Definición 21: Una cláusula Csubsume a una cláusula D si y sólo si todo literal de C pertenece también a D, es decir, C D⊆ .
Ejemplo 16: La cláusula p q∨ ¬ subsume a la cláusula p q r∨ ¬ ∨ .
Ejemplo 17: Sea { }C p q p r q r r= ∨ ¬ ∨ ¬ ∨ ¬, , , . A continuación se aplicará la estrategia de resolución unitaria, para ello, se seleccionan siempre dos cláusulas resolubles tales que una de ellas tenga un literal.
1.- p q∨ 2.- ¬ ∨p r 3.- ¬ ∨q r 4.- ¬r 5.- ¬ p Rr ( , )2 4 6.- ¬ q Rr ( , )3 4
7.- q Rp ( , )1 5 8.- p Rq ( , )1 6 9.- rRq ( , )3 7 10.- r Rq ( , )6 7
Obsérvese que los resolventes generados son un subconjunto de los que se podrían generar mediante la resolución sin restricciones. Por ejemplo, las cláusulas 1 y 2 podrían haberse seleccionado para obtener q r∨ . Sin embargo ni esa cláusula ni sus descendientes podrán ser generados porque ninguna de las cláusulas que la generan es unitaria.
Desafortunadamente, los procedimientos de inferencia basados en resolución unitaria no son, en general, completos. Por ejemplo, el conjunto { }C p q p q p q p q= ∨ ¬ ∨ ∨ ¬ ¬ ∨ ¬, , , es insatisfacible, sin embargo, la resolución unitaria no encontrará la cláusula vacía porque ninguna de las cláusulas es unitaria.
Ejemplo 18: Sea { }C p q p r q r r= ∨ ¬ ∨ ¬ ∨ ¬, , , . A continuación se aplicará la estrategia de resolución de entrada, para ello, se seleccionan siempre dos cláusulas resolubles tales que una de ellas pertenezca al conjunto inicial de cláusulas:
1.- p q∨ 2.- ¬ ∨p r 3.- ¬ ∨q r 4.- ¬r 5.- q r∨ Rp ( , )1 2 6.- p r∨ Rq ( , )1 3
7.- ¬ p Rr ( , )2 4 8.- r Rp ( , )2 6 9.- r Rr ( , )4 8
Se puede demostrar que la resolución unitaria y la resolución de entrada tienen el mismo poder de inferencia en el sentido de que si con una estrategia se puede alcanzar la cláusula vacía, con la otra también.
Una consecuencia de lo anterior es que la resolución de entrada es completa para cláusulas Horn, pero incompleta en general. Como contraejemplo, se puede tomar el del apartado anterior.
La resolución lineal (también conocida como resolución con filtrado de antepasados) es una ligera generalización de la resolución de entrada. Se escoge una cláusula inicial o cláusula cabeza C0 y se forma
una cedena de resolventes R R R Rn0 1 3, , , ,L donde:
R R R C C C C Ri i i i i j
= ∈ = ≤+ , tal que ó j i
La resolución lineal toma su nombre del aspecto lineal que presentan las inferencias realizadas. Una resolución lineal comienza con una cláusula del conjunto inicial y produce una cadena lineal de resoluciones como la que se muestra en la figura para el conjunto de cláusulas
{ }C p q p q p q p q= ∨ ¬ ∨ ∨ ¬ ¬ ∨ ¬, , , . Obsérvese que cada resolvente, después del primero, se obtiene del resolvente anterior y de alguna otra cláusula del conjunto.
p q∨
¬ ∨p q p q∨ ¬ ¬ ∨ ¬p q
La resolucióon lineal evita muchas resoluciones inútiles centrándose en cada paso en los antepasados de una cláusula y en los elementos del conjunto inicial.
Los resultados obtenidos aplicando resolución para una determinada cláusula cabeza se pueden mostrar en forma de árbol de resolución. La raíz del árbol es la cláusula cabeza y se forman los nodos descendientes según las cláusulas con las que se pueda resolver. El árbol de resolución para el ejemplo anterior sería:
5: q 6: p 8:p∨¬ p Tautología
7: q∨ ¬ q Tautología
1: p q∨
9: p 10: ¬ p
11: q 12: ¬ q
13: q 14: ¬ q
15: p 16: ¬ p
En la figura se representan las resoluciones indicando el número de cláusula y el literal por el que se resuelve. A cada resolvente se le asigna un nuevo número. Obsérvese que pueden existir caminos infinitos (el camino más a la izquierda), caminos que llevan a tautologías y caminos de éxito que alcanzan la cláusula vacía.
Se puede demostrar que la resolución lineal es completa. Para cualquier conjunto de cláusulas insatisfacibles, aplicando resolución lineal, se alcanza la cláusula vacía.
Debido al siguiente teorema, no siempre es necesario probar con todas las cláusulas del conjunto inicial como cláusulas cabeza.
Teorema 11: Si un conjunto de cláusulas S es satisfacible y S C∪ es insatisfacible, entonces se encuentra la cláusula vacía mediante resolución lineal tomando como cláusula cabeza una cláusula del conjunto C.
El teorema anterior tiene aplicación al estudio de los razonamientos, en los cuales las premisas son, por lo general, satisfacibles. Si al añadir las cláusulas resultantes de negar la conclusión el conjunto resultante es insatisfacible (y el razonamiento es correcto) entonces, según el teorema anterior basta con probar como cláusula cabeza con las que resultaron de negar la conclusión.
La resolución ordenada o selectiva es una estrategia de resolución muy restrictiva en la cual cada cláusula se toma como un conjunto de literales ordenados. La resolución sólo se realiza con el primer literal de cada cláusula. Los literales del resolvente mantienen el orden de las cláusulas padre con los literales del padre positivo (la cláusula que contenía el literal por el que se resuelve afirmado) seguidos de los literales del padre negativo (la cláusula que contenía el literal por el que se resuelve negado).
Ejemplo 19: Sea { }C p q p r q r r= ∨ ¬ ∨ ¬ ∨ ¬, , , . A continuación se aplicará la estrategia de resolución ordenada (se han ordenado los literales de cada cláusula por orden alfabético):
1.- p q∨
2.- ¬ ∨p r
3.- ¬ ∨q r
5.- q r∨ Rp ( , )1 2
6.- r Rq ( , )3 5
7.- r Rr ( , )4 6
La cláusula 5 es el único resolvente ordenado entre las cláusulas 1 y 4. Las cláusulas 1 y 3 no resuelven puesto que sus literales complementarios no son los primeros. Por la misma razón tampoco resuelven las cláusulas 2 y 4 ni las cláusulas 3 y 4. Una vez generada la cláusula 5, resuelve con la cláusula 3 para producir la cláusula 6, la cual resuelve con la cláusula 4 para producir la cláusula vacía.
La resolución ordenada es la más eficiente (en el ejemplo, se obtuvo la cláusula vacía en el tercer paso de resolución). Desafortunadamente, la resolución ordenada no es completa. Sin embargo, se ha demo strado que la resolución ordenada sí es completa para cláusulas Horn.
Tras este breve repaso de las principales estrategias de resolución, cabe reseñar que los principales sistemas de demostración automática basados en el principio de resolución (por ejemp lo, los sistemas Prolog) utilizan una combinación de las dos últimas estrategias restringidas a conjuntos de cláusulas Horn1.
1Los sistemas Prolog utilizan la resolución lineal ordenada para cláusulas Horn en lógica de predicados. Conocida como resolución SLD (Selective Linear Resolution for Definite Clauses) .
En las secciones anteriores se han utilizado técnicas que estudian la corrección de los razonamientos en base al significado de las fórmulas que contienen. Este conjunto de técnicas se engloban en lo que se denomina teoría semántica. Por el contrario, existe otro conjunto de técnicas, conocido como teoría de la prueba, que prescinde de los posibles valores de las fórmulas y se centra únicamente en la manipulación sintáctica de fórmulas. Existen diversos estilos como el sistema de Hilbert, la deducción natural, etc. Todos ellos utilizan un conjunto de axiomas y una serie de reglas de inferencia que permiten obtener teoremas a partir de dichos axiomas o de otros teoremas previamente derivados.
En esta sección se presenta el estilo de deducción natural, desarrollado por Gentzen en 1935 y cuyo principal objetivo es ofrecer un sistema que se acerque a las técnicas de demostración habituales. La deducción natural no contiene axiomas y ofrece una serie de reglas de inferencia por cada tipo de conectiva. Las reglas de inferencia se presentan en la siguiente tabla.
∧ - I
∧ -E A ∧ B
∨ - I B
A ∨ B A → C B → C ∨ -E
B → - I
→ -E
A → B B → A ↔ - I
↔ -E A ↔ B
B ∧ ¬ B ¬ - I ¬ A
B ∧ ¬ B ¬ -E
¬ A ∨ A V - I
V V -E ¬ A ∨ A
A ∧ ¬ A F - I
F F -E
Las reglas de la forma • - I se refieren a la inclusión del símbolo • y las reglas de la forma • - E se refieren a la eliminación de dicho símbolo.
Para el estudio de razonamientos de la forma {P1, P2, ...Pn} ⇒ Q se parte de las premisas y se intenta llegar a la conclusión.
La utilización de cuadros permite visualizar la idea de pruebas subordinadas. En una prueba subordinada, se realiza un supuesto y, una vez llegado a un resultado, se descarta el supuesto (se cierra el cuadro) obteniendo un resultado libre de supuestos. Un ejemplo es la regla de deducción:
Esta regla enuncia que, si se supone A y se llega a demostrar B, entonces, se puede deducir la fórmula A → B.
4 FF-I 3
Organización Lógica De Datos - Apuntes - Fundamentos De Programación. ...
Apuntes sobre la Organización lógica de datos
Apuntes sobre las probabilidad discretas
Apuntes Lógica y Estructuras Discretas

References: Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución 
 resolución