The Modal Solver Suite

An implementation of a Decision and Minimization Procedure for Modal Logic

This repository containts the Python modules that comprise the Modal Solver Suite.

Modules

1. driverObj.py

   The main module, which contains the decision and minimization procedure, and invokes the Kripke model constructor.

2. kripkeModelConstructor.py

   Parses the output from Enfragmo to produce a .dot file and .svg file for each model.

3. verifier.py

   Parses problem instance files and returns the formula represented by the file in infix notation.

4. reuseableCode.py

   Various code snippets used in multiple modules.

5. formulaConversion.py

   This module is meant to convert the modal benchmark formulas from the Logic Work Bench into a usable form.

Dependencies The Modal Solver Suite requires the following Python modules to function:

1. Union Find (branch of Algorithms repository that includes setup.py)
2. Graphviz - tested with v0.4.10
3. Treelib - tested with v1.3.3 - commit 65635f4
4. Plac
5. Re
6. Os
7. Defaultdict

It is recommended that you create a virtual environment with the Python 3.4 interpreter and these modules.

If you have not already done so, please clone the following repo:

Supplementary Files

Which contains the theory file for the modal logic K, sample problem instance files, and some examples of first-order frame correspondents.