我一直没能理解命题逻辑中的归结规则。归结仅仅是陈述一些规则，通过这些规则可以将一个句子扩展并以另一种形式写出吗？
下面是一个简单的命题逻辑归结算法。该函数通过解析两个输入返回所有可能的子句集。我无法理解这个算法的工作原理，有人能给我解释一下吗？
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 回答：
这是一个可以讨论的主题，但我会试着用一个简单的例子来解释给你听。
你的算法的输入是KB – 用于执行归结的一组规则。很容易理解它是一组事实，比如说：
- 苹果是红色的
- 如果某物是红色的，那么这件东西是甜的
我们引入两个谓词 R(x) – (x 是红色的) 和 S(x) – (x 是甜的)。然后我们可以用正式语言写出我们的事实：
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' 替代。
我们程序的目标是确定句子苹果是甜的是否为真。我们也用正式语言将这个句子写成 S('apple')，并以其否定形式提问。然后问题的正式定义是：
- CLAUSE1 =
R('apple') - CLAUSE2 =
¬R(X) v S(X) - Goal? =
¬S('apple')
算法的工作原理如下：
- 取子句 c1 和 c2
- 计算 c1 和 c2 的归结得到新子句 c3 =
S('apple') - 计算 c3 和目标的归结得到空集。
这意味着我们的句子是真的。如果你无法通过这样的归结得到空集，那就意味着句子是假的（但在大多数实际应用中，这通常是由于知识库中的事实不足）。
