Verified interactive computation of definite integrals
From MaRDI portal
Recommendations
- Formally verified approximations of definite integrals
- Formally verified approximations of definite integrals
- Principles of verified numerical integration
- Deterministic computation of functional integrals
- An adaptive numerical integration algorithm with automatic result verification for definite integrals
- scientific article; zbMATH DE number 4099672
- A computer-verified monadic functional implementation of the integral
- Two adaptive Gauss-Legendre type algorithms for the verified computation of definite integrals
- scientific article; zbMATH DE number 434850
- scientific article; zbMATH DE number 4174213
Cites work
- A certificate-based approach to formally verified approximations
- A complete uniform substitution calculus for differential dynamic logic
- A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
- A Heuristic Program that Solves Symbolic Integration Problems in Freshman Calculus
- A heuristic prover for real inequalities
- A Skeptic's approach to combining HOL and Maple
- A verified ODE solver and the Lorenz attractor
- Automated and readable simplification of trigonometric expressions
- Differential dynamic logic for hybrid systems
- Feedback systems: an introduction for scientists and engineers.
- Formal analysis of continuous-time systems using Fourier transform
- Formal analysis of the kinematic Jacobian in screw theory
- Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec
- Formalization of camera pose estimation algorithm based on Rodrigues formula
- Formalization of geometric algebra in HOL Light
- Formalization of Laplace transform using the multivariable calculus theory of HOL-Light
- Formalization of the integral calculus in the PVS theorem prover
- Formally verified approximations of definite integrals
- HOL Light: An Overview
- scientific article; zbMATH DE number 3858920 (Why is no real title available?)
- scientific article; zbMATH DE number 1254246 (Why is no real title available?)
- scientific article; zbMATH DE number 1259143 (Why is no real title available?)
- scientific article; zbMATH DE number 1863375 (Why is no real title available?)
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Interactive theorem proving from the perspective of Isabelle/Isar
- Isabelle/HOL. A proof assistant for higher-order logic
- KeYmaera X
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- On the formalization of Fourier transform in higher-order logic
- On the formalization of the Lebesgue integration theory in HOL
- The flow of ODEs
- The gauge integral theory in HOL4
- The misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them?
- Theorem Proving in Higher Order Logics
- Theorema 2.0: computer-assisted natural-style mathematics
- Three chapters of measure theory in Isabelle/HOL
- Verified Real Asymptotics in Isabelle/HOL
Cited in
(6)- HolPy
- Formally verified approximations of definite integrals
- Two adaptive Gauss-Legendre type algorithms for the verified computation of definite integrals
- Iscalc: An Interactive Symbolic Computation Framework (System Description)
- Fast, verified computation for candle
- Principles of verified numerical integration
Describes a project that uses
Uses Software
This page was built for publication: Verified interactive computation of definite integrals
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055881)
