Index of Logic Forms

Logic forms

• CNF

• DNF

• NNF

• implicative normal form INF

• Skolem normal form

• prenex normal form

Canonical forms:

• CDNF Canonical Disjunctive Normal Form

• CCNF Canonical Conjunctive Normal Form

• ANF Algebraic Normal Form

• BCF Blake Canonical Form

• complete sum of prime implicants

An implicative normal form is the conjunction of a set of implications, each of which has a conjunction of terms on the left and a disjunction of terms on the right, ⋀[⋀(a✻) -> ⋁(s✻)]✻, like a conjunction of sequents, ⋀(a|-s)*. A nice property of classical FOL is that a formula can be reduced to INF through a series of syntactic simplifications.