[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
My mis-statement in class about the standard resolution refutation proof error
- To: Rao Kambhampati <rao@asu.edu>
- Subject: My mis-statement in class about the standard resolution refutation proof error
- From: Subbarao Kambhampati <rao@asu.edu>
- Date: Tue, 10 Apr 2012 21:34:28 -0700
- Dkim-signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; bh=rPy94854yj4kBq8cmQCCLFlFlyWASCBFeG+gzdvrbdc=; b=U2mRkPvH5OHaWQ1s8x/kteudM/dygfd98kDbOFbAi+b2mnu+MQdkaR4wvU5hHFB3/J TbtIz8sIOkQlC4A1MROlir73smvOWfGta4fl6XoiJOFqhylr11NtXIiH1EK7uBCyRcge 4O0eTPpyF3tNbUukYCU8Y/l5fOTcBWsbwjeL1D8+Dh48UGNa+qKn9qTEbP4i2fBhhtps 7Tx/bRAgzPPYbNTcQgweQCnv0LxkoxVFFLVwgqQzjEqYmGL86v/500tt8U99j2Inyjoa JfZLIcj7Bm1amnGulimjmGgA/2bKaqRsk872RkKrkSveDrdJuQ7RI8JYnXsVKLlx8b/u 5PfQ==
- Sender: subbarao2z2@gmail.com
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).
Rao