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.
Weekend
11 年前
没有评论:
发表评论