# Reasoning in S5

I'm currently working on implementing reasoning involving time.

Since S5 (every world accessible from any other) is sufficient for what I'm trying to represent, I wanted to know what are the techniques used for reasoning (satisfiability) on this kind of logic (tableau based, etc...).

What is an algorithm that can be used? Or do someone know about some software reasoners that can do these tasks already?

• Out of curiosity, why are you using S5 to reason about time? Generally temporal logics are quite different from S5. If you think of the modal logic "accessibility" relation as the "earlier than" relation (as I believe is pretty common) it's easy to see why S5 is a bad choice. Only future and present times are accessible (or, earlier than) to the present time. May 19, 2013 at 15:46
• Because I use it to distinguish between rigid and anti-rigid properties (in other words, temporal entities and snapshot entities). Therefore I don't really need to distinguish past and future May 19, 2013 at 15:56

## 1 Answer

Here you can find a number of modal logic theorem provers. You should be able to find something that works for you there under the heading "Accessible theorem provers".

If you're taking a course on modal logic, or really want to learn this stuff, I'd steer clear of automated theorem provers except maybe to double-check your own work. I'm a pretty big fan of the tableau style of proof that Priest employs in An Introduction to Non-Classical Logic. The way he does the trees it is pretty algorithmic.

Feel free to leave a comment if you need any more info.

• +1 for recommending to do the proofs by hand. In my experience, until you've read the manual of insert your favorite automated theorem here, configured it and learned how to use it, you could have proved the theorems by hand 10 times. May 23, 2013 at 8:49
• @Eric'3ToedSloth' Absolutely agree. Especially with a tableau system like Priest's, the proofs are fairly mechanical without an automated theorem prover. May 23, 2013 at 14:12