9

我一直无法理解命题逻辑中的解析规则是什么。决议是否只是陈述了一些规则，通过这些规则可以扩展句子并以另一种形式书写？
以下是命题逻辑的简单解析算法。该函数返回通过解析它的 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
4

3 回答 3

15

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

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

  1. 苹果是红色的
  2. If smth is red Then this smth is sweet

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

  1. R('apple')
  2. 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是否正确。我们也用正式语言写这句话 asS('apple')并以倒置状态询问。那么问题的正式定义是：

  • 第 1 条=R('apple')
  • 第 2 条=¬R(X) v S(X)
  • 目标？=¬S('apple')

算法工作如下：

  1. 以条款 c1 和 c2
  2. 计算 c1 和 c2 的解析器给出新的子句 c3 = S('apple')
  3. 计算 c3 的解决方案，目标给我们一个空集。

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

于 2012-09-17T15:53:19.723 回答
4

考虑子句 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。

这种扣除被称为决议。

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

于 2012-09-18T04:33:28.040 回答
0

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




于 2012-09-21T20:30:09.457 回答