Clause de Horn

La dénomination « clause de Horn » vient du nom du logicien Alfred Horn qui, le premier, met en évidence l’intérêt de telles clauses en 1951 dans l’article « On sentences which are true of direct unions of algebras » publié dans le Journal of Symbolic Logic, numéro 16, pages 14 à 21.

Que peut–on représenter avec des clauses de Horn ?

• Les clauses de Horn strictes énonçant ${\displaystyle q\lor \lnot p_{1}\lor \ldots \lor \lnot p_{n}}$ sont équivalentes à ${\displaystyle \{p_{1}{\text{,}}\ldots {\text{,}}p_{n}\}\models q}$.
  Intuitivement, elles représentent des règles « si ... alors ... » et permettent de déduire de nouveaux faits à partir de faits existants ;
• Les clauses de Horn positives sont appelées faits. Il s’agit en effet de variables propositionnelles qui représentent intuitivement des propositions élémentaires qui sont soit vraies soit fausses. Par exemple, « L'épice est une drogue » est un fait ;
• Les clauses de Horn négatives représentent des buts à atteindre, i.e. des questions. En effet, si l’on veut prouver ${\displaystyle \{H_{1}{\text{,}}\ldots {\text{,}}H_{n}\}\models q}$, alors q est le but de la résolution. Or on peut se ramener, via le principe de déduction en appliquant une technique d’inconsistance, à ${\displaystyle \{H_{1}{\text{,}}\ldots {\text{,}}H_{n}{\text{,}}\lnot q\}\models \emptyset }$. La clause ${\displaystyle \lnot q}$ est une clause de Horn négative qui modélise bien le but à atteindre.

Les formes normales composées de clauses de Horn sont un cas particulier de formes normales pour lesquelles on connait des méthodes de résolution efficaces. En effet le problème de la satisfiabilité d’un ensemble de clauses de Horn — aussi appelé HORN–SAT — est dans la classe P et complet pour cette classe. Les clauses de Horn jouent donc un rôle fondamental en programmation logique.

Les formules logiques que le langage de programmation Prolog peut utiliser sont des clauses de Horn, autrement dit Prolog est entièrement basé sur des clauses de Horn. Les éléments évoqués ci–dessus ne permettent d’utiliser que des variables propositionnelles et non des prédicats. Or Prolog opère en logique du premier ordre. Il est donc nécessaire d’étendre ces résultats au calcul des prédicats.

Un autre intérêt des clauses de Horn dans la preuve de théorème par calcul des prédicats 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 représentant les prédicats sous forme de clause.

• problème 2-SAT, problème algorithmique associé à un autre type de clauses, lui aussi polynomial

• René Cori et Daniel Lascar, Logique mathématique I. Calcul propositionnel, algèbres de Boole, calcul des prédicats [détail des éditions]
• Michel de Rougemont et Richard Lassaigne, Logique et fondements de l'informatique (logique du premier ordre, calculabilité et lambda calcul), Chapitre 2 : Systèmes de déduction, Hermes Science Publications, 1997. (ISBN 2-86601-380-8)
• J.-M. Alliot, T. Schiex, P.Brisset et F. Garcia, Intelligence artificielle & informatique théorique, Cépaduès, 2002, (ISBN 2-85428-578-6)
• Fred Galvin, « Horn Sentences », Annals of Mathematical Logic, vol. 1, n^o 4,‎ 1970, p. 389-422 (lire en ligne)