Mechanisation of PDA and grammar equivalence for context-free languages

Aditi Barthwal; Michael Norrish

doi:10.1007/978-3-642-13824-9_11

Mechanisation of PDA and grammar equivalence for context-free languages

Aditi Barthwal^*, Michael Norrish

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

5 Citations (Scopus)

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.

Original language	English
Title of host publication	Logic, Language, Information and Computation - 17th International Workshop, WoLLIC 2010, Proceedings
Pages	125-135
Number of pages	11
DOIs	https://doi.org/10.1007/978-3-642-13824-9_11
Publication status	Published - 2010
Event	17th International Workshop on Logic, Language, Information and Computation, WoLLIC 2010 - Brasilia, Brazil Duration: 6 Jul 2010 → 9 Jul 2010

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6188 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	17th International Workshop on Logic, Language, Information and Computation, WoLLIC 2010
Country/Territory	Brazil
City	Brasilia
Period	6/07/10 → 9/07/10

Access to Document

10.1007/978-3-642-13824-9_11

Cite this

Barthwal, A., & Norrish, M. (2010). Mechanisation of PDA and grammar equivalence for context-free languages. In Logic, Language, Information and Computation - 17th International Workshop, WoLLIC 2010, Proceedings (pp. 125-135). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6188 LNAI). https://doi.org/10.1007/978-3-642-13824-9_11

@inproceedings{6ced02bdc7ce49f982a85eb8eecb4951,

title = "Mechanisation of PDA and grammar equivalence for context-free languages",

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.",

author = "Aditi Barthwal and Michael Norrish",

year = "2010",

doi = "10.1007/978-3-642-13824-9\_11",

language = "English",

isbn = "3642138233",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "125--135",

booktitle = "Logic, Language, Information and Computation - 17th International Workshop, WoLLIC 2010, Proceedings",

note = "17th International Workshop on Logic, Language, Information and Computation, WoLLIC 2010 ; Conference date: 06-07-2010 Through 09-07-2010",

}

Barthwal, A & Norrish, M 2010, Mechanisation of PDA and grammar equivalence for context-free languages. in Logic, Language, Information and Computation - 17th International Workshop, WoLLIC 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6188 LNAI, pp. 125-135, 17th International Workshop on Logic, Language, Information and Computation, WoLLIC 2010, Brasilia, Brazil, 6/07/10. https://doi.org/10.1007/978-3-642-13824-9_11

Mechanisation of PDA and grammar equivalence for context-free languages. / Barthwal, Aditi; Norrish, Michael.
Logic, Language, Information and Computation - 17th International Workshop, WoLLIC 2010, Proceedings. 2010. p. 125-135 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6188 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

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 Paper

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 -

Barthwal A, Norrish M. Mechanisation of PDA and grammar equivalence for context-free languages. In Logic, Language, Information and Computation - 17th International Workshop, WoLLIC 2010, Proceedings. 2010. p. 125-135. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-13824-9_11

Mechanisation of PDA and grammar equivalence for context-free languages

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this