Clause de Horn

Une clause Horn est une disjonction logique de littéraux, où au maximum un des littéraux est positif, et tous les autres sont négatifs. Elle porte le nom d'Alfred Horn qui les a décrites dans un article en 1951.

Une clause Horn avec exactement un littéral positif est une clause définie ; une clause définie sans littéraux négatifs est parfois appelée un "fait" ; et une clause Horn sans littéral positif est parfois appelée une clause de but. Ces trois types de clauses Horn sont illustrés dans l'exemple de proposition suivant :

Clause définitive : ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t\vee u} $\neg p\lor \neg q\vee \cdots \vee \neg t\vee u$

fait : u {\displaystyle u} $u$

clause de but : ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t {\displaystyle \neg p\lor \neg q\vee \cdots \vee \neg t} $\neg p\lor \neg q\vee \cdots \vee \neg t$

Dans le cas d'une clause non propositionnelle, toutes les variables d'une clause sont implicitement quantifiées de manière universelle, la portée de la clause étant entière. Ainsi, par exemple :

¬ human ( X ) ∨ mortal ( X ) {\displaystyle \neg {\text{human}}(X)\lor {\text{mortal}(X)} $\neg {\text{human}}(X)\lor {\text{mortal}}(X)$

représente :

∀ X ( ¬ humain ( X ) ∨ mortel ( X ) (X)) $\forall X(\neg {\text{human}}(X)\lor {\text{mortal}}(X))$

ce qui est logiquement équivalent à :

∀ X ( human ( X ) → mortal ( X ) . {\displaystyle \forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)). } $\forall X({\text{human}}(X)\rightarrow {\text{mortal}}(X)).$

Les clauses de corne jouent un rôle fondamental dans la logique constructive et la logique informatique. Elles sont importantes dans le théorème automatisé prouvant par résolution du premier ordre, parce que le résolvant de deux clauses Horn est lui-même une clause Horn, et le résolvant d'une clause de but et d'une clause définie est une clause de but. Ces propriétés des clauses de Horn peuvent conduire à une plus grande efficacité dans la preuve d'un théorème (représenté comme la négation d'une clause de but).

Les clauses de corne sont également la base de la programmation logique, où il est courant d'écrire des clauses définies sous forme d'implication :

( p ∧ q ∧ ⋯ ∧ t ) → u {\displaystyle (p\wedge q\wedge \cdots \wedge t)\rightarrow u $(p\wedge q\wedge \cdots \wedge t)\rightarrow u$

En fait, la résolution d'une clause de but avec une clause définie pour produire une nouvelle clause de but est la base de la règle d'inférence de résolution SLD, utilisée pour implémenter la programmation logique et le langage de programmation Prolog.

Dans la programmation logique, une clause définie se comporte comme une procédure de réduction des objectifs. Par exemple, la clause Horn écrite ci-dessus se comporte comme la procédure :

pour nous montrer u $u$ , p $p$ et q et ⋯ $\cdots$ et montrer t {\displaystyle t} $t$ .

Pour souligner cette utilisation à l'envers de la clause, celle-ci est souvent rédigée à l'envers :

u ← ( p ∧ q ∧ ⋯ ∧ t ) {\displaystyle u\leftarrow (p\land q\land \cdots \land t)} $u\leftarrow (p\land q\land \cdots \land t)$

Dans Prolog, cela s'écrit comme suit :

u :- p, q, ..., t.

La notation du Prologue est en fait ambiguë, et le terme "clause de but" est parfois aussi utilisé de manière ambiguë. Les variables d'une clause de but peuvent être lues comme étant quantifiées de manière universelle ou existentielle, et le fait de dériver "faux" peut être interprété soit comme une contradiction, soit comme une solution réussie du problème à résoudre.

Van Emden et Kowalski (1976) ont étudié les propriétés théoriques du modèle des clauses de Horn dans le contexte de la programmation logique, en montrant que chaque ensemble de clauses définies D a un modèle minimal unique M. Une formule atomique A est logiquement impliquée par D si et seulement si A est vrai dans M. Il s'ensuit qu'un problème P représenté par une conjonction de littéraux positifs quantifiée de manière existentielle est logiquement impliqué par D si et seulement si P est vrai dans M. La sémantique du modèle minimal des clauses de Horn est la base de la sémantique du modèle stable des programmes logiques.

Les clauses de Horn propositionnelles présentent également un intérêt pour la complexité des calculs, où le problème de trouver des assignations de valeurs de vérité pour rendre vraie une conjonction de clauses de Horn propositionnelles est un problème P-complet (en fait, résoluble en temps linéaire), parfois appelé HORNSAT. (Le problème de satisfiabilité booléenne sans restriction est cependant un problème NP-complet). La satisfaisabilité des clauses Horn de premier ordre est indécidable.

Questions et réponses

Q : Qu'est-ce qu'une clause de Horn ?

R : Une clause Horn est une disjonction logique de littéraux, où au plus un des littéraux est positif et tous les autres sont négatifs.

Q : Qui les a décrites pour la première fois ?

R : Alfred Horn les a décrites pour la première fois dans un article en 1951.

Q : Qu'est-ce qu'une clause définie ?

R : Une clause de Horn comportant exactement un littéral positif est appelée clause définie.

Q : Qu'est-ce qu'un fait ?

R : Une clause définie ne comportant aucun littéral négatif est parfois appelée un "fait".

Q : Qu'est-ce qu'une clause de but ?

R : Une clause cornée sans littéral positif est parfois appelée clause de but.

Q : Comment fonctionnent les variables dans les cas non propositionnels ?

R : Dans le cas non propositionnel, toutes les variables d'une clause sont implicitement quantifiées universellement avec une portée de la clause entière. Cela signifie qu'elles s'appliquent à chaque partie de la déclaration.

Q : Quel rôle jouent les clauses de Horn en logique constructive et en logique computationnelle ? R : Les clauses de Horn jouent un rôle important dans la preuve automatisée de théorèmes par résolution du premier ordre, car le résolvant de deux clauses de Horn ou entre une clause de but et une clause définie peut être utilisé pour créer de plus grandes efficacités lors de la preuve de quelque chose représenté comme la négation de sa clause de but. Elles sont également utilisées comme base pour les langages de programmation logique tels que Prolog, où elles se comportent comme des procédures de réduction de but.