Abstract This paper describes a mechanisation of computability the ory in HOL using the Unlimited Register Machine URM model of com putation The URM model is rst specied 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 num ber of functions are then proved to be computable This work forms part of a comparative study of dierent theorem proving approaches and a brief discussion regarding theorem proving in HOL follows...
Add to ORKG