On the Automation of Inductive Proofs in HOL Light

Abstract In this project we investigate the potential of an automated system for inductive proofs within the HOL Light proof assistant. The system is based on the waterfall model described by Boyer and Moore over 30 years ago. We investigate the potential of this model by analysing an implementation originally made in the HOL88/90 systems, reconstructing it in HOL Light, and creating several additions and enhancements. We then evaluate the system using a large list of known,inductive theorems. Our work promotes the use of this system as an automated tactic for inductive proofs in an interactive setting. We conclude with a number,of suggestions for future development. iii Acknowledgements