Une théorie du premier ordre dont les axiomes sont des phrases de Horn : des formules universelles formées d'une implication d'une conjonction d'atomes vers un seul atome (éventuellement la fausseté).

Principe

La restriction aux clauses de Horn préserve certaines propriétés de fermeture (produits, sous-structures, images homomorphes sous conditions) et définit un fragment du premier ordre adapté à la construction de modèles et au raisonnement algorithmique.

Démonstration

La classe de graphes satisfaisant un ensemble d'énoncés de Horn affirmant que certains motifs d'adjacence impliquent l'existence d'un voisin constitue une théorie de Horn : chaque axiome a la forme PourTous x,y,... (E(x,y) ∧ ... → E(z,w)).

Mauvaise application

Considérer comme axiome de Horn une implication universelle contenant des disjonctions dans le conséquent ou plusieurs atomes positifs ; cela viole les résultats de fermeture spécifiques aux Horn et peut compromettre des garanties algorithmiques.

Conséquence

Les modèles d'une théorie de Horn sont stables par colimites dirigées et certains produits, ce qui permet de construire des modèles libres ou minimaux par procédures syntaxiques ou de clôture itérative ; du point de vue computationnel, les fragments de Horn admettent souvent des procédures efficaces.

Inversion

L'inverse est une théorie du premier ordre arbitraire contenant des formules générales (par exemple des disjonctions ou des existentielles en positions non-Horn), qui manque des propriétés constructives de fermeture et présente un comportement model-théorique différent.

Limite

Ne concerne que les axiomes du premier ordre réductibles en phrases universelles de Horn ; exclut les axiomes nécessitant des disjonctions dans le conséquent, des quantificateurs existentiels non éliminables par skolemisation et les énoncés d'ordre supérieur.

Tension sémantique

La théorie de Horn est en tension avec la théorie équationnelle (théorie universelle équationnelle) : les deux sont des fragments universels mais la théorie équationnelle impose des égalités atomiques tandis que la théorie de Horn permet des prédicats atomiques quelconques, entraînant des compromis d'expressivité et de fermeture distincts.

Synthèse

Une Théorie De Horn est une théorie du premier ordre axiomatisée par des implications universelles entre conjonctions d'atomes et une conclusion atomique ; l'idée directrice est que cette restriction syntaxique confère des propriétés algébriques et computationnelles robustes pour la construction et l'analyse de modèles.