Une méthode formelle qui enrichit les formules syntaxiques par des étiquettes explicites (par exemple mondes, états, ressources ou annotations de preuve) portant de l'information sémantique et guidant l'application des règles d'inférence syntaxiques.

Principe

Attacher des annotations sémantiques minimales sous forme d'étiquettes aux objets syntaxiques afin que l'application des règles et la composition des preuves deviennent des opérations locales et dirigées par la syntaxe régies par des règles de manipulation d'étiquettes.

Démonstration

En logique modale, chaque formule est associée à une étiquette de monde w et les règles permutent ou relient les étiquettes (wRv) pour simuler l'accessibilité ; un séquent comme w:A, wRv ⊢ v:B rend explicite la sémantique de □ et ◇ dans les étapes de preuve.

Mauvaise application

Considérer les étiquettes comme de simples étiquettes cosmétiques sans imposer de contraintes sur elles conduit à des preuves non valides où les relations sémantiques (par exemple l'accessibilité ou la consommation de ressources) sont ignorées.

Conséquence

Bien utilisée, la déduction étiquetée produit des systèmes de preuve plus proches des modèles sémantiques, permet une application locale des règles, des extensions modulaires pour de nouvelles modalités ou ressources, et simplifie souvent l'élimination des coupures ou l'extraction de contre-modèles.

Inversion

La version inverse est une déduction purement syntaxique sans étiquettes, où les règles doivent suivre implicitement les conditions sémantiques de façon globale ; cela peut réduire la modularité et augmenter la non-déterminisme dans la recherche de preuves.

Limite

S'applique aux logiques dont la structure sémantique peut être encodée comme une algèbre d'étiquettes finie ou des contraintes relationnelles ; exclut les approches nécessitant une évaluation sémantique complète à chaque étape (par exemple un model checking intensif) plutôt qu'une manipulation symbolique des étiquettes.

Tension sémantique

Un tiraillement existe entre les systèmes riches en étiquettes qui exposent le détail sémantique dans les preuves et les calculs étiquetés qui gardent les étiquettes minimales pour préserver l'élégance syntaxique ; plus d'étiquettes améliorent la fidélité sémantique au prix d'une complexité de preuve accrue.

Synthèse

La déduction étiquetée intègre la tenue de compte sémantique dans la syntaxe au moyen d'étiquettes, échangeant les appels sémantiques globaux contre des transformations d'étiquettes locales et dirigées par les règles qui rendent explicites et modulaires le raisonnement sur modalités, ressources ou états.