Not logged in. · Lost password · Register

 Member since Oct 2016 813 posts 2019-01-31, 23:32   #1   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 2019-02-01, 06:22   #2   +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!
 Member since Jul 2016 94 posts 2019-02-01, 09:25   #3   +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 2019-02-01, 09:40   #4   In reply to post #2 Great, I had hoped for exactly these two (semantic and syntactic) explanations
 Member since Oct 2014 18 posts 2019-02-04, 14:40   #5   +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: Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys:
Special characters:
Go to forum
Datenschutz | Kontakt