S5cheetah is a solver for deciding the satisfiability of modal logic S5. It is developed according to the methodology described in article  . The binaries can be download here:
[Option] can be:
-model to display the S5-model if it exists
[Input_file] is the path of an InToHyLo formula file.
[Output_file] is the output file name.
Input file format
The input file should in InToHyLo format.
file := begin formula end
formula := true | false | proposition | negation | conjunction | disjunction | implication | dimplication | box | diamond | ( formula )
proposition := p number
relation := r number
negation := ~formula
conjunction := formula & formula
disjunction := formula | formula
implication := formula -> formula
dimplication := formula <-> formula
box := [relation] formula
diamond := formula
can be written as:
begin [r1](p1 -> ~q) & (p | q ) end