Horn-Formel

aus Wikipedia, der freien Enzyklopädie

Du hast neue Nachrichten auf deiner Diskussionsseite.

Horn-Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US-amerikanischen Logiker Alfred Horn.

Inhaltsverzeichnis

1 Definition
2 Darstellungsformen von Horn-Klauseln
3 Erfüllbarkeit
4 Anwendung
5 Siehe auch

[Bearbeiten] Definition

Horn-Formeln sind eine Konjunktion mehrerer Horn-Klauseln. Während der Begriff Klausel allgemein eine Disjunktion von Literalen beschreibt (Oder-Verknüpfung von positiven oder negativen Literalen), darf bei der Horn-Klausel nur höchstens ein Literal positiv sein.

[Bearbeiten] Darstellungsformen von Horn-Klauseln

Horn-Klauseln lassen sich nach den Regeln der Aussagenlogik auch als Implikation darstellen. Die folgende Tabelle gibt einen Überblick über die zwei möglichen Typen einer Horn-Klausel und ihre Form sowohl als Disjunktion als auch als Implikation.

Name	Beschreibung	Disjunktion	Implikation	In Worten
Zielklausel	Kein positives Literal	$\neg x_1 \vee \ldots \vee \neg x_n$	$x_1 \wedge \ldots \wedge x_n \rightarrow 0$	$x_1, \ldots, x_n$ ergeben eine falsche Aussage
definite Hornklausel	Genau ein positives Literal	$\neg x_1 \vee \ldots \vee \neg x_n \vee y$	$x_1 \wedge \ldots \wedge x_n \rightarrow y$	$x_1, \ldots, x_n$ führen zu $y$

Die Anzahl der negativen Literale (n) kann für Klauseln mit genau einem positiven Literal auch 0 sein (teilweise lässt man auch die leere Klausel als Zielklausel zu).

[Bearbeiten] Erfüllbarkeit

Mit Hilfe des Markierungsalgorithmus können Horn-Formeln in Polynomialzeit auf Erfüllbarkeit getestet werden. Man kann also in Polynomialzeit feststellen, ob eine Variablenbelegung existiert, für die die Horn-Formel wahr wird. Im Unterschied dazu wird vermutet, dass allgemein für aussagenlogische Formeln kein Polynomialzeit-Algorithmus existiert (siehe Erfüllbarkeitsproblem der Aussagenlogik).

[Bearbeiten] Anwendung

Die Bedeutung der Horn-Klauseln liegt zum Beispiel in der Informatik beim maschinellen Schließen. In der Programmiersprache Prolog zum Beispiel werden Programme als Horn-Klauseln angegeben.