Support for ``Trusted'' Extension in ACL2

J Strother Moore

Abstract: Trust in the soundness of the core ACL2 theorem prover is based
entirely on the care the authors (Kaufmann and Moore) have taken in coding
it.  It does not construct a formal proof object or offer any other artifact
witnessing the correctness of an alleged deduction.  However, the core can be
extended by the user in many ways, without risking (``new'') unsoundness.
Two kinds of extensions are discussed: those that change the logical theory
and those that affect the behavior of the system.  We briefly present many of
the extension features, including definitional extension, introduction of
constrained functions, a powerful macro facility, automatic use of rewrite
rules derived from theorems, verified metafunctions and provers, methods of
speeding up function execution, and exploiting fact that the system is
implemented in the language supported by the theorem prover.