Sciweavers

Share
WOLLIC
2010
Springer

Mechanisation of PDA and Grammar Equivalence for Context-Free Languages

10 years 11 months ago
Mechanisation of PDA and Grammar Equivalence for Context-Free Languages
We provide a formalisation of the theory of pushdown automata (PDAs) using the HOL4 theorem prover. It illustrates how provers such as HOL can be used for mechanising complicated proofs, but also how intensive such a process can turn out to be. The proofs blow up in size in way difficult to predict from examining original textbook presentations. Even a meticulous text proof has “intuitive” leaps that need to be identified and formalised.
Aditi Barthwal, Michael Norrish
Added 31 Jan 2011
Updated 31 Jan 2011
Type Journal
Year 2010
Where WOLLIC
Authors Aditi Barthwal, Michael Norrish
Comments (0)
books