The predicate elimination strategy in theorem proving
Raymond Reiter · 1970
The predicate elimination strategy is a complete resolution proof strategy for multi-predicate formulas. Essentially, the procedure focuses on one of the predicate symbols P, and attempts to deduce clauses independent of P by means of resolution in which only predicates in P are “resolved away” from parent clauses. The completeness theorem states that one can in this way, deduce an unsatisfiable P-independent set of clauses, provided the given set is unsatisfiable.