Sciweavers

CHARME
2003
Springer
103views Hardware» more  CHARME 2003»
14 years 5 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 w...
Warren A. Hunt Jr., Robert Bellarmine Krug, J. Str...