1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
\DOC CNF_CONV
\TYPE {CNF_CONV : conv}
\SYNOPSIS
Converts a term already in negation normal form into conjunctive normal form.
\DESCRIBE
When applied to a term already in negation normal form (see {NNF_CONV}),
meaning that all other propositional connectives have been eliminated in favour
of conjunction, disjunction and negation, and negation is only applied to
atomic formulas, {CNF_CONV} puts the term into an equivalent conjunctive normal
form, which is a right-associated conjunction of disjunctions without
repetitions. No reduction by subsumption is performed, however, e.g. from
{a /\ (a \/ b)} to just {a}).
\FAILURE
Never fails; non-Boolean terms will just yield a reflexive theorem.
\EXAMPLE
{
# CNF_CONV `(a /\ b) \/ (a /\ b /\ c) \/ d`;;
val it : thm =
|- a /\ b \/ a /\ b /\ c \/ d <=>
(a \/ d) /\ (a \/ b \/ d) /\ (a \/ c \/ d) /\ (b \/ d) /\ (b \/ c \/ d)
}
\SEEALSO
DNF_CONV, NNF_CONV, WEAK_CNF_CONV, WEAK_DNF_CONV.
\ENDDOC
|
