Verified interactive computation of definite integrals
From MaRDI portal
Publication:2055881
DOI10.1007/978-3-030-79876-5_28OpenAlexW3183042468MaRDI QIDQ2055881
Bohua Zhan, Runqing Xu, Liming Li
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_28
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- KeYmaera X
- Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec
- A heuristic prover for real inequalities
- Formalization of camera pose estimation algorithm based on Rodrigues formula
- Differential dynamic logic for hybrid systems
- A Skeptic's approach to combining HOL and Maple
- Isabelle/HOL. A proof assistant for higher-order logic
- Formal analysis of the kinematic Jacobian in screw theory
- Formal analysis of continuous-time systems using Fourier transform
- A verified ODE solver and the Lorenz attractor
- A complete uniform substitution calculus for differential dynamic logic
- Formally verified approximations of definite integrals
- Formalization of geometric algebra in HOL Light
- The gauge integral theory in HOL4
- Automated and readable simplification of trigonometric expressions
- The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them?
- The Flow of ODEs
- On the Formalization of Fourier Transform in Higher-order Logic
- Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light
- A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
- Three Chapters of Measure Theory in Isabelle/HOL
- HOL Light: An Overview
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
- Verified Real Asymptotics in Isabelle/HOL
- Theorema 2.0: Computer-Assisted Natural-Style Mathematics
- Hybrid Systems: Computation and Control
- Hybrid Systems: Computation and Control
- Theorem Proving in Higher Order Logics
- A Heuristic Program that Solves Symbolic Integration Problems in Freshman Calculus
- On the Formalization of the Lebesgue Integration Theory in HOL
- A certificate-based approach to formally verified approximations
This page was built for publication: Verified interactive computation of definite integrals
