Change: Resolution

created on March 6, 2013, 1:39 a.m. by Hevok & updated on March 6, 2013, 1:39 a.m. by Hevok

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.

• 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: {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.

---

See entry | Admin

---

Back to top

---