解决算法如何适用于命题逻辑？

Posted 2023-05-08

【中文标题】解决算法如何适用于命题逻辑？

【英文标题】：How does a Resolution algorithm work for propositional logic?

【发布时间】：2012-09-09 18:16:20

【问题描述】：

我一直无法理解命题逻辑中的解析规则是什么。解析是否只是陈述了一些规则，通过这些规则可以扩展句子并以另一种形式书写？ 以下是命题逻辑的简单解析算法。该函数返回通过解析它的 2 输入获得的所有可能子句的集合。我无法理解算法的工作原理，有人可以向我解释一下吗？

  function PL-RESOLUTION(KB,α) returns true or false
     inputs: KB, the knowledge base, a sentence α in propositional logic, the query, a
             sentence in propositional logic 
     clauses <--- the set of clauses in the CNF representation of KB ∧ ¬α
     new <--- 
     loop do
        for each Ci, Cj in clauses do
            resolvents <----- PL-RESOLVE(Ci, Cj)
            if resolvents contains the empty clause then return true
            new <--- new ∪ resolvents
        if new ⊆ clauses then return false
        clauses <---- clauses  ∪ new                                                                           

【参考方案1】：

这是一个完整的讨论主题，但我将尝试向您解释一个简单的示例。

算法的输入是 KB - 一组执行解析的规则。很容易理解为一组事实，例如：

苹果是红色的 如果 smth是红色的那么这个smth是甜蜜的

我们引入两个谓词R(x) - (x is red) 和S(x) - (x is sweet)。比我们可以用正式语言写下我们的事实：

R('apple') R(X) -> S(X)

我们可以将第二个事实替换为¬R v S 以符合解析规则。

在您的程序中计算解析步骤会删除两个相反的事实：

示例：1) a & ¬a -> empty。 2)a('b') & ¬a(x) v s(x) -> S('b')

注意第二个示例变量 x 替换为实际值 'b'。

我们程序的目标是确定句子 apple is sweet 是否为真。我们也用正式语言将这句话写成S('apple')，并以倒置状态询问。那么问题的正式定义是：

条款 1

= R('apple')

条款 2

= ¬R(X) v S(X)

目标？

= ¬S('apple')

算法的工作原理如下：

以子句 c1 和 c2 为例 计算 c1 和 c2 的解析器给出新的子句 c3 = S('apple') 计算 c3 的解析器，目标为我们提供空集。

这意味着我们的句子是正确的。如果你不能用这样的分辨率得到空集，这意味着句子是错误的（但对于实际应用中的大多数情况，它缺乏 KB 事实）。

【讨论】：

当 2 个子句传递给 resolve 函数时会发生什么？在 PL-RESOLVE(Ci, Cj)

应用解析规则。它删除所有对立的谓词（即A 和¬A）并为其余的返回CNF。

哪些子句是 Ci 和 Cj ？它们是Clauses中2组的对应子句吗？

clauses 是一组子句。 Ci 和 Cj 是该集合中的子句，例如 i != j

我花了太多时间试图找出 PL-RESOLVE(Ci, Cj) 做了什么，但您的评论有所帮助。谢谢@mishadoff！

【参考方案2】：

考虑子句 X 和 Y，其中 X = a, x1, x2, ..., xm 和 Y = ~a, y1, y2, ..., yn，其中 a 是一个变量，~ a 是它的否定，而 xi 和 yi 是文字（即可能否定的变量）。

X 的解释是命题 (a \/ x1 \/ x2 \/ ... \/ xm)——也就是说，假设 X 为真，至少 a 或 xi 之一必须为真. Y 也是如此。

我们假设 X 和 Y 为真。

我们也知道 (a \/ ~a) 始终为真，无论 a 的值如何。

如果~a为真，则a为假，所以~a /\ X => x1, x2, ..., xm。

如果 a 为真，则 ~a 为假。在这种情况下 a /\ Y => y1, y2, ..., yn。

因此，我们知道 x1, x2, ..., xm, y1, y2, ..., yn 必须为真，假设 X 和 Y 为真。注意 new 子句没有引用变量 a。

这种推论称为决议。

这在基于分辨率的定理证明器中如何工作？很简单：我们使用反证法。也就是说，我们首先将我们的“事实”变成从句，并添加与我们的“目标”否定相对应的从句。那么，如果我们最终可以解决空子句 ，我们将遇到矛盾，因为空子句等同于虚假。因为事实是给定的，这意味着我们否定的目标一定是错误的，因此（未否定的）目标一定是真的。

【参考方案3】：

解析是用于证明可在谓词逻辑中表达的论点正确的过程 解决导致了命题逻辑中句子的反驳定理证明技术。 resolution 提供了驳斥证明。即为了证明它是有效的，决议试图证明对陈述的否定会产生与已知陈述的矛盾 算法： 1）。将公理的所有命题转换为从句形式 2）。否定命题并将结果转换为子句形式 3) 解决它们 4)如果resolvent是空子句，则发现矛盾