Two Results on Ordering for Resolution with Merging and Linear Format

Abstract

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.