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).
Rao
No comments:
Post a Comment