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

2014/06/04 by Sebastiaan Joosten, Cezary Kaliszyk, Josef Urban · 2 citations
Computer Science · #Algebra over a field #Automated proof checking #Automated reasoning #Automated theorem proving #Calculus (dental) #Logic, Reasoning, and Knowledge #Natural Language Processing Techniques #Speech and dialogue systems #cs.AI #cs.LO

paper · pdf · doi:10.4204/eptcs.152.6

published in Electronic Proceedings in Theoretical Computer Science 152, 77-85 (Open Publishing Association) · In Proceedings ACL2 2014, arXiv:1406.1238

openalex publication_date 2014/06/04 · arxiv created 2014/06/06 · arxiv updated 2014/06/09 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/05

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.

Citations

• Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications