 Of the many calculi used in the implementation of reasoning programs, the ones based on the resolution principle have been the most popular. Resolution is modeled after the chain rule (of which Modus Ponens is a special case) and essentially states that from p ∨ q and ~q ∨ r one can infer p ∨ r. More formally, let C − l denote the clause C with the literal l removed. Assume that C1 and C2 are ground clauses containing, respectively, a positive literal l1 and a negative literal ~l2 such that l1 and ~l2 are complementary. Then, the rule of ground resolution states that, as a result of resolving C1 and C2, one can infer (C1 − l1) ∨ (C2 − ~l2):