Sciweavers

CHARME
2003
Springer

Linear and Nonlinear Arithmetic in ACL2

13 years 8 months ago
Linear and Nonlinear Arithmetic in ACL2
Abstract. As of version 2.7, the ACL2 theorem prover has been extended to automatically verify sets of polynomial inequalities that include nonlinear relationships. In this paper we describe our mechanization of linear and nonlinear arithmetic in ACL2. The nonlinear arithmetic procedure operates in cooperation with the pre-existing ACL2 linear arithmetic decision procedure. It extends what can be automatically verified with ACL2, thereby eliminating the need for certain types of rules in ACL2’s database while simultaneously increasing the performance of the ACL2 system when verifying arithmetic conjectures. The resulting system lessens the human effort required to construct a large arithmetic proof by reducing the number of intermediate lemmas that must be proven to verify a desired theorem.
Warren A. Hunt Jr., Robert Bellarmine Krug, J. Str
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where CHARME
Authors Warren A. Hunt Jr., Robert Bellarmine Krug, J. Strother Moore
Comments (0)