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

TL;DR

This paper presents initial experiments with external automated theorem provers on ACL2 problems to evaluate their effectiveness in aiding formal reasoning tasks.

Contribution

It provides the first assessment of the usefulness of external ATP systems for solving ACL2 problems.

Findings

External ATP systems show potential in solving ACL2 problems.

Initial experiments indicate some success in automated reasoning for ACL2.

Results suggest further research could improve integration and performance.

Abstract

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.