Tuesday, April 10, 2012

My mis-statement in class about the standard resolution refutation proof error

In class, I said that a standard error that I had pointed out to you during resolution refutation class was still made by 3-4 people in the class.

Actually I mis-spoke. 

The error that students did in the exam was  to say that

~(A V B) resolves with A VB to give empty clause.

This is semantically correct (~(A V B) is indeed inconsistent with A V B and allows us to derive false) but syntactically wrong in that ~(A V B) is not in the clausal form.

If you put it in clausal form you will get two clauses, ~A and ~B which can then be resolved with AV B in sequence to get empty clause.

The error I had pointed out in the class earlier was a more egregious one in that it is both syntactically and semantically incorrect.
This one involves saying  ~A V ~B resolves with A V B  giving empty clause. 

Here ~A V ~B is not actually inconsistent with A V B (The world  A=True, B =False, is a model of both formulas, for example). 


No comments:

Post a Comment