Une clause Horn est une disjonction logique de littéraux, où au maximum un des littéraux est positif, et tous les autres sont négatifs. Elle porte le nom d'Alfred Horn qui les a décrites dans un article en 1951.
Une clause Horn avec exactement un littéral positif est une clause définie ; une clause définie sans littéraux négatifs est parfois appelée un "fait" ; et une clause Horn sans littéral positif est parfois appelée une clause de but. Ces trois types de clauses Horn sont illustrés dans l'exemple de proposition suivant :
Dans le cas d'une clause non propositionnelle, toutes les variables d'une clause sont implicitement quantifiées de manière universelle, la portée de la clause étant entière. Ainsi, par exemple :
représente :
ce qui est logiquement équivalent à :
Les clauses de corne jouent un rôle fondamental dans la logique constructive et la logique informatique. Elles sont importantes dans le théorème automatisé prouvant par résolution du premier ordre, parce que le résolvant de deux clauses Horn est lui-même une clause Horn, et le résolvant d'une clause de but et d'une clause définie est une clause de but. Ces propriétés des clauses de Horn peuvent conduire à une plus grande efficacité dans la preuve d'un théorème (représenté comme la négation d'une clause de but).
Les clauses de corne sont également la base de la programmation logique, où il est courant d'écrire des clauses définies sous forme d'implication :
En fait, la résolution d'une clause de but avec une clause définie pour produire une nouvelle clause de but est la base de la règle d'inférence de résolution SLD, utilisée pour implémenter la programmation logique et le langage de programmation Prolog.
Dans la programmation logique, une clause définie se comporte comme une procédure de réduction des objectifs. Par exemple, la clause Horn écrite ci-dessus se comporte comme la procédure :
Pour souligner cette utilisation à l'envers de la clause, celle-ci est souvent rédigée à l'envers :
Dans Prolog, cela s'écrit comme suit :
La notation du Prologue est en fait ambiguë, et le terme "clause de but" est parfois aussi utilisé de manière ambiguë. Les variables d'une clause de but peuvent être lues comme étant quantifiées de manière universelle ou existentielle, et le fait de dériver "faux" peut être interprété soit comme une contradiction, soit comme une solution réussie du problème à résoudre.
Van Emden et Kowalski (1976) ont étudié les propriétés du modèle théorique des clauses de Horn dans le contexte de la programmation logique, en montrant que chaque ensemble de clauses définies D a un modèle minimal unique M. Une formule atomique A est logiquement impliquée par D si et seulement si A est vrai dans M. Il s'ensuit qu'un problème P représenté par une conjonction de littéraux positifs quantifiée de manière existentielle est logiquement impliqué par D si et seulement si P est vrai dans M. La sémantique du modèle minimal des clauses de Horn est la base de la sémantique du modèle stable des programmes logiques.
Les clauses de Horn propositionnelles présentent également un intérêt pour la complexité des calculs, où le problème de trouver des assignations de valeurs de vérité pour rendre vraie une conjonction de clauses de Horn propositionnelles est un problème P-complet (en fait, résoluble en temps linéaire), parfois appelé HORNSAT. (Le problème de satisfiabilité booléenne sans restriction est cependant un problème NP-complet). La satisfaisabilité des clauses Horn de premier ordre est indécidable.