私は解決推論規則に次のような疑問を持っています。
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