Verified interactive computation of definite integrals
type: Item
instance of: scholarly article
title: Verified interactive computation of definite integrals
DOI: 10.1007/978-3-030-79876-5_28
author: Runqing Xu
author: Liming Li
author: Bohua Zhan
publication date: 2021-12-01T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7437096
zbMATH Keywords: symbolic integration
zbMATH Keywords: user interface
zbMATH Keywords: proof automation
cites work: KeYmaera X
cites work: Q4790649
cites work: Q3503410
cites work: A heuristic prover for real inequalities
cites work: Q4227289
cites work: A certificate-based approach to formally verified approximations
cites work: Theorema 2.0: Computer-Assisted Natural-Style Mathematics
cites work: Q3497626
cites work: Formalization of camera pose estimation algorithm based on Rodrigues formula
cites work: A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
cites work: The misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them?
cites work: Verified Real Asymptotics in Isabelle/HOL
cites work: Automated and readable simplification of trigonometric expressions
cites work: KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
cites work: Q4231030
cites work: HOL Light: An Overview
cites work: Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec
cites work: A Skeptic's approach to combining HOL and Maple
cites work: Three Chapters of Measure Theory in Isabelle/HOL
cites work: A verified ODE solver and the Lorenz attractor
cites work: The Flow of ODEs
cites work: Formalization of geometric algebra in HOL Light
cites work: Formally verified approximations of definite integrals
cites work: On the Formalization of the Lebesgue Integration Theory in HOL
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q3328350
cites work: Differential dynamic logic for hybrid systems
cites work: A complete uniform substitution calculus for differential dynamic logic
cites work: Hybrid Systems: Computation and Control
cites work: On the Formalization of Fourier Transform in Higher-order Logic
cites work: Formal analysis of continuous-time systems using Fourier transform
cites work: Theorem Proving in Higher Order Logics
cites work: The gauge integral theory in HOL4
cites work: Formal analysis of the kinematic Jacobian in screw theory
cites work: A Heuristic Program that Solves Symbolic Integration Problems in Freshman Calculus
cites work: Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light
cites work: Q5219926
describes a project that uses: KeYmaera X
describes a project that uses: Theorema
describes a project that uses: Lean
describes a project that uses: jsCoq
describes a project that uses: Isabelle/Isar
describes a project that uses: PVS
describes a project that uses: Isabelle/HOL
describes a project that uses: HOL
describes a project that uses: Python
MaRDI profile type: Publication
full work available at URL: 978-3-030-79876-5 28
OpenAlex ID: W3183042468
Recommended article: Formally Verified Approximations of Definite Integrals
Recommended article: Formally verified approximations of definite integrals
Recommended article: Principles of verified numerical integration
Recommended article: Deterministic computation of functional integrals
Recommended article: An adaptive numerical integration algorithm with automatic result verification for definite integrals
Recommended article: Q3825327
Recommended article: A computer-verified monadic functional implementation of the integral
Recommended article: Two adaptive Gauss-Legendre type algorithms for the verified computation of definite integrals
Recommended article: Q3139694
Recommended article: Q3198780
description: scientific article; zbMATH DE number 7437096