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.

Instead of proofing that a formula is a Tautology, it deducts a logical Contraction from its negation

Considering one has aTheory 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: {F1,...,Fn} with F0 as logical Consequence
{F1,...,Fn} ⊨ F0
F1 ∧ ... ∧ Fn → F0 is a Tautology
¬(F1 ∧ ... ∧ Fn → F0) is a contradiction
G1 ∧ ... ∧ Gk is a contradiction

The Resolution procedure allows the Entailment of a Contradiction from G1 ∧ ... ∧ Gk.

## Comment on This Data Unit