```
$./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
```

```
CONNECTIVES [ "~";"&";"v";"->";"<->" ]
```

The keyword '''CONNECTIVES''' in the TWB introduces a list of string separated with a simicolon ";".
Each string can be used as a connective in the grammar definition (below) and it will become a reserved keyword.
Connectives can be of variable length, can be composed by a mix of numbers, symbols and characters.
====Restrictions====
* The backslash symbol "\" cannot be used.
* The symbol vertical bar "|" cannot be used.
* Double semicolon ";;" cannot be used.
* The string "ATOM" cannot be used.
* The symbols "(", ")", "{" , "}" cannot be used.
===Grammar===
```
GRAMMAR
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| ~ formula
;;
expr := formula ;;
END
```

The TWB allows the user to define the grammar to be used for the formulae in the tableau/sequent rules.
A TWB grammar is composed of a sequence of productions separated by a double semicolon ";;". Two
mandatory productions are ''formula'' and ''expr''. A third pre-defined production that can be omitted is ''node''.
* node: this production defines the shape of a tableau/sequent node. By default, a tableau node is composed of a set of formulae.
* expr: this production defines the outer most expressions used in the definition of tableau rules. Generally an expression is just a formula. In more complicated tableau rules, an expression can be a formula decorated with a label or with another arbitrary data structure.
* formula : this production defines the shape of the formula definition to be used in the tableau rules.
====Conventions====
* Lower case identifier in a production are interpreted as a grammar identifier for a production.
* Upper case identifiers are interpreted as constants (eg. Verum and Falsum).
* The keyword '''ATOM''' identifies an atom in the grammar.
====Restrictions====
The grammar accepted by the TWB is a loose LL(1) grammar. Conflicts are not handled automatically and the definition
of ambiguous grammars can lead to unspecified results.
====NOTA BENE====
At the moment of writing the grammar machinery still has some minor bugs that we
are seeking to address in future releases.
===OCaml Code ===
```
open Twblib
open Pclib
```

Since the TWB is built on top of ocaml, it is possible to specify arbitrary ocaml functions with a twb file.
In this example, we use twb modules by using the ocaml directive ''open''. This operation imports into
the current namespace all the functions and data types defined in the module "twblib.ml" and "pclib.ml".
Note that the leading lowercase letter of the file name is capitalised when using the "open" directive.
In general, it is possible to write arbitrary functions and data types that can be used in the subsequent part of file.
===Tableau Definition===
```
TABLEAU
RULE Id { a } ; { ~ a } ; X === Close END
RULE False { Falsum} ; X === Close END
RULE And { A & B } ; X === A ; B ; X END
RULE Or { A v B } ; X === A ; X | B ; X END
END
```

A tableau definition is delimited of the keywords '''TABLEAU ... END'''.
A tableau is composed of a sequence of
rule definitions. A rule is delimited by the keywords '''RULE ... END''' .
In general, tableau/sequent rules may consist of up to seven components:
*Numerator: The numerator is a list of formula schemas separated by semicolons and specifies a partition of the current node in the proof tree. Formulae schemas are parsed according to the connectives declared in the connectives section with principal formulae enclosed in braces { }. A pattern is ''restricted'' if it is specified by a formula schema containing connectives like A -> B and Box A. A pattern is {\em unrestricted} if it is specified by just a meta-variable like X. There may be many ways of partitioning a node to match the pattern specified by the numerator leading to implicit choice-points.
* Separator: A rule commits to the first numerator pattern choice if the separator between the numerator and denominators is a sequence of at least two "='' symbols. A rule backtracks over the different pattern choice-points if the separator is a sequence of at least two ``-'' symbols and the current partition choice does not close. Intuitively, a rule that commits is declared to be invertible and a rule that does not commit is declared to be non-invertible. However, the TWB does not check that the rule is really invertible. It assumes that the user has proved an inversion lemma independently.
* Denominator: In general, a rule can have a list of denominators related by a branching operator. Each denominator is a list of formula schemas and specifies how to construct the root nodes of the branches that extend the tableau using the patterns assigned to the meta-variables in the numerator. The (universal) branch separator | is an instruction to close the current node if ''every'' denominator closes. The (existential) branch separator || is an instruction to close the current node if ''some'' denominator closes. These are actually instances of conditional branching which are instructions to close the current node if the denominators meet a specified condition.
* Cond: A rule is applicable if the side-conditions are satisfied as specified using the COND construct. If all the side conditions are true, then the tentative partition is accepted. Otherwise the partition is not considered and the pattern matching algorithm proceeds until a successful partition is found.
* Action: If the rule is applicable then the ACTION construct specifies actions on the current histories or variables to compute the histories of the children.
* Branch: Conversely, branch conditions, specified by the keyword BRANCH, are executed on backtracking to check whether to explore the next branch (if there is one) or to backtrack further. It is possible to specify a list of branch conditions, one for every branch and each set of branch conditions will have access to all variables returned by any branch already explored. An attempt to access a variable related to a branch yet to be visit will generate a run-time error.
* Backtrack: Specifies how to synthesize the result for the current node from the results of the children.
====We now analyze each rule definition:====
```
RULE False
{ Falsum } ; X
=======================
Close
END
```

