Wir betrachten die Menge H = {{¬p,¬t,s}, {r}, {¬q,¬r,s}, {¬t, p}, {t}, {¬r,¬t,¬s}} von Hornklauseln.
(a) Bestimmen Sie die minimale erfüllende Interpretation der nicht-negativen Klauseln aus H. Entscheiden Sie, ob H
erfüllbar ist.
(b) Geben Sie einen Ableitungsbaum im Resolutionskalkül an, welcher aus der Klauselmenge H herleitet.
(c) Bei der Einheitsresolution darf die Resolvente zweier Klauseln nur gebildet werden, wenn eine der Klauseln aus
einem einzelnen Literal besteht. Zeigen Sie: Die Einheitsresolution ist im Allgemeinen nicht vollständig, für Hornklauseln
aber schon.
