0

私は解決推論規則に次のような疑問を持っています。

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
4

1 に答える 1

0
  1. はい。
  2. いいえ、その場合は解決を適用できません。
  3. さて、なぜそれが起こらないのですか？
  4. 無限ループを避けるためだと思います（その場合、前の繰り返しの条件に戻ります）
  5. 同じ質問？

1 と 2 についてさらに詳しく説明します。解決の考え方は、(A v B) ^ (not A v C) があれば、B または C が真であると安全に推論できるということです (非公式に言えば、A は真か偽のどちらかだからです)。(A v B) ^ (A v C) がある場合、同じ推論を適用することはできません。

于 2012-11-12T13:35:14.677 に答える