The negation normal form function is written in the TWB as the following Ocaml function:
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.