Clause de Horn

Pour les articles homonymes, voir 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 ${\displaystyle (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 ${\displaystyle (\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.