HOLyHammer

HOL(y)Hammer: online ATP service for HOL Light. HOL(y)Hammer is an online AI/ATP service for formal (computer-understandable) mathematics encoded in the HOL Light system. The service allows its users to upload and automatically process an arbitrary formal development (project) based on HOL Light, and to attack arbitrary conjectures that use the concepts defined in some of the uploaded projects. For that, the service uses several automated reasoning systems combined with several premise selection methods trained on all the project proofs. The projects that are readily available on the server for such query answering include the recent versions of the Flyspeck, Multivariate Analysis and Complex Analysis libraries. The service runs on a 48-CPU server, currently employing in parallel for each task 7 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 and their solutions are discussed, and an initial account of using the system is given.


References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Kohlhase, Michael; Müller, Dennis; Owre, Sam; Rabe, Florian: Making PVS accessible to generic services by interpretation in a universal format (2017)
  2. Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
  3. Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef: A learning-based fact selector for Isabelle/HOL (2016)
  4. Benzmüller, Christoph; Woltzenlogel Paleo, Bruno: Higher-order modal logics: automation and applications (2015)
  5. Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias: Mining the Archive of Formal Proofs (2015)
  6. Färber, Michael; Kaliszyk, Cezary: Random forests for premise selection (2015)
  7. Gauthier, Thibault; Kaliszyk, Cezary: Sharing HOL4 and HOL light proof knowledge (2015)
  8. Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
  9. Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
  10. Kaliszyk, Cezary; Urban, Josef: MizAR 40 for Mizar 40 (2015)
  11. Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
  12. Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène: Formalizing physics: automation, presentation and foundation issues (2015)
  13. Gauthier, Thibault; Kaliszyk, Cezary: Matching concepts across HOL libraries (2014)
  14. Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman: Developing corpus-based translation methods between informal and formal mathematics: project description (2014)