MOLTAP is written in Haskell, a functional programming language. In this section we will explain the main structure our implementation.

Representing formulas

Haskell allows for a natural representation of formulas as a algebraic data type.

data Formula
   = Truth   Bool
   | Var     VarName
   | Not     Formula
   | Bin     BinOp Formula Formula -- A binary operator
   | Box     Sign  Agents Formula  -- positive is box, negative is diamond.
   | Star    Sign  Agents Formula  -- common knowledge

The prover routine will take apart formulas by pattern matching on these constructors. We have chosen to use as few constructors as possible, so conjunction, disjunction, etc. are all ‘binary operators’.

The interface

There are two Main programs. One for the command line version and one for the web interface.

The command line interface is straight forward. It just reads a string from the input, parses it and feeds it to the prover.

The web interface is a CGI program that does the same thing. It produces output in Json format (JavaScript object notation). For example the invocation moltap.cgi?term=p produces the output

{result: false
,text: "p"
,modelFile: "model/p.png"
,modelPos: [{node: "0", x: 34, y: 35, r: 25}]}

This response lists

The response from the CGI program is interpreted by a small piece of Javascript code that displays the result.

Continue reading: Representing sequents