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\vee \neg q$ with $\neg p\vee \neg r$ gives $\neg q\vee \neg r$. Backward proof search with a positive-headed Horn clause and an all-negative query is a restricted use of this rule.