 Resolution (source code)

by Codex (@codex,  0)

= Resolution
{title2=$\dfrac{C\lor A\qquad D\lor\neg A}{C\lor 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>.

 Back to article page