This rule define an axiom. The rule is introduced by the keyword '''RULE''', it is the followed by an uppercase rule
identifier ''False'' that will be used to invoke the rule in the strategy section. The body of the rule is a schema
representing a tableau / sequent node as defined in the grammar. In this case a tableau node is a set of formulae
separated by a semicolon ";". In this case, for the rule to be applicable, the node schema requires a principal formula
containing the constant '''Falsum''' and an anonymous, possibly empty, set of formulae '''X''' that contains all other formulae
in the node.
If the rule is applicable, then this particular rule stops the procedure by using the keyword '''Close'''. Intuitively this rule is
a device to stop the procedure whenever we find an instance of bottom (Falsum) in the tableau node.
```
RULE Id
{ a } ; { ~ a } ; X
=========================
Close
END
```

The rule above defines the axiom '''Id''' that detects classical inconsistencies, that is a positive and a negative occurrence of an
atom in a tableau node. The body of this rule has two principal formulae and a anonymous set X. This rule elucidates two important
features of the pattern matching machinery of the TWB. First we notice that we used lower case to identify the schemas
`{ a } ; { ~ a }`

. In the pattern definitions, lowercase always match atoms, while uppercase match both atoms and
formulae. In this instance we want to restrict the application of the rule Id only to atoms. Secondly, when the same identifier is used
more then once in the definition of a formula schema, the TWB machinery will try to unify it with other occurrences. In this case the rule
will be applicable if and only if, the atom '''a''' occurs both positively and in the formula '''~ a''' .
```
RULE And
{ A & B } ; X
=======================
A ; B ; X
END
```

The rule '''And''' is a rewriting rule. The body of the rule is composed by a principal formula and an anonymous set.
If there is at least one formula in the current tableau node containing a conjunction (eg. a & b), then the rule is applicable.
Then the denominator of the rule, breaks down the conjunction into its conjuncts and copies across all the other formulae in
the node untouched.
====Note====
Even if it is always possible to specify the anonymous set in the rule schemas, this is not recommended. The default of the TWB is to
leave untouched all formulae that are not explicitly manipulated by a rule application. The previous rule could have also been written as
```
RULE And { A & B } === A ; B END
```

and we will often use this formulation in the remainder of this tutorial.
-------------
EXERCISE: how does the following rule differ operationally from the And rule above?
```
RULE And A & B === A ; B END
```

ANSWER:
In the first case, the rule will choose one single &-formula as principal formula.
In the second case all &-formulae will be chosen at once in one rule application.
But note that the subformula (d & e) below is not touched because it is not at the
top-level in node 1.
```
#echo "(a & b) & (c & (d & e)) " | ./pc.twb --trace --noneg
And ( 0 -> 1 )
(a & b) ; (c & (d & e))
And ( 1 -> 2 )
a ; b ; c ; d & e ;
Time:0.0000
Result:Open
Total Rules applications:2
```

--------------------------
```
RULE Or
{ A v B }
======================
A | B
END
```

