Download Lógica de proposiciones

Resolución, la regla de
inferencia y el cálculo
Raúl Monroy
Resolución
• Sistema de inferencia con “sólo” una
regla:
• Modus Ponens y Modus Tollens son casos
especiales de resolución
– Cuidado: nunca resolver sobre proposiciones
distintas simultáneamente
Resolución: el método
• Idea básica: Si, dado un conjunto de
premisas, P, se desea mostrar la
proposición, q, entonces añade a P la
negación de q y busca una refutación; i.e.,
muestra que P{¬q} es inconsistente
• Restricción: Aplica sólo a términos de
primer orden en forma clausular
Forma norma clausular (CNF)
• Un conjunto de fórmulas se encuentra en
forma clausular sii cada fórmula es una
cláusula
• Una cláusula es una disyunción de
literales
• Una literal es una constante objeto o la
negación de una constante objeto
– N.B. use un procedimiento de normalización
Forma normal conjuntiva
• Lema: El procedimiento de forma normal
conjuntiva, aplicado a una fórmula, termina
produciendo otra, equivalente, en forma normal
conjuntiva
Forma clausular
• Romper la conjunción de cláusulas en cláusulas
independientes:
• Lema : El proceso forma clausular, aplicado a
una fórmula en forma normal conjuntiva, termina
produciendo otra en forma clausular
Método de resolución
• Proposición 1: El método de resolución
es correcto
• Proposición 2: El método de resolución
es completo
Conclusiones
• Algunos cálculos son menos
estructurados que otros
• Cálculos estructurados permiten la
construcción de procedimientos de
demostración, algunos de los cuales a su
vez permiten construir un procedimiento
de decisión
• Lógica de proposiciones es soluble