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

Select |




Print


Barthwal, Aditi; Norrish, Michael

Barthwal, Aditi; Norrish, Michael


2010-08-23


Conference Material


19th EACSL Annual Conferences on Computer Science Logic


Brno, Czech Republic


95-109


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


theorem-proving, language theory


http://mfcsl2010.fi.muni.cz/csl


nicta:3885


Barthwal, Aditi; Norrish, Michael. A Formalisation of the Normal Forms of Context-Free Grammars in HOL4. In: 19th EACSL Annual Conferences on Computer Science Logic; Brno, Czech Republic. 2010-08-23. 95-109.



Loading citation data...

Citation counts
(Requires subscription to view)