A Resolution is an automatic to proof that a [Knowledge](/blog/691/) Base is correct.
Resolution is an automatic way to deduce or infer whether a given Formula or Knowledge Base contains a Contradiction or if there is a satisfying Assignment for that Knowledge Base. These Technique relies on the Clausal Form and is much easier done in the Clausal Form.
Resolution is based on simple Deduction Rules and is a special Form of Enumeration
Instead of proofing that a formula is a Tautology, it deducts a logical Contraction from its negation
Considering one has a Theory consisting of the Formulas/Clauses F1 to Fn and one says F0 is a logical Consequence of this Theory. So F0 is entailed by this Theory. Then one can go back to Logical Statements which says that if one forms a Conjunctions of all these Clauses, then it can be implied that also F0 holds, which is a Tautology by a simple equivalence Transformation. When one negate this, then one has the Negation of the Formula. A Negation of this Formula must be a Contradiction. When not negated it is a Tautology. This is simply transformed into a Clausal Form. On this Clausal Form one can show that there is a Contradiction, because resolution is able to show that there is a logical Contradiction. Therefore by proving that there is a Logical Contradiction inside that, one shows that the first assumption holds, that this Theory really entails F0. So F0 is a logical Consequence of this Knowledge Base with F1 to Fn.
Thus, the basics of Resolution is proving a Tautology by deducing a logical Contradiction from its Negation.
Equivalent Assertions
[Theory](/blog/400/): {F1,...,Fn} with F0 as logical Consequence
{F1,...,Fn} ⊨ F0
F1 ∧ ... ∧ Fn → F0 [is a](/blog/221/) Tautology
¬(F1 ∧ ... ∧ Fn → F0) [is a](/blog/221/) contradiction
G1 ∧ ... ∧ Gk [is a](/blog/221/) contradiction