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.
New to topics? Read the docs here!