Mechanisation of PDA and Grammar Equivalence for Context-Free Languages
Date
2010
Authors
Barthwal, Aditi
Norrish, Michael
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
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.
Description
Keywords
Keywords: Blow-up; Formalisation; Mechanisation; Push-down automata; Theorem provers; Automata theory; Linguistics; Machinery; Query languages; Context free languages
Citation
Collections
Source
WoLLIC 2010 proceedings
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31
Downloads
File
Description