ACL2

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

• Type: Conference
• Year: 2006
• Where: TPHOL
• Authors: Ruben Gamboa
• Keywords: ACL2, ACL2’s Numeric System, Artificial Intelligence, Complex Numbers, TPHOL 2006