A Formalization of the Exponential Blowup in the Transformations between CNF and DNF

Leon Raffael Schulz 📧, Martin Desharnais-Schäfer 📧 and Jan Johannsen 📧

June 15, 2026

Abstract

A well-known result about propositional logic is that transforming a formula into disjunctive or conjunctive normal form can lead to an exponential blowup of the formula size. We formalize this result in the form of two theorems and discuss the challenges we encountered.

License

BSD License

Topics

Related publications

  • Schulz, L. R. (2026). Formalisierung einer unteren Schranke an die Formelgröße in der Aussagenlogik mit Isabelle. Universitätsbibliothek Der Ludwig-Maximilians-Universität München. https://doi.org/10.5282/UBM/EPUB.135623
  • https://www.ifi.lmu.de/institut/personen/jjohannsen/jj_unpublished/skript.pdf

Session CNF_DNF_Exp_Blowup

Depends on

Cite

× 
@article{CNF_DNF_Exp_Blowup-AFP,
  author  = {Leon Raffael Schulz and Martin Desharnais-Schäfer and Jan Johannsen},
  title   = {A Formalization of the Exponential Blowup in the Transformations between CNF and DNF},
  journal = {Archive of Formal Proofs},
  month   = {June},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/CNF_DNF_Exp_Blowup.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download