Abstract

This paper reports our initial experiments with using external ATP and premise selection methods on some corpora built with the HOL Light system. The testing is done in three different settings, corresponding to those used earlier for evaluating such methods on the Mizar/MML corpus. This is intended to provide the first estimate about the usefulness of such external reasoning and AI systems for solving problems over HOL Light and its libraries.

BibTeX

@inproceedings{CKJU-PAAR12,
  author    = "Cezary Kaliszyk and Josef Urban",
  title     = "Initial Experiments with External Provers and Premise
               Selection on {HOL} Light Corpora",
  booktitle = "Proceedings of the 3rd Workshop on Practical Aspects of
               Automated Reasoning",
  series    = "EasyChair Proceedings in Computing",
  volume    = 21,
  pages     = "72--81",
  year      = 2013
}