The conversion NNF_CONV proves a term equal to an equivalent in `negation
normal form' (NNF). This means that other propositional connectives are
eliminated in favour of conjunction (`/\'), disjunction (`\/') and negation
(`~'), and the negations are pushed down to the level of atomic formulas,
also through universal and existential quantifiers, with double negations
eliminated.
FAILURE CONDITIONS
Never fails; on non-Boolean terms it just returns a reflexive theorem.
EXAMPLE
# NNF_CONV `(!x. p(x) <=> q(x)) ==> ~ ?y. p(y) /\ ~q(y)`;;
Warning: inventing type variables
val it : thm =
|- (!x. p x <=> q x) ==> ~(?y. p y /\ ~q y) <=>
(?x. p x /\ ~q x \/ ~p x /\ q x) \/ (!y. ~p y \/ q y)
USES
Mostly useful as a prelude to automated proof procedures, but users may
sometimes find it useful.
COMMENTS
A toplevel equivalence p <=> q is converted to (p /\ q) \/ (~p /\ ~q). In
general this ``splitting'' of equivalences is done with the expectation that
the final formula may be put into disjunctive normal form (DNF), as a prelude
to a refutation procedure. An otherwise similar conversion NNFC_CONV prefers
a `conjunctive' splitting and is better suited for a term that will later be
translated to CNF.