A verified ODE solver and the Lorenz attractor
DOI10.1007/S10817-017-9448-YzbMATH Open1448.68460OpenAlexW2792892743WikidataQ90699726 ScholiaQ90699726MaRDI QIDQ1663218FDOQ1663218
Publication date: 21 August 2018
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-017-9448-y
ordinary differential equation[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=Poincar%EF%BF%BD%EF%BF%BD+map&go=Go Poincar�� map]rigorous numericsIsabelle/HOLLorenz attractor
Strange attractors, chaotic dynamics of systems with hyperbolic behavior (37D45) Nonlinear ordinary differential equations and systems (34A34) Numerical methods for initial value problems involving ordinary differential equations (65L05) Algorithms with automatic result verification (65G20) Software, source code, etc. for problems pertaining to ordinary differential equations (34-04) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automatic Data Refinement
- A rigorous ODE solver and Smale's 14th problem
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Deterministic Nonperiodic Flow
- Singular hyperbolic systems
- Isabelle/HOL. A proof assistant for higher-order logic
- The Lorenz attractor exists
- Refinement Calculus
- Mathematical problems for the next century
- The Lorenz equations: bifurcations, chaos, and strange attractors
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- CakeML
- Affine arithmetic: concepts and applications
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Theorem Proving in Higher Order Logics
- Axioms and hulls
- What's new on Lorenz strange attractors?
- Designing and proving correct a convex hull algorithm with hypermaps in Coq
- Automated Deduction in Geometry
- Constructive Type Classes in Isabelle
- Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis
- Theorem Proving in Higher Order Logics
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- The Picard Algorithm for Ordinary Differential Equations in Coq
- Data Refinement in Isabelle/HOL
- Formally Verified Approximations of Definite Integrals
- A compiled implementation of strong reduction
- The Flow of ODEs
- A Verified Enclosure for the Lorenz Attractor (Rough Diamond)
Cited In (9)
- Formally-verified round-off error analysis of Runge-Kutta methods
- Saddle-type blow-up solutions with computer-assisted proofs: validation and extraction of global nature
- A certificate-based approach to formally verified approximations
- Verified interactive computation of definite integrals
- Algorithm and abstraction in formal mathematics
- The art of solving a large number of non-stiff, low-dimensional ordinary differential equation systems on GPUs and CPUs
- Wild pseudohyperbolic attractor in a four-dimensional Lorenz system
- What is the point of computers? A question for pure mathematicians
- Mathematics and the formal turn
Uses Software
This page was built for publication: A verified ODE solver and the Lorenz attractor
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663218)
