Integrating External Deduction Tools with ACL2
M. Kaufmann, J S. Moore, S. Ray, and E. Reeber
In C. Benzmüller, B. Fischer, and G. Sutcliffe, editors, Proceedings
of the 6th
International Workshop on the Implementation of Logics (IWIL 2006), Phnom
Penh, Cambodia, November 2006, volume 212 of CEUR
Workshop Proceedings, pages 7-26.
Abstract
We present an interface connecting the ACL2 theorem prover with external
deduction tools. The logic of ACL2 contains several constructs intended to
facilitate structuring of interactive proof development, which complicates the
design of such an interface. We discuss some of these complexities and develop
a precise specification of the requirements from external tools for sound
connection with ACL2. We also develop constructs within ACL2 to enable the
developers of external tools to satisfy our specifications.
Relevant files
- Paper (ps, pdf)
- Presentation for IWIL 2006 (ppt, pdf)
[Note: The original slides were made in powerpoint with
audio so as to enable remote video presentation, since I could not
attend the workshop personally. However, I remove the audio from the
powerpoint here to facilitate download.]
BibTex
@Inproceedings{kaufmann-integrating,
title = "{Integrating External Deduction Tools with ACL2}",
author = "M. Kaufmann and J S. Moore and S. Ray and E. Reeber",
booktitle = "{Proceedings of the $6$th International Workshop on Implementation of
Logics (IWIL 2006)}",
editor = "C. {Benzm\"uller} and B. Fischer and G. Sutcliffe",
year = "2006",
month = nov,
address = "{Phnom Penh, Cambodia}",
series = "{CEUR Workshop Proceedings}",
volume = "212",
pages = "7-26"
}