Linear and Nonlinear Arithmetic in ACL2
Authors:
Open Access
- 1 January 2003
- book chapter
- Published by Springer Nature in Lecture Notes in Computer Science
- p. 319-333
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- ACL2: an industrial strength version of Nqthm2002
- Combining Shostak Theories2002
- A Rewrite Rule Based Framework for Combining Decision Procedures *Lecture Notes in Computer Science, 2002
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ ProcessorLMS Journal of Computation and Mathematics, 1998
- Verifying the accuracy of polynomial approximations in HOL1997
- Verification of IEEE compliant subtractive division algorithms1996
- Deciding Combinations of TheoriesJournal of the ACM, 1984