解析（逻辑）

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

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

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

命题逻辑中的解析规则是一个单一有效的推理规则，它产生一个由两个包含互补字面的子句隐含的新子句。字面意义是一个命题变量或一个命题变量的否定值。

如果一个字词是另一个字词的否定，那么这两个字词就被说成是互补的由解析规则产生的子句被称为两个输入子句的解析者。

它是适用于子句而不是术语的共识原则。当两个子句包含多于一对互补的字词时，解析规则可以（独立地）应用于每一对这样的字词；然而，结果总是同义词。肯定前件式 (ModuSPonens) 可以被看作是解析的一个特例（一个单字句和一个双字句的）。

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

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

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