Hornklausel

Hornklausel

Horn-Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US-amerikanischen Logiker Alfred Horn.

Inhaltsverzeichnis

Definition mit Horn-Klauseln

Eine Horn-Klausel ist eine Klausel mit höchstens einem positiven Literal, d.h. höchstens einem Literal, in dem die Variable nicht negiert vorkommt. Eine Horn-Formel ist eine Konjunktive Normalform (das heißt eine Konjunktion von Disjunktionen), bei der jeder Disjunktionsterm eine Horn-Klausel ist, also eine Disjunktion von Literalen, von denen höchstens eines unverneint (positiv) auftritt.

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. Die folgende Tabelle gibt einen Überblick über die zwei möglichen Typen einer Horn-Klausel und ihre Form 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

Die Anzahl der negativen Literale (n) kann für Klauseln mit genau einem positiven Literal auch 0 sein (teilweise lässt man auch die leere Klausel als Zielklausel zu).

Erfüllbarkeit

Mit Hilfe des Markierungsalgorithmus können Horn-Formeln in Polynomialzeit auf Erfüllbarkeit getestet werden (folglich ist HORNSAT P-vollständig). Man kann also in Polynomialzeit feststellen, ob eine Variablenbelegung (eine Zuordnung von Wahrheitswerten zu den in in der Horn-Formel vorkommenden Literalen) existiert, für die 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 zum Beispiel in der Informatik beim maschinellen Schließen. So werden in der Programmiersprache Prolog Programme als Horn-Klauseln angegeben.

Siehe auch


Wikimedia Foundation.

Игры ⚽ Поможем написать курсовую

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Klausel-Normalform — Die Klauselform oder Klauselnormalform beschreibt in der Logik eine Formel in konjunktiver Normalform (KNF), bei der die Konjunktionen jeweils in Mengenschreibweise zusammengefasst wurden. Eine Formel in Klauselform (selten auch Klausenform) ist… …   Deutsch Wikipedia

  • Klauselform — Die Klauselform oder Klauselnormalform beschreibt in der Logik eine Formel in konjunktiver Normalform (KNF), bei der die Konjunktionen jeweils in Mengenschreibweise zusammengefasst wurden. Eine Formel in Klauselform (selten auch Klausenform) ist… …   Deutsch Wikipedia

  • Klauselnormalform — Die Klauselform oder Klauselnormalform beschreibt in der Logik eine Formel in konjunktiver Normalform (KNF), bei der die Konjunktionen jeweils in Mengenschreibweise zusammengefasst wurden. Eine Formel in Klauselform (selten auch Klausenform) ist… …   Deutsch Wikipedia

  • Horn-Formel — Horn Formeln sind eine wichtige Teilmenge der prädikatenlogischen 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… …   Deutsch Wikipedia

  • Horn-Klausel — Horn Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US amerikanischen Logiker Alfred Horn. Inhaltsverzeichnis 1 Definition mit Horn Klauseln 1.1 Beispiele 1.2 Darstellungsformen von Horn Klauseln… …   Deutsch Wikipedia

  • Horn-Klauseln — Horn Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US amerikanischen Logiker Alfred Horn. Inhaltsverzeichnis 1 Definition mit Horn Klauseln 1.1 Beispiele 1.2 Darstellungsformen von Horn Klauseln… …   Deutsch Wikipedia

  • Hornformel — Horn Formeln sind eine spezielle Teilmenge der aussagenlogischen Formeln. Benannt wurden sie nach dem US amerikanischen Logiker Alfred Horn. Inhaltsverzeichnis 1 Definition mit Horn Klauseln 1.1 Beispiele 1.2 Darstellungsformen von Horn Klauseln… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”