MOLTAP

• Overview
• The prover
• Examples
• Users guide
• Syntax reference
• Download

Theory

• Introduction
• Propositional tableaux
• Modal tableaux
• KD, S4, S5, etc.
• Soundness
• Completeness
• Knowledge in groups
• Common knowledge

Implementation

• The basics
• Representing tableaux
• Working with models

Conclusion

• Conclusions
• Related work
• References

Downloads

• The users guide in PDF format
• Source code (github)
• Command line executables (linux and windows)

Source code

To be able to build the source code you need the following programs:

• GHC: the Glasgow Haskell Compiler, version 7.8 or newer.
• GraphViz
• Several haskell libraries. These can be installed with cabal.

On both Linux and Windows the source code can than be built by executing:

sh build.sh

Or if some libraries are installed locally:

sh build.sh --user

This builds both the documentation and the two front ends. To only build the programs pass the --no-doc flag, or build manually with

cabal configure
cabal build
cabal install