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

View the users guide in PDF format.

Web interface

Entering a formula

By default the prover web interface shows a single line textbox where a formula can be entered. See the syntax reference for a description of the syntax to use. Press Enter to evaluate the formula.

When a single line does not suffice, the input field can be expanded by clicking the downward pointing arrow on the right.

True formulas

When a formula is valid in all worlds MOLTAP will show a green box.

False formulas

For formulas that are not valid in all worlds MOLTAP will show a red box with a counter model. In this model the formula is false. When the mouse is moved over a subformula the program will indicate in which worlds this subformula is true (by a green circle) and in which worlds it is false (by a red struck circle).

Command line program

MOLTAP also comes with a command line version. The syntax is exactly the same as for the web interface. This program supports three modes of operation

1. Read input from a file or stdin.
2. Read input from the command line.
3. A simple interactive mode.

In each case one or more formulas are evaluated (proven/disproven). The program writes true or false to the output, and if the formula is false generates a counter model. The command line program supports the following arguments

Short form	Long form	Description
FILE		Run the program on the given input file.
-?	--help	Show help page.
-i	--interactive	Interactive mode.
-f FORMULA	--formula=FORMULA	Give a formula directly on the command line.
-o FILE	--model-name=FILE	Filename for generated model images, the default is “model.png”. The extension determines the generated image type.

When reading input from the command line the end of file character must be used to indicate the end of the formula, use ^Z on windows and ^D on linux.

In interactive mode each line is considered to be a formula, unless there are remaining parentheses to be closed. Use :? to show the help page and :q to quit.

Example session

$ moltap
x | ~x
^Z
true
$ moltap -f "p -> K1 p"
false
$ view model.png

$ moltap -i
> K{1,2} p -> (
.. K1 p & K2 p
.. )
true
> :q
Goodbye