S52SAT

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:

```  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> formula```
Example : $\left(\left(p\to ◊q\right)\wedge ◻q\right)$ should be written in InToHyLo : `begin ((p1 -> <r1>p2) & [r1]p2 ) end`

LckS5TabProver

http://users.cecs.anu.edu.au/~rpg/LCKS5TabProver/
Patch

SPASS 3.7

SPASS 3.7 will need `ftt` to read InToHyLo files. Embedded with the solver Spartacus: http://www.ps.uni-saarland.de/spartacus/
```    Valentin Montmirail