S52SAT 1.0
1.0

S52SAT 1.0

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

How to use it

  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

Input Format

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 : ( ( p → ◊ q ) ∧ ◻ q ) should be written in InToHyLo : begin ((p1 -> <r1>p2) & [r1]p2 ) end

State-of-the-art S5 solvers

LckS5TabProver

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

SPASS 3.7

http://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/classic-spass-theorem-prover/download/
SPASS 3.7 will need ftt to read InToHyLo files. Embedded with the solver Spartacus: http://www.ps.uni-saarland.de/spartacus/

Benchmarks used

All the benchmarks used in the article can be find here : https://www.ps.uni-saarland.de/theses/goetzmann/

Contact

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