Clause de Horn
En logique, et en particulier en calcul propositionnel, une clause de Horn est une proposition du type :
- (p ET q ET ... ET t) IMPLIQUE u,
où le nombre de propositions combinées par le connecteur logique ET est aussi élevé que désiré.
Ces dernières jouent un rôle fondamentale, par exemple, dans la programmation logique. Le critère de ce choix vient du fait qu'en logique classique il est possible de réecrire un clause sous la forme :
- (NON p) OU (NON q) OU ... OU (NON t) OU u.
Il est possible de trouver cette définition dans des ouvrages relatif à la logique, bien que cette notation soit inapropriée pour exprimer son intérêt en logique constructiste. Cependant, elle démontre que les clauses de Horn forment un sous-ensemble des formes normales conjonctives dans lesquelles un seul un terme et positif.
L'intérêt des clauses de Horn dans la preuve de théorème par calcul de prédicat du premier ordre est que l'on peut réduire deux clauses de Horn à une clause de Horn. En preuve automatique des théorèmes, on peut atteindre une très grande efficacité en representant les prédicats sous forme de clause.
En fait, le langage de programmation Prolog est entièrement basé sur des clauses de Horn.
La dénomination « clause de Horn » vient de nom du logicien Alfred Horn, qui le premier mis en évidence l'intérêt de telles clauses en 1951, dans l'article « On sentences which are true of direct unions of algebras » du Journal of Symbolic Logic, 16, 14-21.
Cet article est basé sur du matériel provenant d'une traduction de la Free On-line Dictionary of Computing et est utilisé avec permission selon la GFDL.