Sémantique des modèles stables

Modèle:À wikifier

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

p

r \leftarrow p, q

s \leftarrow p, not q .

Dans ce programme, la requête Modèle:Mvar réussira par la premi̠ère règle. La requête Modèle:Mvar échouera, car elle n'est jamais présente dans la tête d'une règle. La requête Modèle:Mvar échouera également, car la seule règle avec Modèle:Mvar dans la tête contient le sous-objectif Modèle:Mvar dans son corps ; et que ce sous-objectif échoue. Enfin, la requête Modèle:Mvar réussit, car chacun de ses sous-objectifs (Modèle:Mvar et $not q$ ) 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 :

Modèle:Mvar	Modèle:Mvar	Modèle:Mvar	Modèle:Mvar
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 $\land$ , le symbole $not$ avec négation $\neg$ , et que l'on accepte de considérer $F \leftarrow G$ comme l'implication $G \to F$ écrite à l'envers). Par exemple, la dernière règle de ce programme donnerait, une fois ré-écrite comme une formule propositionnelle :

p \land \neg q \to s .

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 :

Modèle:Mvar	Modèle:Mvar	Modèle:Mvar	Modèle:Mvar
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 [1987] a proposé de lire $not p$ dans le corps d'une règle comme "je pense que $p$ est faux", 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 [1987] ont proposé de traiter les atomes niés dans les corps de règles comme des justifications. Par exemple, la règle

s \leftarrow p, not q

peut être comprise comme la proposition par défaut qui nous permet de dériver $s$ de $p$ en supposant que $\neg q$ 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é :

Modèle:Mvar	Modèle:Mvar	Modèle:Mvar	Modèle:Mvar
T	F	F	T.

est identifiée à l'ensemble ${p, s}$ . 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é $\emptyset$ 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 :

even (0)

even (s (X)) \leftarrow not even (X)

Il faut comprendre ceci comme le résultat du remplacement de Modèle:Mvar dans ce programme par tous les termes clos possibles :

0, s (0), s (s (0)), \dots .

Le résultat en est donc le programme clos infini

even (0)

even (s (0)) \leftarrow not even (0)

even (s (s (0))) \leftarrow not even (s (0))

\dots

Définition

Soit Modèle:Mvar un ensemble de règles de la forme

A \leftarrow B_{1}, \dots, B_{m}, not C_{1}, \dots, not C_{n}

où $A, B_{1}, \dots, B_{m}, C_{1}, \dots, C_{n}$ sont des termes clos. Si Modèle:Mvar ne contient pas de négation ( $n = 0$ 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^[1]) obtenu par propagation des clauses unitaires, ceci permet de définir le modèle stable de Modèle:Mvar.

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 Modèle:Mvar d'atomes clos, la réduction du programme Modèle:Mvar par rapport à Modèle:Mvar est l'ensemble des règles sans négation obtenu à partir de Modèle:Mvar en supprimant d'abord chaque règle pour laquelle au moins un des atomes $C_{i}$ dans son corps

B_{1}, \dots, B_{m}, not C_{1}, \dots, not C_{n}

appartient à Modèle:Mvar. Puis en supprimant les parties $not C_{1}, \dots, not C_{n}$ dans le corps de toutes les règles restantes.

On dit alors que Modèle:Mvar est un modèle stable de Modèle:Mvar si Modèle:Mvar est le modèle stable du programme $P_{| I}$ obtenu en réduisant Modèle:Mvar par rapport à Modèle:Mvar. Par construction $P_{| I}$ 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 Modèle:Mvar est un modèle de Modèle:Mvar.

Exemple

Pour illustrer ces définitions, vérifions que ${p, s}$ est un modèle stable du programme suivant :

p

r \leftarrow p, q

s \leftarrow p, not q .

La réduction de ce programme par rapport à ${p, s}$ est

p

r \leftarrow p, q

s \leftarrow p .

