www.wikidata.de-de.nina.az

Horn Formel n sind eine wichtige Art prädikatenlogischer Formeln Sie spielen eine zentrale Rolle in der logischen Progra

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 Bearbeiten

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

von Literalen , 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:

In diesem Fall sind bis auf 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:

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:

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 		sind nicht alle wahr
Definite Hornklausel Genau ein positives Literal
Mindestens ein negatives Literal 		Wenn wahr sind, dann ist auch wahr
Faktenklausel Genau ein positives Literal
Kein negatives Literal 		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.

Siehe auch Bearbeiten

Literatur Bearbeiten

  • 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.
wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele
Veröffentlichungsdatum:
Horn Formeln sind eine wichtige Art pradikatenlogischer Formeln Sie spielen eine zentrale Rolle in der logischen Programmierung und sind von Bedeutung fur die konstruktive Logik Benannt wurden sie nach dem US amerikanischen Mathematiker Alfred Horn Inhaltsverzeichnis 1 Definition 2 Darstellungsformen von Horn Klauseln 3 Erfullbarkeit 4 Anwendung 5 Siehe auch 6 LiteraturDefinition BearbeitenUnter einer Klausel auch Disjunktionsterm genannt versteht man die Disjunktion ϕ 1 ϕ 2 ϕ n displaystyle phi 1 vee phi 2 vee ldots vee phi n nbsp von Literalen ϕ i displaystyle phi i nbsp 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 hochstens einem positiven Literal d h mit hochstens einem Literal das keine Negation ist Im Spezialfall der Aussagenlogik sieht eine typische Horn Klausel also so aus p q t u displaystyle neg p lor neg q vee ldots vee neg t vee u nbsp In diesem Fall sind bis auf u displaystyle u nbsp alle atomaren Ausdrucke in diesem Beispiel sind es Aussagenvariablen Negationen Eine Horn Formel ist eine konjunktive Normalform das heisst eine Konjunktion von Disjunktionen bei der jeder Disjunktionsterm eine Horn Klausel ist Beispiele p q r p q s r s displaystyle neg p vee neg q vee r wedge p vee neg q vee neg s wedge neg r vee neg s nbsp Die dritte Horn Klausel hat kein die beiden anderen Horn Klauseln haben je ein positives Literal x 1 x 2 x 3 x 1 x 2 x 3 x 4 displaystyle 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 nbsp Darstellungsformen von Horn Klauseln BearbeitenHorn 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 ϕ ps ϕ ps displaystyle neg phi vee psi phi Rightarrow psi nbsp Gemass Definition kann eine Horn Klausel genau ein oder gar kein positives Literal also hochstens einen atomaren Ausdruck enthalten Ausserdem 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 Uberblick uber diese drei moglichen Formen einer Horn Klausel sowohl als Disjunktion als auch als Implikation Name Beschreibung Disjunktion Implikation In WortenZielklausel Kein positives LiteralMindestens ein negatives Literal x 1 x n displaystyle neg x 1 vee ldots vee neg x n nbsp x 1 x n 0 displaystyle x 1 wedge ldots wedge x n Rightarrow 0 nbsp x 1 x n displaystyle x 1 ldots x n nbsp sind nicht alle wahrDefinite Hornklausel Genau ein positives LiteralMindestens ein negatives Literal x 1 x n y displaystyle neg x 1 vee ldots vee neg x n vee y nbsp x 1 x n y displaystyle x 1 wedge ldots wedge x n Rightarrow y nbsp Wenn x 1 x n displaystyle x 1 ldots x n nbsp wahr sind dann ist auch y displaystyle y nbsp wahrFaktenklausel Genau ein positives LiteralKein negatives Literal y displaystyle y nbsp 1 y displaystyle 1 Rightarrow y nbsp y displaystyle y nbsp ist wahrErfullbarkeit BearbeitenMit Hilfe des Markierungsalgorithmus konnen Horn Formeln in Polynomialzeit auf Erfullbarkeit getestet werden zudem ist HORNSAT P vollstandig Man kann also in Polynomialzeit feststellen ob eine Variablenbelegung eine Zuordnung von Wahrheitswerten zu den in der Horn Formel vorkommenden Literalen existiert fur welche die Horn Formel wahr wird Im Unterschied dazu wird vermutet dass allgemein fur aussagenlogische Formeln kein Polynomialzeit Algorithmus existiert siehe Erfullbarkeitsproblem der Aussagenlogik Anwendung BearbeitenDie Bedeutung der Horn Klauseln liegt in der Informatik beim maschinellen Schliessen So werden in der Programmiersprache Prolog Programme als Horn Klauseln angegeben Siehe auch BearbeitenGentzenscher Hauptsatz SequenzenkalkulLiteratur BearbeitenH D Ebbinghaus J Flum W Thomas Einfuhrung in die mathematische Logik BI Wiss Verlag Mannheim Leipzig Wien Zurich 1992 ISBN 3 411 15603 1 Wolfgang Rautenberg Einfuhrung 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 Zurich 1994 ISBN 3 411 16731 9 Abgerufen von https de wikipedia org w index php title Horn Formel amp oldid 179436793