Horn-Formel
Horn-Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem österreichischen Logiker Alfred Horn.
| Inhaltsverzeichnis |
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.
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.
| Beschreibung | Disjunktion | Implikation | In Worten |
|---|---|---|---|
| Kein positives Literal | 
| 
|  ergeben eine falsche Aussage
|
| Genau ein positives Literal | 
| 
| führen zu y
|
Die Variable n kann für Klauseln mit genau einem positiven Literal auch 0 sein.
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).
Anwendung
Die Bedeutung der Horn-Klauseln liegt zum Beispiel in der Informatik beim maschinellen Schließen. Eine bekannte Programmiersprache mit Horn-Klauseln ist Prolog.