Execution of the tableau method - start


Here you are going to start your tableau method on an initial premodel. You can draw your premodel with the mouse and add formulas in nodes by double-clicking on it. Usually if you just want to test whether a formula phi is satisfiable or not, you just have to double-click on the unique node and add the formula phi to this node. Then click on "Start tableau method".




Load a graph...

It enables to load a graph from a Scheme expression.

Example : (graph ((world n1) (formula n1 (diamond p)) (n1 link n2)))