解析（逻辑）

在数理逻辑和自动定理证明中，解析是一种推理规则，导致命题逻辑和一阶逻辑中的句子的反驳完全定理证明技术。对于命题逻辑，系统地应用解析规则作为公式不满足性的决策程序，解决了布尔可满足性问题的（补充）。

对于一阶逻辑，解析可以作为一阶逻辑不可满足性问题的半算法的基础，提供一个比哥德尔完备性定理更实用的方法。

解析规则可以追溯到戴维斯和普特南（1960）；然而，他们的算法需要尝试给定公式的所有地面实例。1965年，JohnAlanRobinson的语法统一算法消除了这一组合爆炸的根源，该算法允许人们在证明过程中根据需要将公式实例化，以保持反驳的完整性。由解析规则产生的子句有时被称为resolvent。

当与一个完整的搜索算法相结合时，解析规则产生了一个健全和完整的算法，用于决定一个命题公式的可满足性，以及推而广之，决定一个句子在一组公理下的有效性。

这种解决技术使用矛盾证明，其基础是命题逻辑中的任何句子都可以转化为共轭正常形式中的等价句。其步骤如下。

知识库中的所有句子和要证明的句子的否定（猜想）都是连接在一起的。得到的句子被转化为连接的正常形式，连接的句子被看作是子句集合S中的元素。