Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
Artificial Intelligence
2014-06-09 v1 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.1406.1559,
title = {Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems},
author = {Sebastiaan Joosten and Cezary Kaliszyk and Josef Urban},
journal= {arXiv preprint arXiv:1406.1559},
year = {2014}
}
Comments
In Proceedings ACL2 2014, arXiv:1406.1238