(En effet, puisque $q \in̸ {p, s}$ , 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 ${p, s}$ . Ainsi, comme la réduction de notre programme par ${p, s}$ 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 $p, q, r, s$ ne sont pas eux-mêmes des modèles stables. Par exemple, la réduction du programme par rapport à ${p, q, r}$ est

p

r \leftarrow p, q .

Le modèle stable de cette réduction est ${p}$ ce qui est différent de l'ensemble ${p, q, r}$ 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

p \leftarrow not q

q \leftarrow not p

a deux modèles stables ${p}$ , ${q}$ . Tandis que le programme constitué d'une seule règle

p \leftarrow not p

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

A \leftarrow B_{1}, \dots, B_{m}, not C_{1}, \dots, not C_{n}

où $A, B_{1}, \dots, B_{m}, C_{1}, \dots, C_{n}$ sont des atomes clos.

Atomes de tête: Si un atome Modèle:Mvar appartient à un modèle stable d'un programme logique Modèle:Mvar alors Modèle:Mvar est la tête d'une des règles de Modèle:Mvar .

Minimalité: Tout modèle stable d'un programme logique Modèle:Mvar doit être minimal (au sens de l'inclusion des ensembles) parmi les modèles de Modèle:Mvar.

La propriété antichaîne: Si Modèle:Mvar et Modèle:Mvar sont des modèles stables du même programme logique, alors Modèle:Mvar n'est pas un sous-ensemble propre de Modèle:Mvar (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 :

p \leftarrow p

est la tautologie $p \leftrightarrow p$ . Le modèle $\emptyset$ de cette tautologie est un modèle stable de $p \leftarrow p$ , mais son autre modèle ${p}$ n'en est pas un. Comme l'a prouvé François Fages [1994], 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 [2004] 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 $P$ , alors il est vrai dans tous les modèles stables de $P$ . Encore une fois, l'inverse n'est pas vrai en général. Par exemple, le programme

p \leftarrow not q

q \leftarrow not p

r \leftarrow p

r \leftarrow q

a deux modèles stables, ${p, r}$ et ${q, r}$ . Bien que $r$ 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 $p$ ni sa négation n'appartiennent à l'ensemble alors on ne sait pas si $p$ est vrai ou faux.

Dans le contexte de la programmation logique, cette idée conduit à la nécessité de distinguer deux types de négation — la négation par l'échec, discutée ci-dessus, et la négation forte, que nous indiqueront par $\sim$ ^[2]. L'exemple suivant, illustrant la différence entre ces deux types de négation, a été proposé par John McCarthy : "Un autobus scolaire ne peut traverser une voie ferrée qu'à condition qu'aucun train ne s'approche". Si l'on ne sait pas si un train approche ou non, alors une règle reposant sur la négation par l'échec

Cross \leftarrow not Train

n'est pas une représentation adéquate de cette idée : puisqu'elle laisserait à penser qu'il est acceptable de traverser en l'absence d'informations sur l'approche d'un train. La règle, plus faible, qui utilise une négation forte dans son corps, est ainsi préférable :

Cross \leftarrow \sim Train .

elle dit qu'il est possible de traverser si et seulement si nous savons qu'aucun train ne s'approche.

Modèles stables cohérents

Afin d'introduire la notion de négation forte dans la théorie des modèles stables, Gelfond et Lifschitz [1991] ont proposé que chacune des expressions $A$ , $B_{i}$ , $C_{i}$ dans une règle

A \leftarrow B_{1}, \dots, B_{m}, not C_{1}, \dots, not C_{n}

puisse être soit un atome, soit la négation forte d'un atome. Cette généralisation fournit alors des ensembles de réponses (au lieu de modèles stables), qui peuvent inclure à la fois des atomes et des atomes préfixés par une négation forte.

Une approche alternative [Ferraris et Lifschitz, 2005] traite la négation forte comme une partie d'un atome (elle ne nécessite donc aucun changement dans la définition d'un modèle stable). Dans cette théorie de la négation forte, nous distinguons des atomes de deux sortes, positifs et négatifs, et nous supposons que chaque atome négatif est une expression de la forme $\sim A$ , où $A$ est un atome positif. Un ensemble est dit cohérent s'il ne contient pas de paires d'atomes "complémentaires" $A, \sim A$ . Les modèles stables cohérents d'un tel programme sont alors identiques aux ensembles de réponses cohérentes au sens de [Gelfond et Lifschitz, 1991].

Par exemple, le programme

p \leftarrow not q

q \leftarrow not p

r

\sim r \leftarrow not p

a deux modèles stables : ${p, r}$ et ${q, r, \sim r}$ , le premier modèle étant cohérent et le second ne l'étant pas.

Hypothèse du monde fermé

