- Hornklausel
-
Horn-Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US-amerikanischen Logiker Alfred Horn.
Inhaltsverzeichnis
Definition mit Horn-Klauseln
Eine Horn-Klausel ist eine Klausel mit höchstens einem positiven Literal, d.h. höchstens einem Literal, in dem die Variable nicht negiert vorkommt. 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 (positiv) auftritt.
Beispiele
- (die dritte Horn-Klausel hat kein, die beiden anderen Horn-Klauseln haben je ein positives Literal)
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).
Erfüllbarkeit
Mit Hilfe des Markierungsalgorithmus können Horn-Formeln in Polynomialzeit auf Erfüllbarkeit getestet werden (folglich ist HORNSAT 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).
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.
Siehe auch
Wikimedia Foundation.