Horn-Formel
aus Wikipedia, der freien Enzyklopädie
Horn-Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US-amerikanischen Logiker Alfred Horn.
Inhaltsverzeichnis |
[Bearbeiten] Definition mit Horn-Klauseln
Eine Horn-Formel ist eine Konjunktive Normalform (das heißt eine Konjunktion von Disjunktionen), bei der jeder Disjunktionsterm eine Horn-Klausel ist, also eine Disjunktion von Literalen, von denen höchstens eines unverneint auftritt.
[Bearbeiten] Beispiele
- (die dritte Horn-Klausel hat kein, die beiden anderen Horn-Klauseln haben je ein positives Literal)
[Bearbeiten] Darstellungsformen von Horn-Klauseln
Horn-Klauseln lassen sich nach den Regeln der Aussagenlogik auch als materiale Implikationen 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 |  |
 |
 sind nicht alle wahr |
| definite Hornklausel | Genau ein positives Literal |  |
 |
Wenn wahr sind, dann ist auch y wahr |
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 (HORNSAT ist sogar P-vollständig). Man kann also in Polynomialzeit feststellen, ob eine Variablenbelegung (eine Zuordnung von Wahrheitswerten zu den in in der Horn-Formel vorkommenden Literalen) 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. So werden in der Programmiersprache Prolog Programme als Horn-Klauseln angegeben.
