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.

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

Tags: knowledge, logic, correctness, contradiction, proof
Categories: Concept
Parent: Logic
Children: Resolution for Propositional Logic, Resolution of First Order Logic

Update entry (Admin) | See changes

Comment on This Data Unit