This page is presenting the tool called `S52SAT`

(pronounced S5 to SAT), a SAT-based approach for solving the modal logic S5-satisfiability problem

Binaries: Linux Mac OS X View source

v2.0 You can access the version 2.0 and its new features here

Use: ./S52SAT $formula [upperbound] [options] [optis] where $formula is an InToHyLo formula and [upperbound] can be: -diamondDegree to use as an upper-bound, the diamond degree of the formula -nbDiamonds to use as an upper-bound, the number of diamonds in the formula -nbModals to use as an upper-bound, the number of modalities in the formula and [optis] can be : -caching to perform a lazy-caching during the transformation in SAT formula and [options] can be: -print to display the modal logic formula after a NNF transformation -info to get all the information relative to the modal formula in input -model to display the S5-model if it exists -ToCnf to display the CNF equivalent of the input modal logic formula

For the input format, we choose to use the already existing format InToHyLo.

file := begin formulas end formulas := formula | formula ; formulas 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> formulaExample : $((p\to \u25caq)\wedge \u25fbq)$ should be written in InToHyLo :

`begin ((p1 -> <r1>p2) & [r1]p2 ) end`

Patch

SPASS 3.7 will need

`ftt`

to read InToHyLo files.
Embedded with the solver Spartacus: http://www.ps.uni-saarland.de/spartacus/
For any additional information about this tool, please feel free to contact montmirail@cril.fr.

Valentin Montmirail Université d'Artois CRIL - CNRS UMR 8188 Rue Jean Souvraz SP 18 62307 Lens FRANCE http://www.cril.fr/~montmirail