Initial experiments with TPTP-style automated theorem provers on ACL2 problems

2Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

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.

Cite

CITATION STYLE

APA

Joosten, S., Kaliszyk, C., & Urban, J. (2014). Initial experiments with TPTP-style automated theorem provers on ACL2 problems. In Electronic Proceedings in Theoretical Computer Science, EPTCS (Vol. 152, pp. 77–85). Open Publishing Association. https://doi.org/10.4204/EPTCS.152.6

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free