Fourier Series Formalization in ACL2(r)
We formalize some basic properties of Fourier series in the logic of ACL2(r), which is a variant of ACL2 that supports reasoning about the real and complex numbers by way of non-standard analysis. More specifically, we extend a framework for formally evaluating definite integrals of real-valued, con...
Main Authors: | Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr. |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2015-09-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1509.06087v1 |
Similar Items
-
How Can I Do That with ACL2? Recent Enhancements to ACL2
by: Matt Kaufmann, et al.
Published: (2011-10-01) -
Industrial-Strength Documentation for ACL2
by: Jared Davis, et al.
Published: (2014-06-01) -
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
by: Matt Kaufmann, et al.
Published: (2014-06-01) -
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1
by: Matt Kaufmann, et al.
Published: (2013-04-01) -
Convex Functions in ACL2(r)
by: Carl Kwan, et al.
Published: (2018-10-01)