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

Joosten, Sebastiaan; Kaliszyk, Cezary; Urban, Josef

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

Sebastiaan Joosten
(Technical University of Eindhoven/Radboud University Nijmegen)

Cezary Kaliszyk
(University of Innsbruck)

Josef Urban
(Radboud University Nijmegen)

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.

In Freek Verbeek and Julien Schmaltz: Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014), Vienna, Austria, 12-13th July 2014, Electronic Proceedings in Theoretical Computer Science 152, pp. 77–85.
Published: 4th June 2014.

ArXived at: https://dx.doi.org/10.4204/EPTCS.152.6	bibtex	PDF

References in reconstructed bibtex, XML and HTML format (approximated).

Comments and questions to:

eptcs@eptcs.org

For website issues:

webmaster@eptcs.org