TY - GEN
T1 - A formalisation of the normal forms of context-free grammars in HOL4
AU - Barthwal, Aditi
AU - Norrish, Michael
PY - 2010
Y1 - 2010
N2 - We describe the formalisation of the Chomsky and Greibach normal forms for context-free grammars (CFGs) using the HOL4 theorem prover. We discuss the varying degrees to which proofs that are straightforward on pen and paper, turn out to be much harder to mechanise. While both proofs are of similar length in their informal presentations, the mechanised proofs for Greibach normal form blow-up considerably.
AB - We describe the formalisation of the Chomsky and Greibach normal forms for context-free grammars (CFGs) using the HOL4 theorem prover. We discuss the varying degrees to which proofs that are straightforward on pen and paper, turn out to be much harder to mechanise. While both proofs are of similar length in their informal presentations, the mechanised proofs for Greibach normal form blow-up considerably.
UR - http://www.scopus.com/inward/record.url?scp=77956601990&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-15205-4_11
DO - 10.1007/978-3-642-15205-4_11
M3 - Conference contribution
SN - 364215204X
SN - 9783642152047
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 95
EP - 109
BT - Computer Science Logic - 24th International Workshop, CSL 2010, and 19th Annual Conference of the EACSL, Proceedings
T2 - 24th International Workshop on Computer Science Logic, CSL 2010, and 19th Annual Conference of the EACSL
Y2 - 23 August 2010 through 27 August 2010
ER -