Ground resolution
= Ground resolution
The use of <resolution> on <ground clauses>. A finite refutation ends in the empty <ground clause> and establishes unsatisfiability of the chosen ground instances. <Herbrand's theorem> explains the completeness of searching for such refutations for universal equality-free <first-order clauses>.