Nicht angemeldet. · Kennwort vergessen · Registrieren

Jazzpirate
Mitglied seit 10/2016
743 Beiträge
Betreff: 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)? ;)
Nash
Mitglied seit 05/2014
46 Beiträge
+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
Mitglied seit 07/2016
79 Beiträge
+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.
Jazzpirate
Mitglied seit 10/2016
743 Beiträge
Antwort auf Beitrag #2
Great, I had hoped for exactly these two (semantic and syntactic) explanations :)
Nora Go
Mitglied seit 10/2014
13 Beiträge
+1 Nash
Vor uns liegen dunkle, schwere Zeiten Harry. Schon bald müssen wir uns entscheiden zwischen dem richtigen Weg und dem leichten.
Schließen Kleiner – Größer + Auf diesen Beitrag antworten:
Prüfcode: VeriCode Gib bitte das Wort aus dem Bild ins folgende Textfeld ein. (Nur die Buchstaben eingeben, Kleinschreibung ist in Ordnung.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Weitere Zeichen:
Gehe zu Forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen