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).
Motivation 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 réussira par la premi̠ère règle. La requête échouera, car elle n'est jamais présente dans la tête d'une règle. La requête échouera également, car la seule règle avec dans la tête contient le sous-objectif dans son corps ; et que ce sous-objectif échoue. Enfin, la requête réussit, car chacun de ses sous-objectifs ( 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"
|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 :
{| cellpadding=5 style="width:18em"
|T |T |T |F.
L'un des modèles du programme donné est donc particulier, dans le sens où il représente correctement le comportement de la résolution SLDNF. Quelles sont les propriétés mathématiques de ce modèle qui le rendent spécial ? C'est pour répondre à cette question qu'a été défini la notion de modèle stable.
Lien avec la logique non monotone Le sens à donner à la négation dans les programmes logiques est lié à deux théories du raisonnement non monotone (à savoir la logique autoépistémique et la logique par défaut). La découverte de ces relations fut une étape clé pour le développement de la sémantique des modèles stables.
Dans la logique autoépistémique on utilise un opérateur modal afin de distinguer entre ce qui est vrai et ce que l'on croit. Michael Gelfond a proposé de lire dans le corps d'une règle comme , et de comprendre une règle avec négation comme la formule correspondante de la logique autoépistémique. Dans sa forme initiale, la sémantique du modèle stable peut être considérée comme une reformulation de cette idée en évitant les références explicites à cette logique.
Dans la logique par défaut, une position par défaut est similaire à une règle d'inférence, sauf qu'elle inclut, en plus de ses prémisses et sa conclusion, une liste de formules appelées justifications. Une position par défaut peut être utilisée pour tirer sa conclusion si ses justifications sont cohérentes avec ce que l'on croit actuellement. Concrètement, cela consiste à ajouter à la règle une série d'hypothèses qu'il faudra vérifier être vraie par la suite.
Nicole Bidoit et Christine Froidevaux ont proposé de traiter les atomes niés dans les corps de règles comme des justifications. Par exemple, la règle
peut être comprise comme la proposition par défaut qui nous permet de dériver de en supposant que est vrai (ce qu'il faudra vérifier en fin de programme). Là encore et bien qu'il n'y fasse pas explicitement référence, la sémantique des modèles stables utilise une idée similaire.
Modèles stables La définition d'un modèle stable ci-dessous (tirée de [Gelfond et Lifschitz, 1988]) utilise deux conventions.
Premièrement, une affectation de vérité est identifiée avec l'ensemble d'atomes qui obtiennent la valeur T . Par exemple, la table de vérité : {| cellpadding=5 style="width:18em"
|T |F |F |T. |} est identifiée à l'ensemble . Cette convention nous permet d'utiliser la relation d'inclusion des ensembles pour comparer les affectations de vérité les unes avec les autres. La plus petite de toutes les affectations de vérité est celle pour laquelle chaque atome est faux ; la plus grande affectation de vérité est celle où chaque atome est vrai.
Deuxièmement, un programme logique avec des variables est vu comme décrivant l'ensemble de toutes les instances closes de ses règles. C'est-à-dire qu'il décrit la substitution dans les règles du programme des variables par tous les termes clos possibles. Prenons pour exemple, la définition des nombres pairs par le programme logique suivant :
Il faut comprendre ceci comme le résultat du remplacement de dans ce programme par tous les termes clos possibles :
Le résultat en est donc le programme clos infini
Définition Soit un ensemble de règles de la forme
où sont des termes clos. Si ne contient pas de négation ( dans chaque règle du programme) alors, on peut montrer qu'il a exactement un modèle minimal (au sens de l'inclusion des ensembles) obtenu par propagation des clauses unitaires, ceci permet de définir le modèle stable de .
Pour étendre cette définition au cas des programmes avec négation, nous avons besoin du concept auxiliaire de réduction, que l'on définit comme suit.
Pour tout ensemble d'atomes clos, la réduction du programme par rapport à est l'ensemble des règles sans négation obtenu à partir de en supprimant d'abord chaque règle pour laquelle au moins un des atomes dans son corps
appartient à . Puis en supprimant les parties dans le corps de toutes les règles restantes.
On dit alors que est un modèle stable de si est le modèle stable du programme obtenu en réduisant par rapport à . Par construction ne contient pas de négation et son modèle stable est donc bien défini. Comme le suggère le terme « modèle stable », tout modèle stable de est un modèle de .
Exemple Pour illustrer ces définitions, vérifions que est un modèle stable du programme suivant :
La réduction de ce programme par rapport à est
(En effet, puisque , la réduction est obtenue en supprimant la partie négative de la dernière règle.) Comme l'ensemble satisfait toutes les règles de la réduction (et aucun de ses sous-ensembles n'a cette propriété), le modèle stable de la réduction est donc . Ainsi, comme la réduction de notre programme par aboutit à ce même ensemble, cet ensemble est bien un modèle stable.
On peut alors vérifier de la même manière que les 15 autres ensembles constitués des atomes ne sont pas eux-mêmes des modèles stables. Par exemple, la réduction du programme par rapport à est
Le modèle stable de cette réduction est ce qui est différent de l'ensemble utilisé pour la réduction.
Programmes sans modèle stable unique Un programme avec négation peut avoir plusieurs modèles stables ou bien aucun modèle stable. Par exemple, le programme
a deux modèles stables , . Tandis que le programme constitué d'une seule règle
n'a pas de modèles stables.
Si nous considérons la sémantique du modèle stable comme une description du comportement de Prolog en présence de négation, alors les programmes qui n'ont pas un modèle stable unique peuvent être jugés non satisfaisants dans le sens où ils ne fournissent pas une spécification sans ambiguïté pour la réponse aux requêtes de style Prolog. Ainsi, les deux programmes ci-dessus ne forment pas des programmes Prolog raisonnables puisque leur résolution du SLDNF ne termine pas.
Mais l'utilisation des modèles stables dans ASP offre une perspective différente sur de tels programmes. Dans ce paradigme de programmation, un problème de recherche donné est représenté par un programme logique de sorte que les modèles stables du programme correspondent aux solutions. Dans ce cadre, les programmes ayant plusieurs modèles stables correspondent à des problèmes avec plusieurs solutions, tandis que les programmes sans modèles stables sont des problèmes insolubles. Par exemple, le problème des huit reines a 92 solutions ; pour le résoudre à l'aide d'un programme ASP, nous l'encodons par un programme logique ayant 92 modèles stables. De ce point de vue, les programmes logiques avec exactement un modèle stable sont des cas assez spéciaux dans ASP, comme peuvent l'être en algèbre, les polynômes avec une seule racine.
Propriétés de la sémantique du modèle stable Dans cette section, tout comme pour la définition d'un modèle stable ci-dessus, nous entendons par programme logique, un ensemble de règles de la forme
où sont des atomes clos.
Atomes de tête Si un atome appartient à un modèle stable d'un programme logique alors est la tête d'une des règles de .
Minimalité Tout modèle stable d'un programme logique doit être minimal (au sens de l'inclusion des ensembles) parmi les modèles de .
La propriété antichaîne Si et sont des modèles stables du même programme logique, alors n'est pas un sous-ensemble propre de (par minimalité). En d'autres termes, l'ensemble des modèles stables d'un programme est une antichaîne.
NP-complétude Déterminer si un programme de logique clos fini a un modèle stable est NP-complet.
Relation avec d'autres théories de la négation par l'échec
Achèvement du programme Tout modèle stable d'un programme clos fini est non seulement un modèle du programme lui-même, mais aussi un modèle de son achèvement [Marek et Subrahmanian, 1989]. Cependant, l'inverse n'est pas vrai. Par exemple, l'achèvement du programme constitué de l'unique règle :
est la tautologie . Le modèle de cette tautologie est un modèle stable de , mais son autre modèle n'en est pas un. Comme l'a prouvé François Fages , il existe une condition syntaxique sur les programmes logiques permettant de se prémunir contre de tels contre-exemples et qui garantit ainsi la stabilité de chaque modèle d'achèvement du programme. De tels programmes sont dits serrés.
Fangzhen Lin et Yuting Zhao ont montré comment renforcer l'achèvement d'un programme non serré, en y ajoutant des formules dites "de boucles", afin d'éliminer tous ses modèles instables.
Sémantiques bien fondées Dans la sémantique bien fondée, les atomes clos d'un programme logique sont répartis en trois ensembles : vrai, faux et inconnu. Si un atome est vrai dans le modèle bien fondé de , alors il est vrai dans tous les modèles stables de . Encore une fois, l'inverse n'est pas vrai en général. Par exemple, le programme
a deux modèles stables, et . Bien que soit vrai dans ces deux modèles, sa valeur dans le modèle bien fondé est inconnue.
De plus, si un atome est faux dans le modèle bien fondé d'un programme alors il est faux pour tous ses modèles stables. Ainsi, le modèle bien fondé d'un programme logique fournit-il une borne inférieure sur l'intersection de ses modèles stables et une borne supérieure sur leur union.
Négation forte
Représentation d'informations incomplètes Du point de vue de la représentation des connaissances, un ensemble d'atomes clos peut être considéré comme la description d'un état des connaissances : les atomes qui appartiennent à l'ensemble sont connus pour être vrais, et les atomes qui n'appartiennent pas à l'ensemble sont connus pour être faux. Un état de connaissance éventuellement incomplet peut cependant être décrit à l'aide d'un ensemble cohérent mais éventuellement incomplet de littéraux (c'est-à-dire de l'ensemble des atomes clos et de leurs négations) ; si ni un atome ni sa négation n'appartiennent à l'ensemble alors on ne sait pas si est vrai ou faux.