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 ) endWarning: 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]
-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.
