Trustworthy Systems

Beagle as a HOL4 external ATP method

Authors

Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish

University of Innsbruck

INRIA
France

NICTA

Australian National University

Abstract

This paper presents BEAGLE_TAC, a HOL4 tactic for using Beagle as an external ATP for discharging HOL4 goals. We implement a translation of the higher-order goals to the TFA format of TPTP and add trace output to Beagle to reconstruct the intermediate steps derived by the ATP in HOL4. Our translation combines the characteristics of existing successful translations from HOL to FOL and SMT-LIB, however we needed to adapt certain stages of the translation in order to benefit form the expressiveness of the TFA format and the power of Beagle. In our initial experiments, we demonstrate that our system can prove, without any arithmetic lemmas, 81% of the goals solved by Metis.

BibTeX Entry

  @inproceedings{Gauthier_KKN_14,
    address          = {Vienna},
    author           = {Gauthier, Thibault and Kaliszyk, Cezary and Keller, Chantal and Norrish, Michael},
    booktitle        = {Practical Aspects of Automated Reasoning},
    editor           = {{Stephan Schulz and Leonardo De Moura and Boris Konev}},
    month            = jul,
    pages            = {50--59},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8108.pdf},
    publisher        = {EasyChair Proceedings in Computing},
    title            = {Beagle as a {HOL4} external {ATP} method},
    year             = {2014}
  }

Download