2. Littéraux, clauses et clauses de Horn
Un atome applique un prédicat à des termes : chat(leo), p(x), alimentation(carnivore,viande). Les termes peuvent comprendre des constantes, des variables et, lorsque le vocabulaire le permet, des fonctions comme f(x).
Un littéral est un atome positif ou sa négation. chat(leo) est positif; ¬pomme(fuji) est négatif. La négation porte sur l’atome entier, pas sur un argument.
Une clause est une disjonction de littéraux :
Code (text) · sélectionner pour copier
alimentation(x,viande) ∨ ¬sorte_de(x,carnivore)
p(x,y) ∨ ¬q(x) ∨ t(y)
Une clause peut contenir un seul littéral : c’est une clause unitaire. À l’intérieur d’une clause, les seuls connecteurs affichés sont OU et NÉGATION. Les implications, équivalences, conjonctions et quantificateurs doivent avoir été traités par la conversion.
Une base est un ensemble de clauses, interprété comme leur conjonction :
Code (text) · sélectionner pour copier
{ A ∨ B, C } signifie (A ∨ B) ∧ C.
La virgule qui sépare deux clauses n’est donc pas un OU supplémentaire. Cette différence explique pourquoi une phrase contenant ET peut produire deux clauses, alors qu’une phrase contenant OU reste souvent une seule clause.
Les variables sont universellement quantifiées de façon implicite dans chaque clause. Elles sont locales à cette clause. Deux clauses différentes utilisant le même nom x ne désignent pas automatiquement une variable commune; il est utile de les renommer avant une résolution.
Une clause de Horn possède au plus un littéral positif, donc zéro ou un :
| Clause | Positifs | Rôle dans les exemples |
|---|---|---|
p(x,y) |
1 | Fait positif unitaire |
p(x) ∨ ¬q(x) ∨ ¬r(x) |
1 | Règle : q et r permettent p |
¬q(x) |
0 | But négatif dans la preuve |
p(x) ∨ q(x) |
2 | Clause non Horn |
La résolution générale accepte aussi des clauses non Horn. La restriction Horn est celle du fragment de programmation présenté : faits ou règles avec une seule tête positive, et buts à résoudre. Il ne faut pas déclarer une clause non Horn « invalide » en logique simplement parce qu’elle ne correspond pas à ce fragment Prolog.
La clause vide, notée □ ici et {} dans le cours, ne contient aucun littéral. La disjonction vide est fausse : cette clause représente une contradiction. Elle diffère d’un ensemble vide de clauses, dont la conjonction serait vraie.