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
$ moltap -f "p -> K1 p"
$ view model.png
$ moltap -i
> K{1,2} p -> (
.. K1 p & K2 p
.. )
> :q