School of Computing

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},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014