Bin gerad auf Seite 7-15 auf folgende Fragen gestoßen:

Welches Ergebnis liefert der Markierungsalgorithmus
- Wenn es keine Klauseln der Form (T -> Ai) gibt ?
- Wenn es keine Klauseln der Form (A1 ^ A2 ^ … ^ An) -> _|_ gibt ?
(hier soll _|_ = bottom sein )

Begründen Sie, warum dieses Ergebnis korrekt ist.
Greifen Sie dazu auch die Erläuterungen zu 7.4 und 7.6 zu.

Was passiert,
Wenn es keine Klauseln der Form (A1 ^ A2 ^ .. ^ An) -> A gibt?

Ich kann keine der Fragen befriedigend beantworten [img]http://www.fb18.de/gfx/9.gif[/img]
- kann mir da jemand weiterhelfen?

- Wenn es keine Klauseln der Form (T -> Ai) gibt ?

wenn (T ->[img]http://mokrates.de/cgi-bin/texstring?A_%7Bi%7D[/img]) nicht existiert, wird keines markiert. Damit ist der Makierungsalgorithmus schon vor dem ersten Durchlauf korrekt.
Das bedeutet nichts anderes, als dass die Formel erfüllbar ist.

- Wenn es keine Klauseln der Form (A1 ^ A2 ^ … ^ An) -> _|_ gibt ?

Auch in desem Fall ist die Formel erfüllbar.
Wir gehen davon aus, dass mindestens ein [img]http://mokrates.de/cgi-bin/texstring?A_%7Bi%7D[/img] nicht makiert ist, damit die Formel erfüllbar ist. Dass heisst es gilt A([img]http://mokrates.de/cgi-bin/texstring?A_%7Bi%7D[/img])= 0 und deswegen A(K) = 1 (Lemma 7.6)

Wenn es keine Klauseln der Form (A1 ^ A2 ^ .. ^ An) -> A gibt?

Trivial, überlege Dir mal, wie die Hornformel in diesem Fall aussehen muss.

[Edit] falsches Posting gelöscht

Also wenn es keine Klauseln der Form (A1 ^ A2 ^ … ^ An) -> A gibt,
dann kann es nur Hornklausel der Form (A1 ^ A2 ^ … ^ An) -> _|_
(ursprüngliche Hornklausel hatte nur negative Literale)
& T -> A1 ( nur ein positives Literal) geben.
Kann es dann nicht zu beiden Endresultaten kommen:
Fall_1
Es gibt genügend Formeln der Art T -> A1 so dass alle
(A1 ^ A2 ^ … ^ An) der Formel (A1 ^ A2 ^ … ^ An) -> _|_ markiert werden -> unerfüllbar
Fall_2
Es werden nicht alle (A1 ^ A2 ^ … ^ An) markiert -> erfüllbar
?

[Edit] falsches Posting gelöscht

Also wenn es keine Klauseln der Form (A1 ^ A2 ^ … ^ An) -> A gibt,
dann kann es nur Hornklausel der Form (A1 ^ A2 ^ … ^ An) -> _|_
(ursprüngliche Hornklausel hatte nur negative Literale)
& T -> A1 ( nur ein positives Literal) geben.
Kann es dann nicht zu beiden Endresultaten kommen:
Fall_1
Es gibt genügend Formeln der Art T -> A1 so dass alle
(A1 ^ A2 ^ … ^ An) der Formel (A1 ^ A2 ^ … ^ An) -> _|_ markiert werden -> unerfüllbar
Fall_2
Es werden nicht alle (A1 ^ A2 ^ … ^ An) markiert -> erfüllbar
?

^
|

ist das richtig?

ja