Razonamiento Lógico y Demostración de Teoremas
El razonamiento lógico y la demostración de teoremas se refieren al uso de la lógica formal para representar el conocimiento y la automatización de la deducción, derivando conclusiones que necesariamente se desprenden de un conjunto de premisas.
Definition
La demostración de teoremas es la derivación automatizada de si una fórmula lógica se desprende de un conjunto de axiomas, típicamente manipulando las fórmulas con reglas de inferencia sólidas hasta que se deriva el objetivo o se alcanza una contradicción.
Scope
Este tema abarca el razonamiento en lógica proposicional y de primer orden, así como los algoritmos que lo automatizan: la comprobación de satisfacibilidad basada en tablas de verdad y DPLL para la lógica proposicional, la unificación y el principio de resolución para la lógica de primer orden, el encadenamiento hacia adelante y hacia atrás, y los fundamentos de la programación lógica. Aborda la solidez, completitud y decidibilidad de los procedimientos de inferencia. El razonamiento que tolera la incertidumbre o los valores predeterminados se trata en los temas relacionados con el razonamiento bajo incertidumbre y el razonamiento no monótono.
Core questions
- ¿Qué significa que una conclusión se derive de un conjunto de premisas y cómo se verifica mecánicamente esta derivación?
- ¿Cómo el principio de resolución, con la unificación, proporciona una única regla de inferencia completa para la lógica de primer orden?
- ¿En qué se diferencian el encadenamiento hacia adelante y hacia atrás como estrategias de inferencia?
- ¿Cuáles son los límites del razonamiento automatizado, dado que la validez de primer orden es solo semidecidible?
Key concepts
- lógica proposicional y de primer orden
- derivación y validez
- unificación
- resolución y refutación
- DPLL y resolución SAT
- encadenamiento hacia adelante y hacia atrás
- cláusulas de Horn y programación lógica
- solidez y completitud
Key theories
- Principio de resolución
- La resolución de Robinson es una única regla de inferencia sobre cláusulas que, combinada con la unificación, es completa por refutación para la lógica de primer orden: cualquier conjunto insatisfacible de cláusulas puede demostrarse insatisfacible derivando la cláusula vacía.
- DPLL y satisfacibilidad proposicional
- El procedimiento de Davis-Putnam y su refinamiento DPLL deciden la satisfacibilidad proposicional mediante una división sistemática de casos con propagación unitaria y eliminación de literales puros, formando la base de los modernos solucionadores SAT.
- Programación lógica y encadenamiento hacia atrás
- Restringir la lógica de primer orden a cláusulas de Horn y resolver los objetivos hacia atrás produce la programación lógica, en la que la computación es una búsqueda de pruebas, proporcionando tanto un método de razonamiento como un paradigma de programación.
Clinical relevance
La demostración automatizada de teoremas y la resolución SAT/SMT se utilizan en la verificación de hardware y software, el análisis de programas, la planificación y las matemáticas, mientras que los lenguajes de programación lógica como Prolog aplican la inferencia de encadenamiento hacia atrás a bases de datos, análisis sintáctico y sistemas basados en reglas.
History
Los primeros procedimientos de prueba de Gilmore, Davis y Putnam (1960) automatizaron el razonamiento proposicional y cuantificacional, y el principio de resolución de Robinson (1965) unificó la inferencia de primer orden en una sola regla. La década de 1970 vio la resolución refinada en programación lógica y Prolog; la resolución SAT y SMT se convirtió más tarde en una importante tecnología práctica.
Key figures
- John Alan Robinson
- Martin Davis
- Hilary Putnam
- Robert Kowalski
- Alan Robinson
Related topics
Seminal works
- robinson1965
- davis1960
- kowalski1979
Frequently asked questions
- ¿Qué es el principio de resolución?
- La resolución es una única regla de inferencia que toma dos cláusulas que contienen literales complementarios y produce una nueva cláusula que combina el resto. Aplicada repetidamente con unificación, puede demostrar que un conjunto de cláusulas de primer orden es insatisfacible, lo cual es la base para demostrar teoremas por refutación.
- ¿Se garantiza que la demostración automatizada de teoremas terminará?
- Para la lógica proposicional, la validez es decidible, por lo que los procedimientos terminan. Para la lógica de primer orden completa, la validez es solo semidecidible: un probador completo eventualmente confirmará cualquier fórmula válida, pero puede ejecutarse indefinidamente en una inválida, por lo que la terminación no está garantizada en general.