Integrating external deduction tools with ACL2

2Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.
Get full text

Abstract

We present an interface connecting the ACL2 theorem prover with external deduction tools. The ACL2 logic contains several mechanisms for proof structuring, which are important to the construction of industrial-scale proofs. The complexity induced by these mechanisms makes the design of the interface challenging. We discuss some of the challenges, and develop a precise specification of the requirements on the external tools for a sound connection with ACL2. We also develop constructs within ACL2 to enable the developers of external tools to satisfy our specifications. The interface is available with the ACL2 theorem prover starting from Version 3.2, and we describe several applications of the interface. © 2007 Elsevier Inc. All rights reserved.

Cite

CITATION STYLE

APA

Kaufmann, M., Moore, J. S., Ray, S., & Reeber, E. (2006). Integrating external deduction tools with ACL2. In CEUR Workshop Proceedings (Vol. 212, pp. 24–43). https://doi.org/10.1016/j.jal.2007.07.002

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