A Formalisation of the Normal Forms of Context-Free Grammars in HOL4

We describe the formalisation of the normal forms of context-free grammars (CFGs) using the HOL4 theorem prover. These straightforward pen and paper proofs easily understood from the text turn out to be much harder to mechanise. The informal observations in the text become deductive gaps for a theorem prover that need to be patched.

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: Aditi Barthwal, Michael Norrish
• Keywords: Automated Reasoning, Context-free Grammars, CSL 2010, Straightforward Pen, Theorem Prover