A note on linear resolution strategies in consequence-finding

摘要

The completeness, for consequence-finding, of various linear resolution strategies is studied. Linear resolution with merging and subsumption is complete. A-ordered, linear resolution with merging is, in a certain sense, complete. Linear resolution with merging and C-ordering is incomplete. It is argued that the incompleteness of this latter strategy for consequence-finding recommends it above the other two as a complete strategy for theorem-proving.