TY - GEN
T1 - Mechanisation of PDA and grammar equivalence for context-free languages
AU - Barthwal, Aditi
AU - Norrish, Michael
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=77955029239&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-13824-9_11
DO - 10.1007/978-3-642-13824-9_11
M3 - Conference contribution
SN - 3642138233
SN - 9783642138232
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 125
EP - 135
BT - Logic, Language, Information and Computation - 17th International Workshop, WoLLIC 2010, Proceedings
T2 - 17th International Workshop on Logic, Language, Information and Computation, WoLLIC 2010
Y2 - 6 July 2010 through 9 July 2010
ER -