Clause de Horn

Un article de Wikipédia, l'encyclopédie libre.

Pour les articles homonymes, voir 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.

[modifier] Définition

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}$ . Les clauses de Horn forment un sous–ensemble des formes normales disjonctives dans lesquelles un seul terme est positif.

[modifier] Interprétation intuitive

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

Les clauses de Horn strictes $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 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 \empty$ . La clause $\lnot q$ est une clause de Horn négative qui modélise bien le but à atteindre.

[modifier] Applications en programmation logique

Quel est le domaine d’application des clauses de Horn ?

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 de classe $\mathcal{P}$ . Les classes de Horn jouent donc un rôle fondamental dans la programmation logique^[1].

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^[2].

[modifier] Bibliographie

R. Cori et D. Lascar, Logique mathématique, Dunod, 2003, ISBN 210005452X
J.-M. Alliot, T. Schiex, P.Brisset et F. Garcia, Intelligence artificielle & informatique théorique, Cépaduès, 2002, ISBN 2854285786

[modifier] Notes

↑ Il serait intéressant d’ajouter des liens vers des papiers, articles ou implémentations de HORN–SAT. On pourra se rapporter à la version anglaise de l'article HORN–SAT.
↑ Cette partie mérite aussi d’être complétée.