Modal logic axiom S4, transitive and reflexive frame, tableaux solver
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.