Abstract
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. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Barthwal, A., & Norrish, M. (2010). Mechanisation of PDA and grammar equivalence for context-free languages. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6188 LNAI, pp. 125–135). https://doi.org/10.1007/978-3-642-13824-9_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
