S5Cheetah

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 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 binary search
• -minimal=4 MaxSAT