S5cheetah is a solver for deciding the satisfiability of modal logic S5. It is developed according to the methodology described in article [1] . The binaries can be download here:

How to use it?

./S5cheetah [option] [Input_file] [output_file]

[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
Example:
☐(p→ ¬◇q)∧(p∨q)

can be written as:

begin [r1](p1 -> ~q) & (p | q ) end