Two Results on Ordering for Resolution with Merging and Linear Format
Raymond Reiter · Journal of the ACM · 1971
Resolution with merging, linear format, and set of support is shown to be compatible with an A-ordering restriction; in any resolution operation under a linear format, the literal resolved upon in the near parent must be a maximal literal in that clause.The far parent must either be a merge, in which case the literal resolved upon must be a merge literal, or a member of the original set of clauses.A new kind of ordering, called C-ordering, is introduced and shown to be compatible with merge, linear format, and set of support resolution.Its advantage over A-ordering is that the literal to be resolved upon in the near parent is uniquely specified.