Created on March 6, 2013, 1:39 a.m. by Hevok & updated by Hevok on May 2, 2013, 5:35 p.m.
A Resolution is an automatic to proof that a Knowledge 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.
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: {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
Comment on This Data Unit