Selon [Gelfond et Lifschitz, 1991], l'hypothèse du monde clos pour un prédicat $p$ peut être exprimé par la règle

\sim p (X_{1}, \dots, X_{n}) \leftarrow not p (X_{1}, \dots, X_{n})

(la relation $p$ est considérée comme fausse pour un tuple $X_{1}, \dots, X_{n}$ s'il n'y a aucune preuve qu'elle soit vraie). Par exemple, le modèle stable du programme

p (a, b)

p (c, d)

\sim p (X, Y) \leftarrow not p (X, Y)

se compose de 2 atomes positifs

p (a, b), p (c, d)

et 14 atomes négatifs

\sim p (a, a), \sim p (a, c), \dots

c'est-à-dire, les négations fortes de tous les autres atomes clos positifs formés à partir de $p, a, b, c, d$ .

Un programme logique utilisant la négation forte peut inclure les règles d'hypothèse du monde clos uniquement pour certains de ses prédicats, laissant ainsi les autres prédicats dans le domaine de l'hypothèse du monde ouvert.

Programmes avec contraintes

La sémantique des modèles stables peut être généralisée à de nombreux types de programmes logiques au-delà des ensembles de règles "traditionnelles" telles que discuté ci-dessus.

Une simple extension permet aux programmes de contenir des contraintes — c'est-à-dire des règles avec une tête vide :

\leftarrow B_{1}, \dots, B_{m}, not C_{1}, \dots, not C_{n} .

Rappelons qu'une règle traditionnelle peut être considérée comme une notation alternative pour une formule logique (en identifiant la virgule avec la conjonction $\land$ , le symbole $not$ avec négation $\neg$ , et en traitant $F \leftarrow G$ comme l'implication $G \to F$ écrit à l'envers). On peut aussi étendre cette convention aux contraintes, on identifie alors une contrainte avec la négation de son corps :

\neg (B_{1} \land \dots \land B_{m} \land \neg C_{1} \land \dots \land \neg C_{n}) .

Ceci permet d'étendre la définition de modèle stable aux programmes avec contraintes. Comme dans le cas des programmes traditionnels, nous commençons par des programmes qui ne contiennent pas de négation. Un tel programme peut être incohérent ; il n'y a alors pas de modèles stables. Si un tel programme $P$ est cohérent alors $P$ a un modèle minimal unique : c'est le seul modèle stable de $P$ .

Le cas des modèles stables avec négation est traité à l'aide de réductions, de la même manière que dans le cas de programme sans contraintes (voir la définition d'un modèle stable ci-dessus). Un ensemble $I$ d'atomes est un modèle stable d'un programme $P$ avec contraintes, si la réduction de $P$ par $I$ a un modèle stable et que ce modèle stable est $I$ lui-même.

Les propriétés de la sémantique du modèle stable énoncées ci-dessus pour les programmes traditionnels restent valables en présence de contraintes.

Les contraintes jouent un rôle important dans la programmation par ensembles de réponses car l'ajout d'une contrainte à un programme logique $P$ modifie la collection de modèles stables de $P$ de manière très simple : on élimine simplement tous les modèles stables qui ne respectent pas la contrainte.

Programmes disjonctifs

Dans une règle disjonctive, la tête peut être la disjonction de plusieurs atomes :

A_{1}; \dots; A_{k} \leftarrow B_{1}, \dots, B_{m}, not C_{1}, \dots, not C_{n}

(le point-virgule est considéré comme une notation alternative pour la disjonction $\lor$ ). Ainsi, les règles traditionnelles correspondent à $k = 1$ , et les contraintes à $k = 0$ . Afin d'étendre la sémantique du modèle stable aux programmes disjonctifs [Gelfond et Lifschitz, 1991], nous procédons toujours de l amême manière. En commençant par le cas où il n'y a pas de négation ( $n = 0$ dans chaque règle), les modèles stables d'un programme sont alors ses modèles minimaux. Puis nous définissons la réduction pour les programmes disjonctifs de la même manière qu'auparavant. Un ensemble $I$ d'atomes est alors un modèle stable de $P$ si $I$ est un modèle stable de la réduction de $P$ par $I$ .

Par exemple, l'ensemble ${p, r}$ est un modèle stable du programme disjonctif

p; q

r \leftarrow not q

car c'est l'un des deux modèles minimaux de la réduction

