World's most popular travel blog for travel bloggers.

# [Solved]: Modal logic axiom S4, transitive and reflexive frame, tableaux solver

, ,
Problem Detail:

I have a difficult problem to solve which as mentioned in the title is related to modal logic axiom S4. So, here is some background knowledge that can be useful:

• S4 axiom is a class of transitive and reflexive frames
• S4 satisfiability problem is PSpace-Complete
• lastly solver for S4 does not terminate without a trick which will allow it to return a finite model.

Knowing all this, I have implemented a solver for propositional modal logic S4 and it also terminates with a finite model. In general solver uses Tableaux approach and generates graph in which the input formula is true. So, to outline what the algorithm does we have the following:

1. algorithm start by creating a graph with a single node with the input formula.
2. then we solve alpha, beta, gamma and delta formulas until each sub-formula is marked as being visited.
3. for termination part of the algorithm, every time a new node is about to be created (which is caused by delta formulas) we check whether the same node already exists in the graph. If yes, then we do not create a new node but we add an edge to the node that has that value.

This is enough to see what the algorithm does. What I am trying to do next is to prove that the algorithm is correct and will always work. For this purpose I will need to structure a formal proof.

So is anyone familiar enough with the topic to suggest what technique can be used to with the proof? What should be used bisimulation or filtration? Furthermore, it would be great if you could sketch out the proof if possible.

Any help would be very very appreciated.

To find a descriptive answer to this post, please see my thesis which presents background information of various modal logics including S4. It also contains detailed implementations of the algorithms used along with implementations in python.

I have also proved that NPSpace problems such as S4 or K4 are terminating in finite time without infinite looping. Here is the link to full report -> Link to the pdf file located on my website. I would recommend reading it fully and following the research papers which were used to make sure full knowledge is transferred onto you :).

Please note that this was a research project which I have now finished. Nevertheless, if anyone wants to expand on my work or would like me to get involved on similiar topic, please get in touch in any way possible.