Sémantique des modèles stables
La sémantique des modèles stables est une sémantique déclarative en programmation logique utilisant la négation par l'échec. C'est l'une des nombreuses approches standard pour la signification de la négation dans la programmation logique, au côté de la terminaison de programme et de la sémantique bien fondée. La sémantique du modèle stable est à la base du langage de programmation déclarative Answer Set Programming (ASP). Les recherches sur la sémantique déclarative de la négation en programmation logique ont été motivées par une divergence possible entre le comportement de la résolution SLDNF (la généralisation de la résolution SLD utilisée par Prolog en présence de négation dans les corps de règle) et les tables de vérité familières de la logique propositionnelle classique. Considérons, par exemple, le programme Dans ce programme, la requête p réussira par la premi̠ère règle. La requête q échouera, car elle n'est jamais présente dans la tête d'une règle. La requête r échouera également, car la seule règle avec r dans la tête contient le sous-objectif q dans son corps ; et que ce sous-objectif échoue. Enfin, la requête s réussit, car chacun de ses sous-objectifs (p et ) réussit. En résumé, le comportement de la résolution SLDNF sur le programme donné peut être représenté par la table de vérité suivante : {| cellpadding=5 style="width:18em" |p |q |r
| s |
|---|
| T |
| F |
| F |
| T. |
| } |
| Cependant, nous pouvons aussi considérer les règles de ce programme comme des formules propositionnelles (en identifiant la virgule avec la conjonction , le symbole avec négation , et que l'on accepte de considérer comme l'implication écrite à l'envers). Par exemple, la dernière règle de ce programme donnerait, une fois ré-écrite comme une formule propositionnelle : |
| Nous pouvons alors vérifier que, pour l'affectation proposée ci-dessus, chacune des règles est bien vraie (au sens logique). Cette affectation est donc bien un modèle du programme. Mais ce programme a aussi d'autres modèles, par exemple : |
| { |
| p |
| q |
| r |
| s |
| - |
| T |
| T |
| T |
| F. |