p; q

r .

Le programme ci-dessus a un autre modèle stable : ${q}$ .

Comme dans le cas des programmes traditionnels, les éléments d'un modèle stable d'un programme disjonctif $P$ apparaissent dans la tête d'au moins une règle de $P$ . Comme dans le cas traditionnel, les modèles stables d'un programme disjonctif sont minimaux et forment une antichaîne. Tester si un programme disjonctif fini a un modèle stable est $Σ_{2}^{P}$ -complet [ Modèle:Texte exact et Gottlob, 1993].

Modèles stables d'un ensemble de formules propositionnelles

Les règles (y compris les règles disjonctives) ont une forme syntaxique assez particulière, en comparaison des formules propositionnelles arbitraires. Chaque règle disjonctive est en effet une implication dans laquelle l'antécédent (le corps de la règle) est une conjonction de littéraux, et le conséquent (la tête) est une disjonction d'atomes. David Pearce [1997] et Paolo Ferraris [2005] ont cependant montré que l'on pouvait étendre la définition des modèles stables à des ensembles de formules propositionnelles quelconques. Cette généralisation a des applications dans la programmation par ensemble de réponses.

La formulation de Pearce est très différente de la définition originale d'un modèle stable. Au lieu de réduire, il se réfère à la logique d'équilibre — un système de logique non monotone basé sur des modèles de Kripke. La formulation de Ferraris, d'autre part, est basée sur des réductions, bien que le processus de construction de la réduction qu'il utilise diffère de celui décrit ci-dessus . Les deux approches pour définir des modèles stables pour des ensembles de formules propositionnelles sont équivalentes.

Définition générale d'un modèle stable

Selon [Ferraris, 2005], la réduction d'une formule propositionnelle $F$ par rapport à un ensemble $I$ d'atomes est la formule obtenue à partir de $F$ en remplaçant chaque sous-formule maximale non satisfaite par $I$ par la constante logique $⊥$ (faux). La réduction d'un ensemble $P$ de formules propositionnelles par $I$ se compose alors des réductions de toutes les formules de $P$ par $I$ . Comme dans le cas des programmes disjonctifs, on dit qu'un ensemble $I$ d'atomes est un modèle stable de $P$ si $I$ est minimale (au sens de l'inclusion des ensembles) parmi les modèles de la réduction de $P$ par $I$ .

Par exemple, la réduction de l'ensemble

{p, p \land q \to r, p \land \neg q \to s}

par l'ensemble ${p, s}$ est

{p, ⊥ \to ⊥, p \land \neg ⊥ \to s} .

Puisque ${p, s}$ est un modèle de cette réduction, et que les sous-ensembles stricts de cet ensemble ne sont pas des modèles de la réduction, ${p, s}$ est bien un modèle stable de cet ensemble de formules.

Nous avons vu que ${p, s}$ est aussi un modèle stable de la même formule, écrit en tant que programme logique. C'est un exemple d'un fait général : lorsqu'elle est appliquée à un ensemble de (formules correspondant à) des règles (au sens traditionnel, avec contrainte ou même disjonctives), la définition d'un modèle stable selon Ferraris est équivalente à la définition donnée dans cet article.

Propriétés de la sémantique générale des modèles stables

Le théorème affirmant que les éléments de tous les modèle stable d'un programme $P$ sont des atomes des têtes de $P$ peut être étendu à des ensembles de formules propositionnelles en utilisant la définition suivante. Un atome $A$ est un atome de tête d'un ensemble $P$ de formules propositionnelles si au moins une occurrence de $A$ dans une formule de $P$ n'est ni dans la portée d'une négation ni dans l'antécédent d'une implication.

La minimalité et la propriété d'antichaîne des modèles stables valable pour un programme traditionnel ne sont cependant plus vrai dans ce cas général. Par exemple, (l'ensemble singleton composé de) la formule

p \lor \neg p

a deux modèles stables, $\emptyset$ et ${p}$ . Ce dernier n'est cependant pas minimal et c'est un sur-ensemble strict du premier.

Tester si un ensemble fini de formules propositionnelles a un modèle stable est $Σ_{2}^{P}$ -complet, comme dans le cas des programmes disjonctifs.

Voir également

Bibliographie

