Horn - Klauseln

[ Zum Seminar "Programmierkonzepte und Programmiersprachen" ] ↔ [ Zum Inhalt ] ↔ [ Resolution ]

Übersicht:


Allgemeine Klauseldefinition


Klauseln sind Disjunktionen von Literalen, d.h. eine ODER-Verknüpfung von negativen und positiven Elementen.


Definition Horn - Klausel


Horn - Klauseln sind eine Einschränkung normaler Klauseln. Die Disjunktion bleib bestehen, jedoch darf es in der ganzen Klausel nur ein einziges positives Literal geben. Alle anderen müssen negiert sein.
Ein Beispiel:
A v ¬B v ¬C v ¬D
Das Gesetz der Kontraposition sagt folgendes aus:
¬p v q ↔ q ← p
 angewendet auf obige Klausel bekommen wir also
A ← B ^ C ^ D
und dieses ähnelt sehr den schon verwendeten Regeln ;) (welch ein Zufall).

Horn - Klauseln sind erforderlich wenn ein Klauseltheorembeweisverfahren angewendet wird und wie fortführend bewiesen wird, verwendet PROLOG solch ein verfahren, deswegen arbeitet es ausschließlich mit Horn - Klauseln.

Es gibt 4 veschiedene Arten der Horn - Klausel:
1.Assertion/Fakt
F ←
 wobei die rechte Seite aus Bedingungen die immer wahr sind besteht bzw. das true darstellt.Deswegen stimmt dieser Fakt, die Folgerung immer.

2.Implikation
F ← B1, B2,...Bn
 Die Folgerung F ist erfüllt, wenn alle Bedingungen (rechte Seite) als wahr ausgewertet werden.

3.Zielanweisung/Frage
← B1, B2,...Bn
Anfrage, was zutrifft wenn alle Bedingungen erfüllt werden.Auf der linken Seite kann man sich gedanklich ein false vorstellen.

4.Widerspruch
←
Der Wiederspruch "besteht" nur aus dem Implikationszeichen, auf dessen linker Seite sich das false befindet und auf dessen rechter Seite das true besteht.
Da dieses aber der Logik widerspricht (true kann nicht false implizieren) ist es folglich ein Widerspruch und daher auch dessen Name. ;)


Von Prädikatenklauseln zu Horn - Klauseln
Es gibt 3 Regeln die man anwenden kann um relativ einfach eine Umformung von allgemeinen (Prädikaten-)Klauseln zu Horn-Klauseln zu vollziehen.
1.Ein ODER wird durch zwei einzelne Klauseln realisiert, die jeweils die durch das ODER getrennte Bedingungen darstellen.
2.Variablen im Klauselkopf sind universell
3.Variablen im Klauselkörper sind existentiell

Ein Beispiel hierfür:

Ein natürlichsprachiger Satz:
X ist der Grossvater von Y, wenn X ein Elternteil von einem Elternteil von Y ist.
jetzt als Prädikatenklausel:
Für alle X, für alle Y, (existiert ein Z,elternteil(X,Z), elternteil(Z,Y)) → grossvater(X,Y).
und zum Finale als Horn - Klausel:
grossvater(X,Y) ← elternteil(X,Z), elternteil(Z,Y).

[ Zum Seminar "Programmierkonzepte und Programmiersprachen" ] ↔ [ Zum Inhalt ] ↔ [ Seitenanfang ] ↔ [ Resolution ]