Propositional Modal Logic Using Tableaux Methodology For Theorem Proving

Master Thesis can be found here

These are Propositional Modal Logic solvers. I have used tableaux method to derive solutions. We have following logics covered:

K: completed - no properties

T: completed - reflexive []p -> p

K4: completed- transitive frames

KB: completed - symmetric p -> []<>p

B: completed - symmetric and reflexive

S4: completed - reflexive and transitive []p -> [][]p

S5: completed - reflexive, transitive and symmetric S4 + <>p ->[]<>p

How to use:

1. Download all the .py files
2. Place them in one folder
3. Open Logic_?.py with python interpreter where ? corresponds to logic
4. Using instructions below write formula
5. Input your formula inside specific file str_psi = "formula"
6. Run, test and get results
7. Each graph corresponds to a Kripke model in which the formula is satisfiable
Formula input instructions:
    To input correctly formula
        AND is represented by the symbol:                ^
        OR is represented by the symbol:                 V
        IMPLICATION is represented by the symbol:        >
        BOX (must) is represented by the symbol:         B
        DIAMOND (possibly) is represented by the symbol: D

    :Example input:
        str_psi = "~(p > Br) ^  (Dp >((DDDs^Bt) V (Bs ^ Dq))) "

        which can be easier visualised as
        ~(p -> []r) ^ (<>p -> ((<><><>s ^ []t) V ([]s ^ <>q)))
    :After writting a formula run Logic_?.py and it will bring the results
    :Do no change the name of the string (str_psi)

Note: that a lot more information can be found in the report mentioned above.


If you have any questions, drop me an email or open an issue and leave stars! :). If you require any help within complexity theory or have a potentials projects I could be interested as well.

This Work

My work has potentially been used by many people, mainly in academia.

here you can find another project which adapted some of the algorithms, theorems and optimised some of those solvers. It is a fork of the repo.


Final Year Masters Project: modal logic solver tableaux

Modal_logic Info

⭐ Stars 16
🔗 Source Code
🕒 Last Update a year ago
🕒 Created 6 years ago
🐞 Open Issues 0
➗ Star-Issue Ratio Infinity
😎 Author marcincuber