Axiome de logique modale S4, cadre transitif et réflexif, solveur de tableaux

Question

J'ai un problème difficile à résoudre qui, comme mentionné dans le titre, est lié à axiome de logique modale S4.Voici donc quelques connaissances de base qui peuvent être utiles :

• L'axiome S4 ​​est une classe de cadres transitifs et réflexifs
• Le problème de satisfiabilité S4 est PSpace-Complete
• enfin le solveur pour S4 ne se termine pas sans une astuce qui lui permettra de renvoyer un modèle fini.

Sachant tout cela, j'ai implémenté un solveur pour la logique modale propositionnelle S4 et il se termine également par un modèle fini.En général, le solveur utilise l'approche Tableaux et génère un graphique dans lequel la formule d'entrée est vraie.Donc, pour décrire ce que fait l’algorithme, nous avons ce qui suit :

1. L'algorithme commence par créer un graphique avec un seul nœud avec la formule d'entrée.
2. puis nous résolvons les formules alpha, bêta, gamma et delta jusqu'à ce que chaque sous-formule soit marquée comme visitée.
3. pour la partie terminaison de l'algorithme, chaque fois qu'un nouveau nœud est sur le point d'être créé (ce qui est provoqué par des formules delta), nous vérifions si le même nœud existe déjà dans le graphique.Si oui, alors nous ne créons pas de nouveau nœud mais nous ajoutons une arête au nœud qui a cette valeur.

Cela suffit pour voir ce que fait l’algorithme.Ce que j'essaie de faire ensuite, c'est de prouver que l'algorithme est correct et qu'il fonctionnera toujours.Pour cela, je devrai structurer une preuve formelle.

Alors, est-ce que quelqu'un connaît suffisamment le sujet pour suggérer quelle technique peut être utilisée avec la preuve ?Que faut-il utiliser en bisimulation ou en filtration ? De plus, ce serait formidable si vous pouviez esquisser la preuve si possible.

Toute aide serait très très appréciée.