Resolution ($\frac{C\vee AD\vee \neg A}{C\vee D}$)

An inference rule deriving a clause from two clauses containing complementary literals. In propositional logic the displayed rule eliminates the atom $A$. For first-order clauses, complementary atoms can first be made identical by a suitable first-order substitution.

A rule that combines first-order clauses by unifying complementary first-order literals and retaining the other literals under the resulting first-order substitution. Completeness requires the appropriate calculus and search conditions.

A family of resolution calculi for first-order Horn clauses. A selection function chooses either the positive head atom alone or a nonempty set of body atoms. Permitted inferences respect those choices; fair saturation is refutationally complete. Function symbols need not be excluded, so completeness does not by itself guarantee termination. ^[ref]

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.