3
$\begingroup$

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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ You are aware that NPSpace=PSpace, right? Almost nobody talks about NPSpace, for this reason. $\endgroup$
    – David Richerby
    Commented Oct 13, 2016 at 7:05
  • $\begingroup$ If you actually read the question and then read my proposed answer, you would easily find a link to the report which nicely covers these things, including your unrelated comment which does not bring anything new. $\endgroup$
    – marcincuber
    Commented Oct 13, 2016 at 15:42
  • $\begingroup$ Your reply is completely irrelevant to the comment I wrote. I stand by my comment, and I point out that it is related to your answer because your answer talks about the class NPSpace. $\endgroup$
    – David Richerby
    Commented Oct 13, 2016 at 15:45
  • $\begingroup$ Keep it up, perhaps move your irrelevant comments somewhere where it will matter. I do talk about NPSpace and PSpace, the document I pointed out clearly outlines that they are the same. I wonder why you didn't comment at all when answer was required... Maybe concentrate more on helping others and less on posting opinions which nobody asked for. $\endgroup$
    – marcincuber
    Commented Oct 13, 2016 at 17:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.