Real Number Calculations and Theorem Proving

DOI10.1007/978-3-540-71067-7_19MaRDI QIDQ3543660zbMATH OpenOpenAlexFDO

Authors David R. Lester

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

zbMATH Keywords

computable realsexact arithmetichigher-order logicPVStheorem proving

Mathematics Subject Classification ID

Recommendations

• Theorem Proving in Higher Order Logics
• Using PVS to validate the algorithms of an exact arithmetic.
• scientific article; zbMATH DE number 1259143
• The world's shortest correct exact real arithmetic program?
• Applications of real number theorem proving in PVS

Cites work

• Affine functions and series with co-inductive real numbers
• Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
• Computable functionals
• Extending a Resolution Prover for Inequalities on Elementary Functions
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• scientific article; zbMATH DE number 3735125 (Why is no real title available?)
• scientific article; zbMATH DE number 42077 (Why is no real title available?)
• Isabelle. A generic theorem prover
• Numerical Software with Result Verification
• On Computable Numbers, with an Application to the Entscheidungsproblem
• On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
• On the definition of computable functionals
• On the definitions of computable real continuous functions
• Theorem Proving in Higher Order Logics
• Using PVS to validate the algorithms of an exact arithmetic.

Cited in

(14)

• Real number computations: On the use of information
• Using PVS to validate the algorithms of an exact arithmetic.
• A validated real function calculus
• Exact real arithmetic for interval number systems
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• Digital look up tables and real number theorem proving
• Formalization of real analysis: a survey of proof assistants and libraries
• Formal proofs for theoretical properties of Newton's method
• Formal Verification of Exact Computations Using Newton’s Method
• scientific article; zbMATH DE number 1259143 (Why is no real title available?)
• Validating Brouwer's continuity principle for numbers using named exceptions
• Applications of real number theorem proving in PVS
• Numerical Software with Result Verification
• Theorem Proving in Higher Order Logics

Describes a project that uses

Uses Software

• HOL Light
• PVS

This page was built for publication: Real Number Calculations and Theorem Proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3543660)