N. Bidoit et C. Froidevaux [1987] Le minimalisme subsume la logique par défaut et la circonscription . Dans : Actes de LICS-87, pages 89-97.
T. Modèle:Texte exact et G. Gottlob [1993] Résultats de complexité pour la programmation logique disjonctive et application aux logiques non monotones . Dans : Actes de l'ILPS-93, pages 266-278.
M. van Emden et R. Kowalski [1976] La sémantique de la logique des prédicats comme langage de programmation . Journal de l'ACM, Vol. 23, pages 733-742.
F. Fages [1994] Cohérence de l'achèvement de Clark et existence de modèles stables . Journal des méthodes de logique en informatique, vol. 1, pages 51-60.
P. Ferraris [2005] Ensembles de réponses pour les théories propositionnelles . Dans : Actes du LPNMR-05, pages 119-131.
P. Ferraris et V. Lifschitz [2005] Fondements mathématiques de la programmation par ensembles de réponses . Dans : Nous allons leur montrer ! Essais en l'honneur de Dov Gabbay, King's College Publications, pages 615-664.
M. Gelfond [1987] Sur les théories autoépistémiques stratifiées . Dans : Actes de l'AAAI-87, pages 207-211.
M. Gelfond et V. Lifschitz [1988] La sémantique des modèles stables pour la programmation logique . Dans : Actes de la cinquième conférence internationale sur la programmation logique (ICLP), pages 1070-1080.
M. Gelfond et V. Lifschitz [1991] Négation classique dans les programmes logiques et les bases de données disjonctives . Informatique de nouvelle génération, Vol. 9, pages 365-385.
S. Hanks et D. McDermott [1987] Logique non monotone et projection temporelle . Intelligence Artificielle, Vol. 33, pages 379-412.
F. Lin et Y. Zhao [2004] ASSAT : Calcul des ensembles de réponses d'un programme logique par les solveurs SAT . Intelligence Artificielle, Vol. 157, pages 115-137.
V. Marek et VS Subrahmanian [1989] La relation entre la sémantique des programmes logiques et le raisonnement non monotone . Dans : Actes de l'ICLP-89, pages 600–617.
D. Pearce [1997] Une nouvelle caractérisation logique des modèles stables et des ensembles de réponses . Dans : Extensions non monotones de la programmation logique (Notes de cours sur l'intelligence artificielle 1216), pages 57-70.
R. Reiter [1980] Une logique pour le raisonnement par défaut . Intelligence Artificielle, Vol. 13, pages 81 à 132.

Notes et références

Modèle:Références

Modèle:Portail

↑ This approach to the semantics of logic programs without negation is due to Maarten van Emden and Robert Kowalski [1976].
↑ Gelfond and Lifschitz [1991] call the second negation classical and denote it by $\neg$ .

[1] This approach to the semantics of logic programs without negation is due to Maarten van Emden and Robert Kowalski [1976].

[2] Gelfond and Lifschitz [1991] call the second negation classical and denote it by $\neg$ .

[1]

[2]

Sémantique des modèles stables

Sommaire

Motivation

Lien avec la logique non monotone

Modèles stables

Définition

Exemple

Programmes sans modèle stable unique

Propriétés de la sémantique du modèle stable

Relation avec d'autres théories de la négation par l'échec

Achèvement du programme

Sémantiques bien fondées

Négation forte

Représentation d'informations incomplètes

Modèles stables cohérents

Hypothèse du monde fermé

Programmes avec contraintes

Programmes disjonctifs

Modèles stables d'un ensemble de formules propositionnelles

Définition générale d'un modèle stable

Propriétés de la sémantique générale des modèles stables

Voir également

Bibliographie

Notes et références

Menu de navigation

Sémantique des modèles stables

Motivation

Lien avec la logique non monotone

Modèles stables

Définition

Exemple

Programmes sans modèle stable unique

Propriétés de la sémantique du modèle stable

Relation avec d'autres théories de la négation par l'échec

Achèvement du programme

Sémantiques bien fondées

Négation forte

Représentation d'informations incomplètes

Modèles stables cohérents

Hypothèse du monde fermé

Programmes avec contraintes

Programmes disjonctifs

Modèles stables d'un ensemble de formules propositionnelles

Définition générale d'un modèle stable

Propriétés de la sémantique générale des modèles stables

Voir également

Bibliographie

Notes et références

Menu de navigation

Rechercher