A Unifying View of Some Linear Herbrand Procedures

Abstract

The linked conjunct, resolution, matrix reduction, and model elimination proof procedures constitute a nearly exhaustive list of the basic Herbrand proof procedures introduced in the 1960's. Each was introduced as a hopefully efficient complete procedure for the first order predicate calculus for the purpose of mechanical theorem proving. This paper contains a demonstration that versions of these procedures can be highly related in their design. S-linear resolution, a particular strategy of resolution previously proposed, is seen to possess a natural refinement isomorphic at ground level to a refinement of the model elimination procedure. There is also an isomorphism at the general level between a less natural s-linear resolution refinement and the model elimination refinement. The model elimination procedure is also interpreted within the linked conjunct and matrix reduction procedures. An alternate interpretation of these results is that, very roughly, the procedures other than resolution can be viewed as forms of linear resolution. © 1972, ACM. All rights reserved.