cl-banner

Initial Experiments with External Provers and Premise Selection on HOL Light Corpora

Cezary Kaliszyk and Josef Urban

Proceedings of the 3rd Workshop on Practical Aspects of Automated Reasoning (PAAR 2012), EasyChair Proceedings in Computing 21, pp. 72 – 81, 2013.

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.

 

  PDF

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
}
Nach oben scrollen