First-order resolution
= 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.