algorithm - 分辨率推理规则算法

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. Yes.
2. No, you can't apply resolution in that case.
3. Well, why shouldn't it happen?
4. I guess it's to avoid infinite loops (in that case you return to the conditions at the previous iteration)
5. Same question?

More about 1 and 2. The idea for resolution is that if you have (A v B) ^ (not A v C) then you can safely infer that B or C are true (informally because A is either true or false). If you have (A v B) ^ (A v C) you can't apply the same reasoning.