Resolution inference rule
= Resolution inference rule
From <Boolean clauses> containing complementary <Boolean literals>, derive the <Boolean clause> formed by removing that complementary pair and taking the remaining <Boolean literals>. For example, resolving $p\lor\neg q$ with $\neg p\lor\neg r$ gives $\neg q\lor\neg r$. Backward proof search with a positive-headed <Horn clause> and an all-negative query is a restricted use of this rule.