Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
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)? 
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!
1 „Gefällt mir“
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.
1 „Gefällt mir“
Great, I had hoped for exactly these two (semantic and syntactic) explanations 
Vor uns liegen dunkle, schwere Zeiten Harry. Schon bald müssen wir uns entscheiden zwischen dem richtigen Weg und dem leichten.
1 „Gefällt mir“