### Abstract

We present a formally verified implementation of multivariate Taylor models. Taylor models are a form of rigorous polynomial approximation, consisting of an approximation polynomial based on Taylor expansions, combined with a rigorous bound on the approximation error. Taylor models were introduced as a tool to mitigate the dependency problem of interval arithmetic. Our implementation automatically computes Taylor models for the class of elementary functions, expressed by composition of arithmetic operations and basic functions like exp, sin, or square root.

### License

BSD License

### Topics

- Computer science/Algorithms/Mathematical
- Computer science/Data structures
- Mathematics/Analysis
- Mathematics/Algebra

### Session Taylor_Models

- Polynomial_Expression
- Float_Topology
- Horner_Eval
- Polynomial_Expression_Additional
- Taylor_Models_Misc
- Taylor_Models
- Experiments

### Depends on

- Affine Arithmetic

### Auto-related entries

- Hensel’s Lemma for the p-adic Integers

## Cite

×

Taylor_Models-AFP

    @article{Taylor_Models-AFP,
      author  = {Christoph Traut and Fabian Immler},
      title   = {Taylor Models},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Taylor_Models.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Jan 8, 2018 : Isabelle2017