imported>Texvc2LaTeXBot: Texvc Makros durch LaTeX Pendant ersetzt gemäß mw:Extension:Math/Roadmap

2018-07-25T11:08:49Z

Texvc Makros durch LaTeX Pendant ersetzt gemäß mw:Extension:Math/Roadmap

Neue Seite

'''Horn-Formeln''' sind eine wichtige Art [[Prädikatenlogik|prädikatenlogischer]] Formeln. Sie spielen eine zentrale Rolle in der [[Logische Programmierung|logischen Programmierung]] und sind von Bedeutung für die konstruktive Logik. Benannt wurden sie nach dem US-amerikanischen Mathematiker [[Alfred Horn (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 [[Literal]]en <math>\phi_i</math>, wobei jedes entweder ein [[Atomare Aussage|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 \lor \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 [[Implikation]]en 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.

{| class="wikitable"
|-
! 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ändigkeit|P-vollständig]]). Man kann also in Polynomialzeit feststellen, ob eine [[Belegung (Logik)|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 [[Maschinelles Schließen|maschinellen Schließen]]. So werden in der [[Programmiersprache]] [[Prolog (Programmiersprache)|Prolog]] [[Computerprogramm|Programme]] als Horn-Klauseln angegeben.

== Siehe auch ==
* [[Gentzenscher Hauptsatz]]
* [[Sequenzenkalkül]]

== 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.
* {{Literatur
|Autor=[[Wolfgang Rautenberg]]
|Titel=Einführung in die Mathematische Logik
|Auflage=3.
|Verlag=Vieweg+Teubner
|Ort=Wiesbaden
|Jahr=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.

[[Kategorie:Mathematische Logik]]

Horn-Formel - Versionsgeschichte

imported>Texvc2LaTeXBot: Texvc Makros durch LaTeX Pendant ersetzt gemäß mw:Extension:Math/Roadmap