a Java implementation of an interative tableau first order theorem prover.
It is mainly used for teaching, but can also prove simple FOL formulas automatically.
Several options can be set when running to activate/deactivate features.
The following parameters can be set when calling the applet from the command line.
| Option | default | Meaning |
|---|---|---|
| `-Dtablet.showancestor=[true | false]` | true |
| `-Dtablet.allowautorun=[true | false]` | false |
| `-Dtablet.absolutetex=[true | false]` | ? |
-Dtablet.fontsize=<number> |
? | font size to be used to show nodes |
| `-Dtablet.allowunification=[true | false]` | false |