Logica modale axiom S4, frame transitivo e riflessivo, risolutore di tableaux

Question

Ho un problema difficile da risolvere che come menzionato nel titolo è correlato a logica modale axiom S4.Quindi, ecco alcune conoscenze di base che possono essere utili:

• S4 Axiom è una classe di cornici transitive e riflessive
• S4 Il problema di soddisfazione è PSPACE-completo
• Infine, il risolutore di S4 non termina senza un trucco che gli consentirà di restituire un modello finito.

Sapendo tutto questo, ho implementato un risolutore per la logica modale proposizionale S4 e termina anche con un modello finito. In generale il solutore utilizza l'approccio Tableaux e genera grafico in cui è vera la formula di input. Quindi, per delineare ciò che l'algoritmo abbiamo quanto segue:

1. Algoritmo Inizia creando un grafico con un singolo nodo con la formula di input.
2. Quindi risolviamo formule alfa, beta, gamma e delta fino a quando ogni sotto-forma è contrassegnata come visitata.
3. Per una parte di terminazione dell'algoritmo, ogni volta che un nuovo nodo sta per essere creato (che è causato da formule delta) controlliamo se lo stesso nodo esiste già nel grafico. Se sì, non creiamo un nuovo nodo ma aggiungiamo un bordo al nodo che ha quel valore.

Questo è abbastanza per vedere cosa fa l'algoritmo. Quello che sto cercando di fare dopo è dimostrare che l'algoritmo è corretto e funzionerà sempre. A tale scopo dovrò strutturare una prova formale.

Quindi qualcuno ha abbastanza familiarità con l'argomento per suggerire a quale tecnica può essere abituata con la prova? Cosa dovrebbe essere usato bisimolazione o filtrazione? Inoltre, sarebbe bello se potessi disegnare la prova se possibile.

Qualsiasi aiuto sarebbe molto apprezzato.