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

- Read input from a file or stdin.
- Read input from the command line.
- 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