Satisfaisabilité

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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) qui rend la formule vraie. Une formule est valide si pour toutes les interprétations la formule est vraie. Les concepts opposés sont l'insatisfaisabilité et la non-validité, ainsi, 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 : une théorie est satisfaisable (valide) si une (toutes) interprétations rend chacun des axiomes de la théorie vrai, et la théorie est insatisfaisable (non valide) si toute (une) interprétation rend chacun des axiomes de la théorie faux.[réf. souhaitée]

La satisfaisabilité dans la théorie des modèles[modifier | modifier le code]

Dans la théories des modèles, une formule atomique est satisfaisable s'il existe des éléments d'une structure qui rendent la formule vraie[1]. Si A est une structure, φ une formule, et a une collection d'éléments pris à partir de la structure, qui satisfont φ, alors on note

A ⊧ φ [a].

Si φ n'a pas de variable, alors, si φ est une formule atomique, et qui est satisfaite par A, alors on écrit

A ⊧ φ.

Dans ce cas, on peut aussi dire que A est un modèle pour φ, ou que φ est vrai dans A. Si T est un ensemble de formules atomiques (une théorie en somme) satisfaite par A, on écrit

A ⊧ T.

Notes et références[modifier | modifier le code]

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Satisfiability » (voir la liste des auteurs).

  1. (en) Wilfrid Hodges (de), A Shorter Model Theory, Cambridge University, (ISBN 0521587131, lire en ligne), p. 12.

Voir aussi[modifier | modifier le code]