Resolución proposicional

Definición: Es una regla de inferencia utilizada sobre cierto tipo de proposiciones lógicas y es especialmente utilizada para los demostradores automatizados de teoremas. Utilizando resolución se puede construir un demostrador que sea completo (por contradicción) y correcto (en inglés refutational complete and sound) para la lógica proposicional y de primer orden supuesto que un conjunto de proposiciones son insatisfacibles. Por otro lado si el conjunto de proposiciones de hecho es satisfacible, puede o no terminar en una cantidad finita de pasos una demostración por resolución, generalmente lo que sucede es que se asigna un tiempo límite para hallar si un conjunto es insatisfacible o no.

 Algortmo:
-Def.: Sea S un conjunto de clausulas.
Res(S)=Su(U{Res(C1,C2):C1,C2 ∈ S}).
-Algoritmo de resolucion por saturacion

      Entrada: Un conjunto infinito de clausulas, S.
     Salida: Consistente, si S es consistente;
                  Inconsistente, en caso contrario.
S' :=0
     Mientras ( x ∉  S) y (S ≠ S')  Hacer
     S':= S
     S := Res(S)
     fmientras
     Si (x ∈ S) entonces
        Devolver inconsistente
    En caso contrario
        Devolver consistente
    fsi
- Prop.: El algoritmo de resolución por saturación es correcto.

 Ejemplos:
1. (p ∨ q) → r ≡ ¬(p ∨ q) ∨ r ≡ (¬p ∧ ¬q) ∨ r ≡ (¬p ∨ r) ∧ (¬q ∨ r) ≡ {¬p ∨ r, ¬q ∨ r} 
2. ¬p ∨ q ¬q ∨ r ¬p ∨ r Tenemos que: {¬p ∨ q, ¬q ∨ r} |= ¬p ∨ r
3. Σ = {p ∨ q ∨ r, ¬p ∨ s, ¬q ∨ s, ¬r ∨ s} y C = q ∨ r ∨ s.
Una demostración de C desde Σ:
(1) p ∨ q ∨ r pertenece a Σ.
(2) ¬p ∨ s pertenece a Σ.
(3) q ∨ r ∨ s resolución de (1) y (2).

Comentarios

Publicar un comentario

Entradas populares de este blog

Deducción natural en lógica matematica

Imagen
La deducción natural es una aproximación a la teoría de la demostración en la que se busca capturar la manera en que las personas razonan naturalmente al construir demostraciones matemáticas. 1.En vez de contar con unos pocos axiomas a los que se aplican unas pocas reglas de inferencia, la deducción natural propone vaciar la lista de axiomas y ampliar la de reglas de inferencia, introduciendo dos reglas para cada constante lógica: una para introducirla y otra para eliminarla. 2.Una demostración se construye partiendo de supuestos y aplicando las reglas para llegar a la conclusión deseada. Procedimiento: De acuerdo al método de la deducción natural, para evaluar una inferencia, es decir, para mostrar que la conclusión de una inferencia se sigue lógicamente de las premisas, es preciso indicar las reglas de inferencias validadas elementales que conducen de las premisas a la conclusión. Dada una inferencia cualquiera, el proceso derivado consta de...
Leer más

Ensayo

Imagen
1)Variable libre y ligada La expresión a la cual el cuantificador se aplica es el dominio del cuantificador; y una ocurrencia de una variable individual x está ligada  si aparece como  o  o dentro del dominio de un o . Cualquier otro tipo de ocurrencia de una variable es una ocurrencia libre.     Inductiva conjunto de VL(A) conjunto de variables libres de A. 1. Si A es atómica VL(A):= conjunto de todas las variables que aparecen en un A.  2. Si A es ¬B entonces VL(A):= VL(B)  3. Si A es (B*C) donde * es cualquier conectivo binario, entonces VL(A):= VL(B) U VL(C)  4. Si A es B o B entonces VL(A):= VL(B) - {x}     Si  es una proposición; sino es una forma proposicional. Ejemplo. 1) 2) Equivalencias lógicas Dos formas proposicionales P y Q se dicen lógicamente equivalentes, y se escribe P ≡ Q, si sus tablas de verdad coinciden. Ejemplos: 1. Las dos sentencias siguientes son lógicamente...
Leer más

Prolog

-Definición Es un lenguaje para programar artefactos electrónicos mediante el paradigma lógico con técnicas de producción final interpretada. Es bastante conocido en el área de la Ingeniería Informática para investigación en Inteligencia Artificial. -Relaciones Ejemplos de relaciones:            padre(pepe, maria). // en esta relación se denota una existencia de parentesco entre pepe y maria, prolog en este punto no conoce                                                            //quien es el padre de quien, somos nosotros quienes le damos esa interpretación, prolog solamente se encarga de                                                            //crear...
Leer más