Email Gateway (Sep 24 2026 at 12:13): Email Gateway (Sep 24 2026 at 12:13):From: Tobias Nipkow <nipkow@in.tum.de>
Subject: [isabelle] New in the AFP: Deterministic Context-Free Languages are Closed Under Complementation
Deterministic Context-Free Languages are Closed Under Complementation (Hopcroft
and Ullman)
Kaan Taskin and Tobias Nipkow
A deterministic context-free language (DCFL) is a language accepted by a
deterministic pushdown automaton (DPDA). This entry proves that the
deterministic context-free languages are closed under complementation. The proof
follows the one in the book by Hopcroft and Ullman (1979).
https://isa-afp.org/entries/DPDA_Complement_HU.html
Enjoy!
Last updated: Oct 08 2026 at 21:07 UTC