Hornformel

Hornformel

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

  • (\neg P \vee \neg Q \vee R) \wedge (P \vee \neg Q \vee \neg S) \wedge (\neg R \vee \neg S)
(die dritte Horn-Klausel hat kein, die beiden anderen Horn-Klauseln haben je ein positives Literal)
  • (x_1 \vee \neg x_2 \vee \neg x_3) \wedge (\neg x_1 \vee \neg x_2 \vee \neg x_3 \vee x_4)

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 \neg x_1 \vee \ldots \vee \neg x_n x_1 \wedge \ldots \wedge x_n \rightarrow 0 x_1, \ldots, x_n sind nicht alle wahr
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 Wenn x_1, \ldots, x_n 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.

Игры ⚽ Нужен реферат?

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”