页面

2011-08-08

why is `resolution' incomplete?

The general resolution rule is $ p \vee s , \neg p \vee t \Rightarrow s \vee t $. Applying the rule, $ x \vee y $ will never be reached from $ x $. In other words, applying the rule strictly needs existence of such formula as $ p \vee s , \neg p \vee t $, which may not be the case. However, resolution is complete for Horn clauses. Moreover, `resolution refutation' is complete.

没有评论: