Inverse functions in ACL2(r)
| Autor: | Ruben Gamboa, John Cowles |
|---|---|
| Rok vydání: | 2009 |
| Předmět: |
Inverse function theorem
Generalized inverse Continuous function Computer science Inverse functions and differentiation Inverse hyperbolic function Natural logarithm Square root Inverse element Multiplicative inverse Applied mathematics Inverse trigonometric functions Quantum inverse scattering method Inverse function Integral of inverse functions |
| Zdroj: | Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications. |
| DOI: | 10.1145/1637837.1637846 |
| Popis: | ACL2(r) supports the definition of real-valued functions. In this paper, we introduce a theory of inverse functions into ACL2(r). The theory is developed in stages, from an abstract description of inverse functions, to a still abstract but more tractable treatment of the inverse of continuous functions. A macro is introduced to simplify the introduction of concrete inverse functions. We illustrate the approach by defining some inverse functions in ACL2, including the square root, natural logarithm, inverse sine, and inverse cosine functions. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|