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.


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


  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"