An inference rule deriving a clause from two clauses containing complementary literals. In propositional logic the displayed rule eliminates the atom . For first-order clauses, complementary atoms can first be made identical by a suitable first-order substitution.
New to topics? Read the docs here!