Disjunctive Normal Form (DNF) is the form into which each Cyc assertion or query can be recast at the HL level. This is most salient for Cyc with respect to queries, as each query is translated into its disjunctive normal form prior to looking for bindings to the variables in the queries. For non-logicians: this form is a disjunctive sentence all of whose disjuncts are conjunctive sentences. (In the trivial case, an atomic formula, say p, is considered a disjunction with just one disjunct — that disjunct being a conjunction with just one conjunct.) Cf. Conjunctive Normal Form (CNF).
