unicode_fol_kit.to_dnf¶
- unicode_fol_kit.to_dnf(node)[source]¶
Return prenex form whose matrix is a disjunction of conjunctive clauses.
The dual of
to_cnf(): reuse the prenex prefix fromto_pnfand distribute ∧ over ∨ in the quantifier-free matrix (each conjunctive clause is a conjunction of literals). Equivalence-preserving.