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
Type: Thesis (PhD)
DOI: 10.25911/5d6e4c3c4b543


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:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator