逻辑推理与定理证明
逻辑推理与定理证明涉及使用形式逻辑来表示知识，以及自动化演绎，即从一组前提中推导出必然的结论。
用 PaperMind 寻找选题即将推出Find papers & topics
Tools & resources
Learn & explore
视频即将推出
Definition
定理证明是通过使用可靠的推理规则操作公式，直到推导出目标或达到矛盾，从而自动推导出一个逻辑公式是否从一组公理中得出。
Scope
本主题涵盖命题逻辑和一阶逻辑中的推理及其自动化算法：命题逻辑的真值表和基于DPLL的可满足性检查，一阶逻辑的合一和归结原理，前向和后向链，以及逻辑编程的基础。它讨论了推理过程的可靠性、完备性和可判定性。容忍不确定性或默认值的推理在相关主题“不确定性推理”和“非单调推理”中处理。
Core questions
- 一个结论被一组前提蕴涵意味着什么？如何机械地检查蕴涵？
- 归结原理如何与合一相结合，为一阶逻辑提供一个单一的完备推理规则？
- 前向链和后向链作为推理策略有何不同？
- 鉴于一阶有效性仅是半可判定的，自动化推理的局限性是什么？
Key concepts
- 命题逻辑和一阶逻辑
- 蕴涵和有效性
- 合一
- 归结与反驳
- DPLL和SAT求解
- 前向链和后向链
- 霍恩子句和逻辑编程
- 可靠性和完备性
Key theories
- 归结原理
- Robinson的归结是一种对子句进行操作的单一推理规则，它与合一相结合，对于一阶逻辑是反驳完备的：任何不可满足的子句集都可以通过推导出空子句来证明其不可满足性。
- DPLL和命题可满足性
- Davis-Putnam过程及其DPLL改进通过系统地进行案例分割，结合单元传播和纯文字消除来判定命题可满足性，构成了现代SAT求解器的基础。
- 逻辑编程和后向链
- 将一阶逻辑限制为霍恩子句并向后归结目标，就产生了逻辑编程，其中计算是证明搜索，既提供了一种推理方法，也提供了一种编程范式。
Clinical relevance
自动化定理证明和SAT/SMT求解用于硬件和软件验证、程序分析、规划和数学领域，而Prolog等逻辑编程语言则将后向链推理应用于数据库、解析和基于规则的系统。
History
Gilmore、Davis和Putnam（1960）的早期证明程序自动化了命题和量化推理，Robinson的归结原理（1965）将一阶推理统一为一条规则。20世纪70年代，归结被完善为逻辑编程和Prolog；SAT和SMT求解后来发展成为一项重要的实用技术。
Key figures
- John Alan Robinson
- Martin Davis
- Hilary Putnam
- Robert Kowalski
- Alan Robinson
Related topics
Seminal works
- robinson1965
- davis1960
- kowalski1979
Frequently asked questions
- 什么是归结原理？
- 归结是一种单一的推理规则，它接受两个包含互补文字的子句，并产生一个结合其余部分的新子句。通过与合一反复应用，它可以证明一组一阶子句是不可满足的，这是通过反驳来证明定理的基础。
- 自动化定理证明是否保证终止？
- 对于命题逻辑，有效性是可判定的，因此过程会终止。对于完整的一阶逻辑，有效性仅是半可判定的：一个完备的证明器最终会确认任何有效的公式，但对于无效的公式可能会永远运行，因此通常不保证终止。