HornKlauseln

HornKlauseln sind eine Klasse von Klauseln in der Aussagen- und Prädikatenlogik, bei der in jeder Klausel höchstens eine positive Literal vorkommt. Formal lassen sie sich als Implikationen der Form (A1 ∧ ... ∧ An) → B darstellen, wobei B ein Atom ist. Enthält die Klausel kein positives Literal, entspricht sie (A1 ∧ ... ∧ An) → ⊥ und dient als Integritätsbedingung. Allgemein lassen sich Hornklauseln als disjunktionen mit maximal einem positiven Literal interpretieren.

In der Logikprogrammierung spielen Hornklauseln eine zentrale Rolle. Ein Fakt ist eine Hornklausel mit genau einem positiven Literal und leerem Körper (z. B. p). Eine Regel hat Form Kopf ← Körper, also eine Konjunktion von Prädikaten im Körper, deren Schluss das Kopfatom ist (z. B. r ← p, q). Anfragen (Ziele) entsprechen Klauseln mit leerem Kopf. In Prolog-Ausdrücken entspricht r :- p, q einer Regel, und eine Abfrage ?- r ruft dieses System zur Inferenz auf.

Eigenschaften und Bedeutung. Hornklauseln ermöglichen eine polynomielle Entscheidbarkeit in der Erfüllbarkeit und effiziente Inferenz durch Vorwärtsverkettung (Forward Chaining). Die Semantik wird oft über das kleinste Herbrand-Modell beschrieben; aus diesem Modell lassen sich Ziele ableiten. Wegen ihrer Struktur eignen sich Hornklauseln gut für automatische Theorembeweise, logische Programmierung, Wissensrepresentation und relationale Datenbanken (Datalog basiert auf Hornklauseln).

Verwandte Konzepte. Hornklauseln sind eine Teilmenge der Horn-Formeln und umfassen Definite Clauses (genauer: Klauseln mit exakt einem positiven Literal). Sie bilden eine Brücke zwischen formaler Logik und praktischer Inferenztechnik.