Skip navigation
Skip navigation

A formalisation of the theory of context-free languages in higher order logic

Barthwal, Aditi


We present a formalisation of the theory of context-free languages using the HOL4 theorem prover. The formalisation of this theory is not only interesting in its own right, but also gives insight into the kind of manipulations required to port a pen-and-paper proof to a theorem prover. The mechanisation proves to be an ideal case study of how intuitive textbook proofs can blow up in size and complexity, and how details from the textbook can change during formalisation. The mechanised...[Show more]

CollectionsOpen Access Theses
Date published: 2010-12
Type: Thesis (PhD)


File Description SizeFormat Image
Barthwal Thesis 2010.pdf863.51 kBAdobe PDFThumbnail

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