Construction modèle-théorique en logique modale qui quotientte un modèle de Kripke (éventuellement infini) par une équivalence définie à partir d′un ensemble fini de formules, de sorte que le quotient fini obtenu (la filtration) préserve la vérité de chaque formule de cet ensemble fini, permettant des arguments de modèle fini pour la satisfaisabilité et la complétude.

Principe

Partitionner les états selon leurs valuations sur l′ensemble fini de sous-formules pertinentes et écraser les états équivalents en classes d′équivalence, en définissant des relations de successeur entre classes pour préserver la satisfaisabilité des formules choisies tout en réduisant la taille du modèle.

Démonstration

Pour prouver la propriété du modèle fini pour une logique modale normale sur une classe restreinte de cadres, prendre un modèle satisfaisant une formule, rassembler l′ensemble fini des sous-formules, construire l′équivalence de filtration sur les états qui coïncident sur ces sous-formules, et former le modèle quotient fini qui satisfait encore la formule initiale.

Mauvaise application

Supposer qu′une filtration préserve la vérité de formules en dehors de l′ensemble de sous-formules choisi, ou appliquer la filtration standard sans tenir compte des conditions de cadre (comme la transitivité ou la symétrie) que le quotient peut violer, entraînant des affirmations incorrectes de complétude ou de préservation de cadres.

Conséquence

Lorsqu′elle est valide, la filtration produit des modèles finis pour des formules satisfaisables (propriété du modèle fini), simplifie les preuves de complétude en réduisant des modèles canoniques en quotients finis et fournit des témoins finis algorithmiques pour la satisfaisabilité dans de nombreux systèmes modaux.

Inversion

L′idée inverse est le dépliage en arbre (unravelling) qui transforme un modèle en une structure arborescente préservant les vérités locales mais pouvant l′étendre ; l′inversion met en lumière le compromis entre écrasement pour la finitude et expansion pour la régularité arborescente.

Limite

La filtration est liée à un ensemble fini de formules choisi et à des logiques où la préservation des sous-formules et les propriétés de cadre sont compatibles avec la quotientation ; elle peut échouer ou nécessiter une adaptation pour des logiques avec modalités globales, opérateurs à point fixe, fonctionnalités hybrides, ou lorsque les conditions de cadre ne sont pas préservées par le quotient.

Tension sémantique

La tension survient entre l′utilisation de la filtration pour obtenir des modèles canoniques petits et l′emploi de méthodes automates-théoriques ou algébriques qui évitent l′écrasement des modèles ; aussi entre la préservation syntaxique des sous-formules et la perte d′autres contraintes sémantiques de cadre dans le quotient.

Synthèse

La Méthode de Filtration écrase un modèle selon l′équivalence induite par un ensemble fini de formules pour produire un modèle plus petit préservant la vérité de ces formules ; c′est un moyen sémantique concret d′obtenir des résultats de modèles finis et des témoins constructifs de satisfaisabilité, à condition de traiter soigneusement les conditions de cadre et les caractéristiques du langage.