Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Satisfaisabilité
Résumé
En logique mathématique, la satisfaisabilité ou satisfiabilité et la validité sont des concepts élémentaires de sémantique. Une formule est satisfaisable s'il est possible de trouver une interprétation (modèle), une façon d'interpréter tous les éléments constitutifs de la formule, qui rend la formule vraie. Une formule est universellement valide, ou en raccourci valide si, pour toutes les interprétations, la formule est vraie. Les concepts opposés sont la non satisfaisabilité ou insatisfaisabilité et la non-validité : une formule est insatisfaisable si aucune de ses interprétations ne rend la formule vraie et non valide s'il existe une interprétation qui rend la formule fausse.
Les quatre concepts peuvent être appliqués aux théories. Ainsi une théorie est satisfaisable s'il existe une interprétation qui rend chacun des axiomes de la théorie vrai, non satisfaisable si toute interprétation rend l'un des axiomes faux.
En théorie des modèles (de la logique du premier ordre), une formule écrite dans un certain langage, défini par une signature, s'interprète dans une structure sur cette même signature. Une formule peut contenir des variables libres. On dit alors qu'une formule est satisfaisable dans une structure s'il existe des éléments de l'ensemble de base de cette structure qui, substitués à ses variables libres, rendent la formule vraie. Une formule est satisfaisable quand elle est satisfaisable dans une certaine structure.
Si A est une structure, φ une formule, et a une collection d'éléments de l'ensemble de base de cette structure, qui satisfont φ, alors on note
A ⊧ φ [a].
Si φ est une formule close satisfaite par A, c'est-à-dire qu'elle n'a pas de variable libre, alors on écrit simplement :
A ⊧ φ.
Dans ce cas, on peut aussi dire que A est un modèle pour φ, ou que φ est vraie dans A. Si T est un ensemble de formules (une théorie en somme) satisfaite par A, on écrit
A ⊧ T.
La définition formelle de la satisfaction d'une formule dans une structure, pour une certaine interprétation des variables libres dans cette formule, procède récursivement à partir de la définition de la satisfaction des formules atomiques.
Source officielle
À 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.