Logic Resolution

See: Mathematical Logic, Automated Theorem Proving, Inference, Reductio ad Absurdum, Theorem-Proving, Propositional Logic, First-Order Logic, Propositional Formula, David-Putnam Algorithm, Ground Instance, Unification (Computer Science), Refutation Completeness.

References

(Wikipedia, 2014) ⇒ http://en.wikipedia.org/wiki/resolution_(logic) Retrieved:2014-12-30.
- In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic. In other words, iteratively applying the resolution rule in a suitable way allows for telling whether a propositional formula is satisfiable and for proving that a first-order formula is unsatisfiable. Attempting to prove a satisfiable first-order formula as unsatisfiable may result in a nonterminating computation; this problem doesn't occur in propositional logic.
  The resolution rule can be traced back to Davis and Putnam (1960); ^[1] however, their algorithm required to try all ground instances of the given formula. This source of combinatorial explosion was eliminated in 1965 by John Alan Robinson's syntactical unification algorithm, which allowed one to instantiate the formula during the proof "on demand" just as far as needed to keep refutation completeness.
  The clause produced by a resolution rule is sometimes called a resolvent.