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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Hunt, W. A., Krug, R. B., & Moore, J. (2003). Linear and nonlinear arithmetic in ACL2. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2860, 319–333. https://doi.org/10.1007/978-3-540-39724-3_29
Mendeley helps you to discover research relevant for your work.