Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems

Sebastiaan Joosten, Cezary Kaliszyk, and Josef Urban

Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014), Electronic Proceedings in Theoretical Computer Science 152, pp. 77 – 85, 2014.


This paper reports our initial experiments with using external ATP on some corpora built with the ACL2 system. This is intended to provide the first estimate about the usefulness of such external reasoning and AI systems for solving ACL2 problems.


  PDF |    doi:10.4204/EPTCS.152.6  |  © Creative Commons License


author = "Sebastiaan Joosten and Cezary Kaliszyk and Josef Urban",
title = "Initial Experiments with {TPTP}-style Automated Theorem Provers on
{ACL2} Problems",
booktitle = "Proceedings of the 12th International Workshop on the
{ACL2} Theorem Prover and its Applications",
editor = "Freek Verbeek and Julien Schmaltz",
series = "Electronic Proceedings in Theoretical Computer Science",
volume = 152,
pages = "77--85",
year = 2014,
doi = "10.4204/EPTCS.152.6"
Nach oben scrollen