Resolution Prover

The main principle behind resolution proofs is the following rule of inference, known as Resolution:
(A ∨ B) ∧ (¬B ∨ C) ⊨ (A ∨ C)
With Resolution, we take two clauses D1 and D2, where D1 contains p, and D2 contains Np, and then add a new clause constisting of the elements of D1 "minus" p and D2 "minus" Np. In English: we take p out of one clause, and Np out of the other one, and then combine the clauses to make a new one.
Example: Resolving [p, Krs] and [Np, Aqs] "on" p yields [Krs, Aqs].

In constructing a resoluton proof, we follow two procedures: First, we translate the initial propositions into Conjunctive Normal Form (CNF); then, we repeatedly apply Resolution as many times as possible. In CNF, propositions are represented as conjunctions of disjunctions of literals. (E.g., (p ∨ (q ∧ r)) becomes ((p ∨ q) ∧ (p ∨ r)).)

In our proofs, clauses are represented as lists of propositions. A clause (e.g., [Cpq, Nq, r]), represents the universal DISJUNCTION of its members (i.e., Cpq ∨ Nq ∨ r). Each line of our proof represents a set of clauses, where a set of clauses represents the universal CONJUNCTION of its members. For example: 〈[Cpq, Nq, r], [Kst]〉 is equivalent to: (Cpq ∨ Nq ∨ r) ∧ (Kst)

Like tableaux, resolution proofs involve proof by refutation. In a proof by refutation, the proof assumes the NEGATION of the desired conclusion, along with any (optional) premises. We then convert the premises into CNF and repeatedly apply Resolution for as long as possible, or until we derive the empty clause ( [ ] ). If the proof derives the empty clause, then the argument is valid. If no more rules can be applied, and the empty clause has not been derived, then the argument is invalid.