Horn-Formel - LinkFang.de





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 Mathematiker Alfred Horn.

Definition

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

[math]\phi_1 \vee \phi_2 \vee \ldots \vee \phi_n[/math]

von Literalen [math]\phi_i[/math], wobei jedes entweder ein atomarer Ausdruck (ein positives Literal) oder die Negation eines solchen (ein negatives Literal) ist.

Eine Horn-Klausel ist eine Klausel mit höchstens einem positiven Literal, d. h. mit höchstens einem Literal, das keine Negation ist.

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

[math]\neg p \or \neg q \vee \ldots \vee \neg t \vee u[/math]

In diesem Fall sind bis auf [math]u[/math] alle atomaren Ausdrücke (in diesem Beispiel sind es Aussagenvariablen) Negationen.

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

Beispiele:

  • [math](\neg p \vee \neg q \vee r) \wedge (p \vee \neg q \vee \neg s) \wedge (\neg r \vee \neg s)[/math]
    Die dritte Horn-Klausel hat kein, die beiden anderen Horn-Klauseln haben je ein positives Literal.
  • [math](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)[/math]

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:

[math]\neg \phi \vee \psi = \phi \Rightarrow \psi[/math]

Gemäß Definition kann eine Horn-Klausel genau ein oder gar kein positives Literal (also höchstens einen atomaren Ausdruck) enthalten. Außerdem kann es vorkommen, dass es unter den Literalen gar keine Negationen gibt. Es gibt daher 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
Mindestens ein negatives Literal
[math]\neg x_1 \vee \ldots \vee \neg x_n[/math] [math]x_1 \wedge \ldots \wedge x_n \Rightarrow 0[/math] [math]x_1, \ldots, x_n[/math] sind nicht alle wahr
Definite Hornklausel Genau ein positives Literal
Mindestens ein negatives Literal
[math]\neg x_1 \vee \ldots \vee \neg x_n \vee y[/math] [math]x_1 \wedge \ldots \wedge x_n \Rightarrow y[/math] Wenn [math]x_1, \ldots, x_n[/math] wahr sind, dann ist auch [math]y[/math] wahr
Faktenklausel Genau ein positives Literal
Kein negatives Literal
[math]y\!\;[/math] [math]1 \Rightarrow y[/math] [math]y\!\;[/math] 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.

Siehe auch

Literatur

  • H. D. Ebbinghaus, J. Flum, W. Thomas: Einführung in die mathematische Logik. BI-Wiss. Verlag, Mannheim/Leipzig/Wien/Zürich 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.
  • Hans-Peter Tuschik, Helmut Wolter: Mathematische Logik – kurzgefasst. Grundlagen, Modelltheorie, Entscheidbarkeit, Mengenlehre. BI-Wiss. Verlag, Mannheim/Leipzig/Wien/Zürich 1994, ISBN 3-411-16731-9.

Kategorien: Mathematische Logik

Quelle: Wikipedia - http://de.wikipedia.org/wiki/Horn-Formel (Vollständige Liste der Autoren des Textes [Versionsgeschichte])    Lizenz: CC-by-sa-3.0

Änderungen: Alle Bilder mit den meisten Bildunterschriften wurden entfernt. Ebenso alle zu nicht-existierenden Artikeln/Kategorien gehenden internen Wikipedia-Links (Bsp. Portal-Links, Redlinks, Bearbeiten-Links). Entfernung von Navigationsframes, Geo & Normdaten, Mediadateien, gesprochene Versionen, z.T. ID&Class-Namen, Style von Div-Containern, Metadaten, Vorlagen, wie lesenwerte Artikel. Ansonsten sind keine Inhaltsänderungen vorgenommen worden. Weiterhin kann es durch die maschinelle Bearbeitung des Inhalts zu Fehlern gerade in der Darstellung kommen. Darum würden wir jeden Besucher unserer Seite darum bitten uns diese Fehler über den Support mittels einer Nachricht mit Link zu melden. Vielen Dank!

Stand der Informationen: August 201& - Wichtiger Hinweis: Da die Inhalte maschinell von Wikipedia übernommen wurden, ist eine manuelle Überprüfung nicht möglich. Somit garantiert LinkFang.de nicht die Richtigkeit und Aktualität der übernommenen Inhalte. Sollten die Informationen mittlerweile fehlerhaft sein, bitten wir Sie darum uns per Support oder E-Mail zu kontaktieren. Wir werden uns dann innerhalb von spätestens 10 Tagen um Ihr Anliegen kümmern. Auch ohne Anliegen erfolgt mindestens alle drei Monate ein Update der gesamten Inhalte.