Eine prädikatenlogische Theorie, deren Axiome Horn-Sätze sind: universelle Formeln, die eine Konjunktion atomarer Formeln in eine einzelne atomare Formel (gegebenenfalls Falschheit) implizieren.

Prinzip

Die Beschränkung auf Horn-Klauseln erhält bestimmte Abschluss-Eigenschaften (Produkte, Teilstrukturen, homomorphe Bilder unter Bedingungen) und liefert einen Teilbereich der Prädikatenlogik, der sich für konstruktive Modellbildung und algorithmisches Schließen eignet.

Demonstration

Die Klasse aller Graphen, die eine Menge von Horn-Axiomen erfüllen, die besagen, dass bestimmte Adjazenzmuster das Vorhandensein eines Nachbarn implizieren, ist eine Horn-Theorie: jedes Axiom hat die Form Für alle x,y,... (E(x,y) ∧ ... → E(z,w)).

Fehlanwendung

Jede universelle Implikation mit Disjunktionen im Konsequent oder mehreren positiven Atomen fälschlich als Horn-Axiom zu behandeln; dies bricht horn-spezifische Abschlussresultate und kann algorithmische Garantien zunichte machen.

Konsequenz

Modelle einer Horn-Theorie sind unter gerichteten Kolimiten und gewissen Produkten abgeschlossen, sodass man freie oder kleinste Modelle durch syntaktische oder iterative Abschlußverfahren konstruieren kann; rechnerisch besitzen Horn-Fragmente oft effiziente Entscheidungsverfahren.

Umkehrung

Das Gegenteil ist eine beliebige prädikatenlogische Theorie mit allgemeinen Formeln (z. B. Disjunktionen oder Existenzaussagen in nicht-Horn-Positionen), die die konstruktiven Abschlusseigenschaften nicht hat und anderes modelltheoretisches Verhalten zeigt.

Abgrenzung

Gilt nur für prädikatenlogische Axiome, die als universelle Horn-Sätze formuliert werden können; schließt Axiome mit Disjunktionen im Konsequent, nicht eliminierbare Existenzquantoren oder höherstufige Aussagen aus.

Semantische Spannung

Horn-Theorie steht im Spannungsfeld zur äquationalen Theorie: beide sind universelle Fragmente, aber äquationale Theorien verlangen atomare Gleichheiten, während Horn-Theorien beliebige atomare Prädikate in Antezedens und Konsequent zulassen, mit unterschiedlichen Konsequenzen für Ausdrucksstärke und Abschlusseigenschaften.

Synthese

Eine Horn-Theorie ist eine prädikatenlogische Theorie, die durch universelle Implikationen zwischen Konjunktionen atomarer Formeln und einer atomaren Konklusion axiomatisiert ist; die organisierende Idee ist, dass diese syntaktische Einschränkung stabile algebraische und rechnerische Eigenschaften für Modelle liefert.