S
Ich habe Probleme Answer-Sets zu bestimmen. Folgendes Horn-Programm:
a v b :- .
// ist gleichbedeutend mit:
a oder b :- true. // Regel feuert also immer
Nun soll ich die Answer-Sets berechnen, mein Solver-Programm (DLV http://www.dbai.tuwien.ac.at/proj/dlv/ ) sagt mir schonmal die Lösung: {a} und {b} sind die Answer-Sets.
Leider weiß ich nicht wie ich dorthin komme...
Die möglichen Modelle sind: {}, {a}, {b}, {a,b}
Ein Answer-Set oder Stable-Model wird mit dem Redukt des Programms definiert. Wobei das Redukt folgendes ist:
- Alle Regeln aus dem Porgramm eliminierendie "not x" enthalten wobei x € M ist
- Danach alle "not y" aus den restlichen Regeln entfernen
Wobei "not y" die Default-Negation ist, keine starke Negation.
Dabei gibt es in diesem Programm imho nichts zu erledigen...dieses Redukt ist nun ein Horn-Programm. Es hat ein Least-Model, falls das Least-Model dieses Horn-Programms = dem Modell von oben ist, dann ist dieses Modell ein Answer-Set.
(a) Wie bekomme ich das Least-Modell eines Answer-Sets? Solange Regeln anwenden bis keine mehr durchführbar sind, oder? Falls ja was heißt das in diesem Fall? Ich erhalte immer Least-Model = {a oder b} -> also niemals das Modell?! Das kann ja nicht sein.
(b) Wie behandle ich das "oder" da korrekt...
Hoffe irgendjemand kann helfen und hat soetwas schonmal gemacht.
EDIT:
(a) Antwort auf http://www.dlvsystem.com/dlvsystem/html/DLV_User_Manual.html#AEN311
(b) Das "oder" ist exklusiv.
MfG SideWinder