In recent years the number of computational tools useful for modal logics, and related logics, has increased significantly, and is continuously increasing. The following is an incomplete list of

Your contribution

If you'd like something added or changed please let Renate Schmidt ( know. Some of the links below are unfortunately broken. I would particularly welcome updates about these so that this page remains useful.

Accessible theorem provers



Automated correspondence theory

These tools are useful for computing correspondence properties:

For the back-translation:


Other tools

Generators of formulae

Collections of problems

The collection of modal problem sets is beginning to grow rapidly. The webpages of some provers above also have links to benchmark collections.

Also of interest: Benchmark formulae for intuitionistic propositional logic.