© University of Kent - Contact | Feedback | Legal | FOI | Cookies
A mechanisation of computability theory in HOL
Vincent Zammit
In J. von Wright, J. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 182-196, Turku, Finland, August 1996. Springer-Verlag.Abstract
This paper describes a mechanisation of computability theory in HOL using the Unlimited Register Machine (URM) model of computation. The URM model is first specified as a rudimentary machine language and then the notion of a computable function is derived. This is followed by an illustration of the proof of a number of basic results of computability which include various closure properties of computable functions. These are used in the implementation of a mechanism which partly automates the proof of the computability of functions and a number of functions are then proved to be computable. This work forms part of a comparative study of different theorem proving approaches and a brief discussion regarding theorem proving in HOL follows the description of the mechanisation.
Download publication 206 kbytes (PostScript)Bibtex Record
@inproceedings{328, author = {Vincent Zammit}, title = {A Mechanisation of Computability Theory in {H}{O}{L}}, month = {August}, year = {1996}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {}, doi = {}, url = {http://www.cs.kent.ac.uk/pubs/1996/328}, ISBN = {3-540-61587-3}, ISSN = {0302-9743}, address = {Turku, Finland}, booktitle = {Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics}, editor = {J. von Wright and J. Grundy and J. Harrison}, publisher = {Springer-Verlag}, refereed = {yes}, series = {Lecture Notes in Computer Science}, volume = {1125}, }