Automated Reasoning Service for HOL Light

Cezary Kaliszyk and Josef Urban

Proceedings of the 6th Conference on Intelligent Computer Mathematics (CICM 2013), Lecture Notes in Computer Science 7961, pp. 120 – 135, 2013.


HOL(y)Hammer is an AI/ATP service for formal (computer-understandable) mathematics encoded in the HOL Light system, in particular for the users of the large Flyspeck library. The service uses several automated reasoning systems combined with several premise selection methods trained on previous Flyspeck proofs, to attack a new conjecture that uses the concepts defined in the Flyspeck library. The public online incarnation of the service runs on a 48-CPU server, currently employing in parallel for each task 25 AI/ATP combinations and 4 decision procedures that contribute to its overall performance. The system is also available for local installation by interested users, who can customize it for their own proof development. An Emacs interface allowing parallel asynchronous queries to the service is also provided. The overall structure of the service is outlined, problems that arise are discussed, and an initial account of using the system is given.


  PDF |    doi:10.1007/978-3-642-39320-4_8  |  © Springer


author = "Cezary Kaliszyk and Josef Urban",
title = "Automated Reasoning Service for {HOL} Light",
booktitle = "Proceedings of the 6th Conference on Intelligent Computer Mathematics",
editor = "Jacques Carette and David Aspinall and Christoph Lange and
Petr Sojka and Wolfgang Windsteiger",
series = "Lecture Notes in Computer Science",
volume = 7961,
pages = "120--135",
publisher = "Springer-Verlag",
year = 2013,
doi = "10.1007/978-3-642-39320-4_8"
Nach oben scrollen