Une fonction qui assigne des valeurs de vérité (généralement Vrai ou Faux) à des variables propositionnelles ou à des atomes ground dans une structure donnée, utilisée pour évaluer des formules ou tester la satisfiabilité.

Principe

Fournir une fonction complète de l'ensemble des propositions atomiques (ou atomes ground) vers les valeurs de vérité afin que la vérité des formules complexes puisse être déterminée compositionnellement à partir de ces affectations atomiques.

Démonstration

Une affectation de vérité v avec v(p)=V, v(q)=F donne v(p ∨ q)=V et v(p ∧ q)=F ; en model checking, une affectation qui satisfait tous les atomes ground d'une théorie correspond à un modèle candidat sur la couche propositionnelle.

Mauvaise application

Confondre une affectation partielle (valeurs pour certains atomes seulement) avec une affectation totale lors du test de satisfiabilité globale peut produire de faux négatifs ; de même, utiliser des affectations inconsistantes (attribuer à la fois V et F) est mal formé.

Conséquence

Une affectation de vérité bien définie permet l'évaluation constructive et les vérifications algorithmiques de satisfiabilité (p. ex. via des solveurs SAT) et sous-tend la construction de contre-modèles pour réfuter des implications.

Inversion

La perspective inverse considère l'évaluation sémantique comme basée sur des structures modèles (interprétations des symboles non atomiques) plutôt que comme de simples fonctions des atomes vers des valeurs de vérité.

Limite

Se réfère aux affectations d'atomes propositionnels ou d'atomes ground dans un domaine fixé ; exclut les valuations sémantiques qui attribuent des objets sémantiques non booléens (p. ex. dénotations de termes dans des modèles du premier ordre) sauf si elles sont réduites à des valeurs de vérité.

Tension sémantique

Tension entre voir les affectations de vérité comme des objets computationnels finis utilisés dans les algorithmes et voir les valuations sémantiques comme des applications structurelles portant un contenu interprétatif plus riche que de simples valeurs de vérité.

Synthèse

Une affectation de vérité est la fonction explicite qui fixe les valeurs de vérité des constituants atomiques, permettant l'évaluation compositionnelle des formules et servant de substrat computationnel aux tâches de satisfiabilité et de recherche de modèles.