S5cheetah 1.0 is a solver which can decide the satisfiability of modal logic S5. It is developed according to the methodology described in article [1] .

S5cheetah 2.0  can find the Minimal Kripke Model for an S5 formula.

How to use S5cheetah 1.0?

./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 := <relation> formula
Example:
☐(p→ ¬◇q)∧(p∨q)
can be written as:
begin [r1](p1 -> ~<r1>q1) & (p1 | q1 ) end
Warning: 0 can not appear after an atom.    p0, q0, r0... are not acceptable.

How to use S5cheetah 2.0?

./S5cheetah2.0 [option] [Input_file] [output_file]
[Option] can be:

-minimal=1      use increamental method

-minimal=2      use decremental method

-minimal=3      use binary search

-minimal=4      use MaxSAT

[Input_file] is the path of an InToHyLo formula file. [Output_file] is the output file name.
 

References