Abstract
Many of the known refinements of the first order resolution rule of J. A. Robinson suffer from various redundancies, which have a common underlying cause, which we identify as "lack of ground faithfulness". We say a refinement is ground faithful if for each deduction, D, in the refinement, there exists at least one "ground instance" of D, which is also in the refinement. In this report it is shown how certain refinements which are not ground faithful can be modified, both in a theoretical and an implementation sense, into ground faithful versions. This modification yields a stronger refinement than refinement. In practice Ground faithfulness can be achieved for many refinements by the addition to each clause of a notational device, called the constraint of the clause. The approach emphasizes that resolution clauses are the result of deductions, and the notational device constrains clauses based on information contained in the deductions of the individual clauses. Also presented are some overall characteristics and properties both of refinements, and of the methods of defining refinements, which provides a common qualitative framework for understanding the various specific refinements presented.