Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

19

TPHOL
2006
IEEE

favoriteEmaildiscussreport

131views Automated Reasoning» more TPHOL 2006»

ACL2

13 years 11 months ago

Download www.cs.uwyo.edu

This case study shows how ACL2 can be used to reason about the real and complex numbers, using non-standard analysis. It describes some modiﬁcations to ACL2 that include the irrational real and complex numbers in ACL2’s numeric system. It then shows how the modiﬁed ACL2 can prove classic theorems of analysis, such as the intermediate-value and mean-value theorems.

Ruben Gamboa

Real-time Traffic

ACL2 | ACL2’s Numeric System | Artificial Intelligence | Complex Numbers | TPHOL 2006 |

claim paper

Related Content

» ACL2s The ACL2 Sedan

» Towards a formal theory of on chip communications in the ACL2 logic

» The ideal of verified software

» ACL2 in DrScheme

» Theory Extension in ACL2r

» Implementing a costaware evaluator for ACL2 expressions

» Toward a Practical Module System for ACL2

» Linear and Nonlinear Arithmetic in ACL2

» A SATbased procedure for verifying finite state machines in ACL2

Post Info
More Details (n/a)

Added	12 Jun 2010
Updated	12 Jun 2010
Type	Conference
Year	2006
Where	TPHOL
Authors	Ruben Gamboa

Comments (0)