 First-order resolution

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.