Horn-Formel

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

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

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

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

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

• H. D. Ebbinghaus, J. Flum, W. Thomas: Einführung in die mathematische Logik. Mannheim-Leipzig-Wien-Zürich; BI-Wiss. Verlag, 1992, ISBN 3-411-15603-1
•  Wolfgang Rautenberg: Einführung in die Mathematische Logik. 3. Auflage. Vieweg+Teubner, Wiesbaden 2008, ISBN 978-3-8348-0578-2 (http://www.springerlink.com/content/978-3-8348-0578-2/).
• Hans-Peter Tuschik, Helmut Wolter: Mathematische Logik - kurzgefasst. Grundlagen, Modelltheorie, Entscheidbarkeit, Mengenlehre. Mannheim-Leipzig-Wien-Zürich; BI-Wiss. Verlag, 1994, ISBN 3-411-16731-9

Siehe auch

• Gentzenscher Hauptsatz
• Sequenzenkalkül