Compilation and Running of the TWB

===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