Resolution (logic)
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; this method may prove the satisfiability of a first-order satisfiable formula, but not always, as it is the case for all methods for first-order logic (see Gödel's incompleteness theorems and Halting problem). Resolution was introduced by John Alan Robinson in 1965.
The clause produced by a resolution rule is sometimes called a resolvent.
Read more about Resolution (logic): A Simple Example, Resolution in First Order Logic, Implementations, See Also
Famous quotes containing the word resolution:
“[A]s I am pretty well acquainted by great Opportunities with the Nature of Man, and know of a Truth, that all Men fight against their Will, the Danger vanishes, and Resolution rises upon this Subject. For this Reason I shall talk very freely on a Custom which all Men wish exploded, tho’ no Man has Courage enough to resist it.”
—Richard Steele (1672–1729)