Least Model eines Horn-Programms?

SideWinder

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