The University of New South Wales

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

Download