Skip to Content

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

Posted on

Authors:

  • Joosten, Sebastiaan J. C.
  • Kaliszyk, Cezary
  • Urban, Josef

Published in: ACL2 Workhop pp 77–85

DOI: 10.4204/EPTCS.152.6

Paper

Slides

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.

BibTeX entry:

@inproceedings{Joosten14,
 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.},
 author = {Joosten, Sebastiaan Jozef Christiaan and Kaliszyk, Cezary and Urban, Josef},
 bdsk-url-1 = {https://doi.org/10.4204/EPTCS.152.6},
 booktitle = {ACL2 Workhop},
 doi = {10.4204/EPTCS.152.6},
 month = {Jul},
 pages = {77--85},
 title = {Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems},
 volume = {152},
 year = {2014}
}