We present a formalisation of the theory of context-free languages using the HOL4
theorem prover. The formalisation of this theory is not only interesting in its own right,
but also gives insight into the kind of manipulations required to port a pen-and-paper
proof to a theorem prover. The mechanisation proves to be an ideal case study of how
intuitive textbook proofs can blow up in size and complexity, and how details from the
textbook can change during formalisation.
The mechanised...[Show more]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.