Resolution

[Ali Helmy]

Hey lads,

I want to make sure I got something correctly

In page 215, in the Simple Conversion Procedure to CNF, we start with the statement [B1,1 iff (P1,2 OR P2,1)] , then we end up with [(!B1,1 OR P1,2 OR P2,1) AND (!P1,2 OR B1,1) AND (!P2,1 OR B1,1)] which is said 'can be used as an input to a resolution procedure...

My problem is, what do we get if we DO input it to a resolution procedure?

1. taking the first two: (!B1,1 OR P1,2 OR P2,1) AND (!P1,2 OR B1,1)
• we can infer (P1,2 OR P2,1 OR !P1,2) by removing !B1,1 with B1,1
• then by simple logic, we can remove P1,2 with !P1,2 to get (P2,1)
2. now by combining the result of the first two (P2,1) with the next clause (!P2,1 OR B1,1)
• we can infer B1,1, which is already what we know

So, as far as I can understand, that is what is meant by Refutation Completeness property of Resolution...

Sa7?

--
Cheers,
     Seth
     <A. Helmy>
==================
  One Life... LIVE It
==================