分辨率推理规则算法

Question

我对解决推理规则有以下疑问。

1* 在for each Ci, Cj in clauses do 中，每个 Ci 和 Cj 是否必然包含互补符号（例如，一个包含 A，另一个包含 ~A）？

2* 在上面的示例中，如果两个子句具有相同的符号（例如 A 和 A）会怎样。我应该考虑推论吗？如果是，它返回什么结果？

3* if new ⊆ clauses then return false 何时运行？探索完所有子句之后？

4*if new ⊆ clauses then return false有什么用？

5*if new ⊆ clauses then return false有什么用？

 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  

Answer 1

1. 是的。
2. 不，在这种情况下您不能应用分辨率。
3. 那么，为什么不应该发生呢？
4. 我猜是为了避免无限循环（在那种情况下你会回到上一次迭代的条件）
5. 同样的问题？

关于 1 和 2 的更多信息。解析的想法是，如果您有 (A v B) ^（不是 A v C），那么您可以安全地推断 B 或 C 为真（非正式地，因为 A 为真或假）。如果您有 (A v B) ^ (A v C)，则不能应用相同的推理。