Download Lógica de proposiciones
Document related concepts
Transcript
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