===Compilation===
Each file in the TWB are translated in an Ocaml compilation unit. We assume that the logic rules for
the propositional modal logic shown before are saved in a file ''pc.ml'' and the negation normal form function
in a file ''pclib.ml'' . To compile the logic module we use the utility '''twbcompile''' that is shipped with the TWB
libraries.
$./twbcompile pc.ml
............Done.
$
The result of the compilation is the file '''pc.twb''' that is the object prover for propositional classical logic.
===Running .twb files===
To run the file '''pc.twb''' we can either give it a file of formulae to prove as argument or passing a formula
on the stdin channel.
We show the proof trace of a simple tautology
~ (~ p) <-> p:
$./pc.twb --trace
~ (~ p) <-> p
Proving: ~ (~ p) <-> p
Start Node: ((p & (~ p)) v (p & (~ p)))
Or ( 0 -> 1 )
(p & (~ p)) ;
And ( 1 -> 2 )
(~ p) ; p
Id ( 2 -> 3 )
Or ( 0 -> 4 )
(p & (~ p)) ;
And ( 4 -> 5 )
(~ p) ; p
Id ( 5 -> 6 )
Time:0.0000
Result:Close
Total Rules applications:6
''''Note that the initial formula is immediately transformed into
negated normal form before being processed by the tableau
rules.''''
====Command Line Options====
Provers generated with the TWB have a number of standard options to switch on/off different
behaviors. In particular, for the moment we concentrate on just a few of the options :
* ''--noneg'' is the runtime option to switch off the negation of the input formula. This is useful when
the prover is used as a satisfiability procedure. The same effect is obtained by not specifying
a value for the NEG function in the logic module source.
* ''--nopp'' disables the preprocessing function. In our example, the negation normal form function nnf
is the pre-processing function PP.
* ''--trace'' enables a rule by rule trace of the proof. By default the twb outputs only the outcome of the proof. By tracing the proof it
is possible to do a step by step analysis of the proof. Useful for debugging.
* ''--verbose'' displays additional information
$./pc.twb --help
usage: ./pc.twb [-options] [file]
--nopp disable preproc function
--noneg disable negation function
--level trace level
--trace print proof trace
--time set exec timeout
--verbose print additional information
--outdir set output directory
--out set output type
--nocache disable function memoization
-help Display this list of options
--help Display this list of options