Real Number Calculations and Theorem Proving
From MaRDI portal
Publication:3543660
DOI10.1007/978-3-540-71067-7_19zbMath1165.68463OpenAlexW1586880486MaRDI QIDQ3543660
Publication date: 4 December 2008
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-71067-7_19
Related Items
A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem, Formal Verification of Exact Computations Using Newton’s Method, Formalization of real analysis: a survey of proof assistants and libraries, Formal proofs for theoretical properties of Newton's method
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Isabelle. A generic theorem prover
- Using PVS to validate the algorithms of an exact arithmetic.
- Computable functionals
- On the definition of computable functionals
- On the definitions of computable real continuous functions
- Affine functions and series with co-inductive real numbers
- Extending a Resolution Prover for Inequalities on Elementary Functions
- Numerical Software with Result Verification
- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
- Theorem Proving in Higher Order Logics
- On Computable Numbers, with an Application to the Entscheidungsproblem
- On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
