Zammit, Vincent (1996) A Mechanisation of Computability Theory in HOL. In: von Wright, Joakim and Grundy, Jim and Harrison, John, eds. Theorem Proving in Higher Order Logics 9th International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 431446. ISBN 9783540615873. EISBN 9783540706410. (doi:10.1007/BFb0105420) (KAR id:21347)
PDF
Language: English 

Download (423kB)
Preview



Postscript
Language: English 

Download (211kB)
Preview



Official URL http://dx.doi.org/10.1007/BFb0105420 
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.
Item Type:  Book section 

DOI/Identification number:  10.1007/BFb0105420 
Uncontrolled keywords:  Computability Theory, URM, Theorem Proving, Formalization of Mathematics 
Subjects:  Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, 
Divisions:  Faculties > Sciences > School of Computing > Theoretical Computing Group 
Depositing User:  Mark Wheadon 
Date Deposited:  27 Aug 2009 18:44 UTC 
Last Modified:  31 May 2019 09:19 UTC 
Resource URI:  https://kar.kent.ac.uk/id/eprint/21347 (The current URI for this page, for reference purposes) 
 Export to:
 RefWorks
 EPrints3 XML
 BibTeX
 CSV
 Depositors only (login required):