Skip navigation
Skip navigation

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

Request a Copy

link to publisher version

  • Altmetric Citations

Barthwal, Aditi; Norrish, Michael

Description

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

dc.contributor.authorBarthwal, Aditi
dc.contributor.authorNorrish, Michael
dc.coverage.spatialBrasília Brazil
dc.date.accessioned2015-12-08T22:25:14Z
dc.date.createdJuly 16 2010
dc.identifier.isbn364215204X9783
dc.identifier.urihttp://hdl.handle.net/1885/33365
dc.description.abstractWe 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
dc.publisherSpringer
dc.relation.ispartofseriesWorkshop on Logic, Language, Information and Computation (WoLLIC 2010)
dc.sourceWoLLIC 2010 proceedings
dc.subjectKeywords: Blow-up; Formalisation; Greibach normal forms; Informal presentation; Normal form; Theorem provers; Computer science; Context free grammars; Technical presentations
dc.titleA Formalisation of the Normal Forms of Context-Free Grammars in HOL4
dc.typeConference paper
local.description.notesImported from ARIES
local.description.refereedYes
dc.date.issued2010
local.identifier.absfor080199 - Artificial Intelligence and Image Processing not elsewhere classified
local.identifier.ariespublicationu4963866xPUB101
local.type.statusPublished Version
local.contributor.affiliationBarthwal, Aditi, College of Engineering and Computer Science, ANU
local.contributor.affiliationNorrish, Michael, College of Engineering and Computer Science, ANU
local.description.embargo2037-12-31
local.bibliographicCitation.startpage15
local.identifier.doi10.1007/978-3-642-15205-4_11
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
dc.date.updated2016-02-24T11:29:44Z
local.identifier.scopusID2-s2.0-77956601990
CollectionsANU Research Publications

Download

File Description SizeFormat Image
01_Barthwal_A_Formalisation_of_the_Normal_2010.pdf144.07 kBAdobe PDF    Request a copy
Show simple item record


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator