Clause de Horn

En logique, en particulier en calcul propositionnel, une clause de Horn est une clause comportant au plus un littéral positif.

Il existe donc trois types de clauses de Horn :

• celles qui comportent un littéral positif et au moins un littéral négatif, appelées clauses de Horn strictes ;
• celles qui comportent un littéral positif et aucun littéral négatif, appelées clauses de Horn positives ;
• celles qui ne comportent que des littéraux négatifs, appelées clauses de Horn négatives.

De plus toute clause de Horn est de la forme $(r_{1}\land r_{2}\land \ldots \land r_{n})\Rightarrow h{\text{, avec }}n\in \mathbb {N}$ (qui peut aussi s'écrire sous la forme $(\lnot r_{1}\lor \lnot r_{2}\lor \ldots \lor \lnot r_{n})\lor h{\text{, avec }}n\in \mathbb {N}$) . Les clauses de Horn forment un sous–ensemble des formes normales disjonctives dans lesquelles un seul terme est positif.

Historique

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.

Interprétation intuitive

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

• Les clauses de Horn strictes énonçant $q\lor \lnot p_{1}\lor \ldots \lor \lnot p_{n}$ sont équivalentes à $\{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 $\{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, à $\{H_{1}{\text{,}}\ldots {\text{,}}H_{n}{\text{,}}\lnot q\}\models \emptyset$. La clause $\lnot q$ est une clause de Horn négative qui modélise bien le but à atteindre.

Applications en programmation logique

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.

Articles connexes

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

Bibliographie

• 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)