Skip navigation
Skip navigation

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

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

CollectionsANU Research Publications
Date published: 2010
Type: Conference paper
URI: http://hdl.handle.net/1885/33365
Source: WoLLIC 2010 proceedings
DOI: 10.1007/978-3-642-15205-4_11

Download

File Description SizeFormat Image
01_Barthwal_A_Formalisation_of_the_Normal_2010.pdf144.07 kBAdobe PDF    Request a copy


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

Updated:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator