Resolution for Propositional Logic

Created on March 6, 2013, 1:45 a.m. by Hevok & updated by Hevok on May 2, 2013, 5:35 p.m.

The basic steps of Resolution in Propositional Logic is based on finding a Contradiction of the negated form of the Knowledge base.

Considering one has two Clauses conjunctive connected so one has a Clausal Form. So both of these Clauses contain the Variable p, one has p and the other has not p, so the negated form. If this Clausal Form is True, then of course one of both either p or not p must be wrong. Therefore, when one removes p and not p from these two Clauses then it must still be true, otherwise it wouldn't be true with the two.

So the basic step is that if one has in an Clause a Literal and in the other its Negation, the it holds that one can remove this Literal from the Clause because it holds if one removes it, the clause that results from its removal also must be True.

On the other hand if one says that the Clause without the Literal p, is a Contradiction, then of course also the clause with p and not p must also be a Contradiction.

  • if (p1 ∨ ... ∨ pk ∨ p ∨ ¬q1 ∨ ... ∨ ¬ ql) ∧ (r1 ∨ ... ∨ rm ∨ ¬p ¬s1 ∨ ... ∨ ¬sn) is true, then:

    • One of both p, ¬p has to be wrong
    • Therefore: One of the other Literals must be true, i.e.

      p1 ∨ ... ∨ pk ∨ ¬q1 ∨ ... ∨ ¬ ql ∨ (r1 ∨ ... ∨ rm ∨ ¬s1 ∨ ... ∨ ¬sn

      must be true.

  • Therefore:

if p1 ∨ ... ∨ pk ∨ ¬q1 ∨ ... ∨ ¬ ql ∨ (r1 ∨ ... ∨ rm ∨ ¬s1 ∨ ... ∨ ¬sn is a

Contradiction, then

(p1 ∨ ... ∨ pk ∨ p ∨ ¬q1 ∨ ... ∨ ¬ ql) ∧ (r1 ∨ ... ∨ rm ∨ ¬p ¬s1 ∨ ... ∨ ¬sn)

is also a Contradiction.

If Clause K1 and Clause K2 are transformed during a Resolution step to a Clause K3.

So having a Knowledge Base or Theory that contains Clause K1 and Clause K2, one can entail from them Clause K3, where K3 does not contain Variable p which is i both of the Clauses on the one hand not negated and on the other hand negated. So the two Clauses K1 and K2 can be transformed into a new Clause K3.

Then one procedure with all the Clauses by removing the same Literals that are in one Clause negated and in the other not negated. One will come to an end where Clauses are resolved that consists of an Atom and its negated Atom. Then one will receive the empty Clause. With this one has shown that there is an Contradiction.

  • Resolution stop {K1, K2} ⊨ K3
  • Two Clauses K1``` andK2are transformed into a new oneK3``
  • End of the resolution procedure:
  • if Clauses are resolved that consist only of an atom and the negated atom, then a new "empty clause" can be resolved.

In general a Contradiction is deduced from a set of Clauses is done in the following way. Considering we have a set M of Clauses what we do then is to select two Clauses from M and try to create a new Clause via a Resolution Step. If the new Clause is then already the empty Clause, then a Contradiction has been found and if not the new Clause is added to the Set and one continuous with Step one and select another two Clauses. This procedure is for Propositional Logic correct and also complete.

  • How to deduce a Contradiction from a set M of clauses:

    1. Select two Clauses from M and create a new Clause K via a Resolution step.
    2. If K = ⊥, then a contradiction as been found.
    3. If K ≠ ⊥, K is added to the set M, continue with step 1.
  • The Resolution Calculus (for Propositional Logic) is correct and complete

I order to proof that a Formula ψ is a logical Consequence of a Knowledge Base or Theory Φ of Clauses (so that Φ can be entailed by ψ) on computes the Negation of the Implication that Φ implies ψ, which is a Contradiction. So one has not Φ implies ψ which is equivalent to Φ and not ψ. Next one determines the Clausal Form of this Formula, then we simply select two clauses from this Formula and try to create a new Clause with a Resolution Step. if the newly created Clause is the empty Clause, then a Contradiction has been found and we are done because then it holds that the original Formula really holds or is true, so Φ entails ψ. On the other hand, if the formula that is the result of the Resolution step is not the empty Clause, then we add this formula to our Knowledge Base/Theory and one continuous with step 3.

With the help of Resolution on wants to identify a Contradiction.

  • How to proof that a Formula ψ is a logical Consequence of a Knowledge Base (Theory) Φ of Clauses, i.e. Φ ⊨ ψ?

  • Compute the negation of Φ → ψ, which is a contradiction: ¬(Φ → ψ) ≣ Φ ∧ ¬ ψ

  • Determine the Clausal form of Φ ∧ ¬ ψ
  • Select two Clauses from Φ ∧ ¬ ψ and create a new Clause K via a Resolution step.
  • If K = ⊥, then a Contradiction has been found.

    It holds that Φ ⊨ ψ, q.e.d.

  • If K ≠ ⊥, K is added to the set Φ ∧¬ ψ,

    continue with step 3.

  • example

  • Knowledge Base Φ
    • If it rains, Jane brings her umbrella r -> u
    • If Jane has an umbrella, she doesn't get wet u -> ¬w
    • If it doesn't rain, Jane doesn't get wet ¬r -> ¬w
  • Formula ψ

    • Now, prove that Jane doesn't get wet ¬w
  • Transform Knowledge Base into Clausal Form

    • r -> u = ¬r ∨ u = {¬r,u}
    • u -> ¬w = ¬u ∨ ¬w = {¬u,¬w}
    • ¬r -> ¬w = r ∨ ¬w = {r,¬w}
  • Add negated formula to Knowledge Base
    • ¬¬w = w
    • New Knowledge Base Φ∧¬ψ
      1. {¬r,u}
      2. {¬u,w}
      3. {r,¬w}
      4. {w}
  • Start Resolution

       (3,4) {r,¬w}
       5.    {r}
       (2,4) {¬u,¬w}
       6.    {¬u}
       (1,5) {¬r,u}
       7.    {u}
       (6,7) {¬u}
  • We have found a Contradiction in Φ∧¬ψ,

    therefore it holds that Φ ⊨ ψ, q.e.d.


Tags: knowledge, logic, correctness, contradiction, proof
Categories: Concept
Parent: Resolution

Update entry (Admin) | See changes

Comment on This Data Unit