Not logged in. · Lost password · Register

Member since Oct 2016
813 posts
Subject: Resolution - popular error
Since I'm not sure this was pointed out in the lecture explicitly, but it has been an issue every year for many students:

Assume we have two clauses {A,-B} and {-A,B} - can I resolve both literals in one step and conclude an empty clause directly? If so/not, why (not)? ;)
Member since May 2014
48 posts
+1 Jazzpirate
*waves hand vigorusly*
*does not wait for a response*

No, because resolving {A,-B} and {-A,B} to an empty clause would mean that this term is unsatisfiable. However, since {A,-B} and {-A,B} actually means (A or -B) and (-A or B), which is satisfiable (Model: A = true, B = true), resolving to empty clause would be wrong.

*classroom cheers*

5 points for Gryffindor!
Jonas S
Member since Jul 2016
94 posts
+1 Jazzpirate
The purely syntactical answer:
Resolving {A,-B} and {-A,B} gets us {A,-A} and {B,-B}, and now we cannot get any new resolvents.
Member since Oct 2016
813 posts
In reply to post #2
Great, I had hoped for exactly these two (semantic and syntactic) explanations :)
Nora Go
Member since Oct 2014
18 posts
+1 Nash
Vor uns liegen dunkle, schwere Zeiten Harry. Schon bald müssen wir uns entscheiden zwischen dem richtigen Weg und dem leichten.
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen