Abstract
In this chapter we prove a few theorems to drive home the point that ACL2 is a mathematical logic rather than just a programming language. For use in our proofs, here are some of the theorems, axioms, and definitions mentioned above.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Notes
We increment the first component by 1 to insure that it is non-0, as required by e0-ordinalp.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media New York
About this chapter
Cite this chapter
Kaufmann, M., Manolios, P., Moore, J.S. (2000). Proof Examples. In: Computer-Aided Reasoning. Advances in Formal Methods, vol 3. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-4449-4_7
Download citation
DOI: https://doi.org/10.1007/978-1-4615-4449-4_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-7003-1
Online ISBN: 978-1-4615-4449-4
eBook Packages: Springer Book Archive