First note, that there is no ancillary X in the numerator or denominator in keeping with the just mentioned note which allows us to assume that all other formulae in the node are left untouched.
The '''Or''' rule matches a disjunction and creates two new branches that will be explored by the tableau procedure. The semantics of the
Or rule requires both branches to be closed, for the tableau rooted at the current node to be closed. This semantics is enforced by using the
single bar "|" as the separator between two branches. In particular, the single bar imposes a condition on backtracking whether to explore the
next branch or not. To understand how the TWB works in this instance we need to introduce the notion of visit more in details. By default, the
TWB uses a left-to-right depth-first visiting strategy. When the strategy is invoked with the current node, first an applicable rule is selected, then
the rule is applied and the strategy is re-invoked on all branches that result from the rule application. On backtrack, that is, when the visit function
returns from the visit of a branch, a branching condition is checked to decide whether to explore the next branch. In this particular instance
the visit condition will check if the visit of the first branch lead to a closed tableau. If this is the case, the second branch is explored. Otherwise
a result of an open branch is immediately returned.
EXERCISE: Consider the variant Or-rule below:
```
RULE Or-wrong
A v B
======================
A | B
END
```

How does it differ from the previous Or-rule, and more importantly, is it semantically sound given our
usual interpretation of the classical disjunction?
===Strategy===
` STRATEGY := tactic ( (Id ! False ! And ! Or)* ) `

===Operators===
```
PP := List.map nnf
NEG := List.map neg
MAIN
```

The '''PP''' directive defines a PreProcessor as indicated by the function to the right of the := sign.
If '''PP''' is defined then the TWB first uses this preprocessor on all input formulae.
The '''NEG''' directive defines a NEGation function as indicated by the function to the right of the := sign.
By default, the TWB NEGates all input formulae using this function.
The preprocessor '''PP''' is invoked ''*after*'' the NEGation function so the directives in this case tell the TWB to NEGate all inputs, and then put the result into nnf by pushing negations down to atomic level.
The MAIN directive just tells the TWB to link the default command line application to the prover. In principle it would be possible to specify different routine, for example to run the prover as a cgi from the web. This is still work in progress.
```
CONNECTIVES [ "~" ; "&" ; "v" ; "->" ; "<->" ; "=>"]
GRAMMAR
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| ~ formula
;;
expr := formula ;;
node := set => set ;;
END
SEQUENT
RULE Id Close === { A } => { A } END
RULE False Close === { Falsum } => END
RULE True Close === => { Verum } END
RULE AndL A ; B => === { A & B } => END
RULE AndR => A | => B === => { A & B } END
RULE OrL A => | B => === { A v B } => END
RULE OrR => A ; B === => { A v B } END
RULE NegR A => === => { ~ A } END
RULE NegL => A === { ~ A } => END
RULE ImpL => A | B => === { A -> B } => END
RULE ImpR A => B === => { A -> B } END
RULE IffL (A -> B) & (B -> A) => === { A <-> B } => END
RULE IffR => (A -> B) & (B -> A) === => { A <-> B } END
END
let exit = function
|"Open" -> "Not Derivable"
|"Close" -> "Derivable"
|s -> assert(false)
EXIT := exit(status@1)
STRATEGY := tactic ( ( Id
! True ! False
! NegL ! NegR
! AndL ! AndR
! ImpL ! ImpR
! OrL ! OrR
! IffL ! IffR )* )
MAIN
```

```
source Pc
let neg = function formula ( a ) -> formula ( ~ a )
let rec nnf = function
|formula ( a & b ) -> formula ( {nnf a} & {nnf b} )
|formula ( ~ ( a & b ) ) ->
formula ( {nnf formula ( ~ a )} v {nnf formula ( ~ b )} )
|formula ( a v b ) -> formula ({nnf a} v {nnf b})
|formula ( ~ ( a v b ) ) ->
formula ( {nnf formula ( ~ a )} & {nnf formula ( ~ b )} )
|formula ( a <-> b ) ->
formula ( {nnf formula ( a -> b )} & {nnf formula ( b -> a )} )
|formula ( ~ ( a <-> b ) ) ->
formula ( {nnf formula ( ~ (a -> b) )} v {nnf formula ( ~ (b -> a) )} )
|formula ( a -> b ) -> nnf formula ( (~ a) v b )
|formula ( ~ (a -> b) ) -> nnf formula ( a & (~ b) )
|formula ( ~ ~ a ) -> nnf a
|formula (Verum) -> formula (Verum)
|formula (Falsum) -> formula (Falsum)
|formula (~ Verum) -> formula (Falsum)
|formula (~ Falsum) -> formula (Verum)
|formula ( ~ A ) as f -> f
| _ as f -> f
```

We assume this function to be in a file pclib.ml. The file is then included in the the main logic module by
using the directive `Open Pclib`

.