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 : {| cellpadding=5 style="width:18em" |p |q |r |s |- |T |T |T |F.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées (11)

Unités associées (1)

Concepts associés (7)

Séances de cours associées (4)

Négation par l'échec

La négation par l'échec (en anglais NAF pour negation as failure, ou NBF pour negation by failure) est une règle d'inférence non monotone en programmation logique, utilisée pour la dérivation de à partir de l'échec de la dérivation de . C'est une caractéristique importante de la programmation logique depuis les origines de Planner et de Prolog. En Prolog, la négation par l'échec est habituellement implémentée en utilisant les fonctionnalités non logiques du langage.

Hypothèse du monde clos

La notion d'hypothèse de monde clos est utilisée en particulier en Prolog, elle s'oppose à l'hypothèse de monde ouvert (voir aussi l'article Logique argumentative) et concerne la question du vrai et du faux. Elle signifie qu'un fait est considéré comme faux si, en un temps fini, on échoue à montrer qu'il est vrai, ce qui revient à dire que tout ce qui est vrai doit être connu (inclus dans la base de données des faits) ou démontrable en temps fini, il n’y a pas de monde extérieur qui pourrait contenir des éléments de preuve inconnus du programme.

Autoepistemic logic

The autoepistemic logic is a formal logic for the representation and reasoning of knowledge about knowledge. While propositional logic can only express facts, autoepistemic logic can express knowledge and lack of knowledge about facts. The stable model semantics, which is used to give a semantics to logic programming with negation as failure, can be seen as a simplified form of autoepistemic logic. The syntax of autoepistemic logic extends that of propositional logic by a modal operator indicating knowledge: if is a formula, indicates that is known.

Atelier Coq: Types de données inductives et preuves CS-452: Foundations of software

Couvre la définition d'un type de données inductives dans Coq et la façon de construire des preuves de manière interactive en utilisant des tactiques.

Analyse de terminaison à l'aide de paires de dépendances

Explore l'analyse automatisée de terminaison à l'aide de paires de dépendances, couvrant les techniques classiques et modernes, les concours annuels et des outils comme AProVE.

Induction pour les solvants SMT

Explore les techniques d'induction dans les résolveurs SMT, en mettant l'accent sur l'implémentation de CVC4 et la performance compétitive avec d'autres proverbes.

Imagine the Unseen World: A Benchmark for Systematic Generalization in Visual World Models

Caglar Gulcehre

Systematic compositionality, or the ability to adapt to novel situations by creating a mental model of the world using reusable pieces of knowledge, remains a significant challenge in machine learning. While there has been considerable progress in the lang ...

2023

Machine Learning Methods for Robust Uncertainty Quantification and Controller Approximation

Emilio Maddalena

This thesis is situated at the crossroads between machine learning and control engineering. Our contributions are both theoretical, through proposing a new uncertainty quantification methodology in a kernelized context; and experimental, through investigat ...

EPFL2023

Emergence of diauxie as an optimal growth strategy under resource allocation constraints in cellular metabolism

Vassily Hatzimanikatis, Pierre Guy Rémy Salvy

Diauxie, or the sequential consumption of carbohydrates in bacteria such as Escherichia coli, has been hypothesized to be an evolutionary strategy which allows the organism to maximize its instantaneous specific growth-giving the bacterium a competitive ad ...

NATL ACAD SCIENCES2021