Trustworthy Systems

A formalisation of the normal forms of context-free grammars in HOL4

Authors

Aditi Barthwal and Michael Norrish

Australian National University

NICTA

Abstract

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.

BibTeX Entry

  @inproceedings{Barthwal_Norrish_10_2,
    address          = {Brno, Czech Republic},
    author           = {Barthwal, Aditi and Norrish, Michael},
    booktitle        = {19th EACSL Annual Conferences on Computer Science Logic},
    keywords         = {theorem-proving, language theory},
    month            = aug,
    pages            = {95--109},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/3885.pdf},
    title            = {A Formalisation of the Normal Forms of Context-Free Grammars in {HOL4}},
    year             = {2010}
  }

Download