A Verified Enclosure for the Lorenz Attractor (Rough Diamond)

DOI10.1007/978-3-319-22102-1_14zbMath1465.65040OpenAlexW1924092145MaRDI QIDQ2945634

Fabian Immler

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_14

zbMATH Keywords

ordinary differential equationLorenz attractorrigorous numericsIsabelle/HOL

Mathematics Subject Classification ID

Dynamics induced by flows and semiflows (37C10) Strange attractors, chaotic dynamics of systems with hyperbolic behavior (37D45) Attractors of solutions to ordinary differential equations (34D45) Algorithms with automatic result verification (65G20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

A verified ODE solver and the Lorenz attractor

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Ordinary Differential Equations

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• A rigorous ODE solver and Smale's 14th problem
• Affine arithmetic: concepts and applications
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis
• The Lorenz attractor exists

This page was built for publication: A Verified Enclosure for the Lorenz Attractor (Rough Diamond)