S52SAT is a SAT-based approach for solving the modal logic S5 satisfiability problem.It is able to give in output the S5-model, when the formula is satisfiable.

The source code, written in C++ is accessible here: http://www.cril.univ-artois.fr/~montmirail/s52SAT/

View Project

Project performed in partnership with Alain Krok. The goal of this project was to copy what Nature is able to do since thousands of years:

View Project

MDK-verfier is, with some specifications in the I/O, able to tell if a Kripke model satisfies a formula for the modal logic K.The source code, written in C++ is accessible here: http://www.cril.univ-artois.fr/~montmirail/mdk-verifier/

View Project