Email Gateway (Jun 16 2026 at 15:55): Email Gateway (Jun 16 2026 at 15:55):From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] New in the AFP: A Formalization of the Exponential Blowup in the Transformations between CNF and DNF
A Formalization of the Exponential Blowup in the Transformations between CNF and DNF
Leon Raffael Schulz, Martin Desharnais-Schäfer and Jan Johannsen
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.
https://isa-afp.org/entries/CNF_DNF_Exp_Blowup.html
Last updated: Jul 02 2026 at 07:34 UTC