logicartificial-intelligenceresolutionconjunctive-normal-form

Proof by resolution - Artificial Intelligence


I'm working with an exercise where I need to show that KB |= ~D.

And I know that the Knowledge Base is:

 - (B v ¬C) => ¬A
 - (¬A v D) => B
 - A ∧ C

After converting to CNF:

A ∧ C ∧ (¬A v ¬B) ∧ (¬A v C) ∧ (A v B) ∧ (B v ¬D)

So now I have converted to CNF but from there, I don't know how to go any further. Would appreciate any help. Thanks!


Solution

  • The general resolution rule is that, for any two clauses (that is, disjunctions of literals)

    P_1 v ... v P_n
    

    and

    Q_1 v ... v Q_m
    

    in your CNF such that there is i and j with P_i and Q_j being the negation of each other, you can add a new clause

    P_1 v ... v P_{i-1} v P_{i+1} ... v P_n v Q_1 v ... v Q_{j-1} v Q_{j+1} ... v Q_m
    

    This is just a rigorous way to say that you can form a new clause by joining two of them, minus a literal with opposite "signs" in each.

    For example

    (A v ¬B)∧(B v ¬C)
    

    is equivalent to

    (A v ¬B)∧(B v ¬C)∧(A v ¬C),
    

    by joining the two clauses while removing the opposites B and ¬B, obtaining A v ¬C.

    Another example is

    A∧(¬A v ¬C)
    

    which is equivalent to

    A∧(¬A v ¬C) ∧ ¬C.
    

    since A counts as a clause with a single literal (A itself). So the two clauses are joined, while A and ¬A are removed, yielding a new clause ¬C.

    Applying this to your problem, we can resolve A and ¬A v ¬B, obtaining ¬B. We then resolve this new clause ¬B with B v ¬D, obtaining ¬D.

    Because the CNF is a conjunction, the fact that it holds means that every clause in it holds. That is to say, the CNF implies all of its clauses. Since ¬D is one of its clauses, ¬D is implied by the CNF. Since the CNF is equivalent to the original KB, the KB implies ¬D.