Horn-Formel

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

Horn-Formeln sind eine wichtige Art prädikatenlogischer Formeln. Sie spielen eine zentrale Rolle in der logischen Programmierung und sind von Bedeutung für die konstruktive Logik. Benannt wurden sie nach dem US-amerikanischen Logiker Alfred Horn.

Definition[Bearbeiten]

Unter einer Klausel, auch Disjunktionsterm genannt, versteht man die Disjunktion

\phi_1 \vee \phi_2 \vee ... \vee \phi_n

von Literalen, wobei jedes Literal \phi_i\!\; entweder ein atomarer Ausdruck oder ein negierter atomarer Ausdruck ist.

Eine Horn-Klausel ist eine Klausel mit höchstens einem positiven Literal, d. h. mit höchstens einem Literal, dessen atomarer Ausdruck nicht negiert ist.

Im Spezialfall der Aussagenlogik sieht eine typische Horn-Klausel also so aus:

\neg p \or \neg q \vee \cdots \vee \neg t \vee u

In diesem Fall sind bis auf u\!\; alle atomaren Ausdrücke (in diesem Beispiel sind es Aussagenvariablen) negiert.

Eine Horn-Formel ist eine konjunktive Normalform (das heißt eine Konjunktion von Disjunktionen), bei der jeder Disjunktionsterm eine Horn-Klausel ist.

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[Bearbeiten]

Horn-Klauseln lassen sich nach den Regeln der Aussagenlogik auch als materiale Implikationen darstellen. So gilt im einfachsten Fall einer Horn-Klausel mit zwei Literalen bekanntlich:

\neg \phi \vee \psi = \phi \Rightarrow \psi

Gemäß Definition kann eine Horn-Klausel genau ein oder gar kein nicht-negiertes Atom enthalten. Außerdem kann es vorkommen, dass gar keine Literale mit negierten atomaren Ausdrücken auftreten. Es gibt also drei Grundtypen von Horn-Klauseln. Die folgende Tabelle gibt einen Überblick über diese drei möglichen Formen einer Horn-Klausel, 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
Faktenklausel Keine negativen Literale y\!\; 1 \Rightarrow y y\!\; ist wahr

Erfüllbarkeit[Bearbeiten]

Mit Hilfe des Markierungsalgorithmus können Horn-Formeln in Polynomialzeit auf Erfüllbarkeit getestet werden (zudem ist HORNSAT P-vollständig). Man kann also in Polynomialzeit feststellen, ob eine Variablenbelegung (eine Zuordnung von Wahrheitswerten zu den in der Horn-Formel vorkommenden Literalen) existiert, für welche 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[Bearbeiten]

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

Quellen[Bearbeiten]

Siehe auch[Bearbeiten]