Approximate Axiomatization for Differentially-Defined Functions 2TXXQ2575Y
| URI | m2://res/2TXXQ2575Y |
|---|---|
| Kind | preprint |
| Creators | André Platzer, Long Qian |
| Date | 2025-06-09 |
| MSC | 03B70, 03F03, 65L70, 65G20 |
| Subjects | arxiv cs.LO, arxiv math.LO |
| Scope | in |
Expressions
e1: version, preprint
| Language | en |
|---|---|
| Date | 2025-06-09 |
| Ids | arXiv 2506.08233, zbl_id 902757447 |
Items in this resource
The mentions of the inventory that name this resource. Each name links to the card of its inventory row.
| Item | Kind | Where | Source |
|---|---|---|---|
| 11193H199Y | statement | lemma 5.16 | arxiv |
| $\eps$-enclosures | definition | definition 4.5 | arxiv |
| Stone-Weierstrass | statement | theorem 3.2 | arxiv |
| 3W8KPY6P1C | statement | lemma 5.10 | arxiv |
| Transfer of approximations | statement | lemma 5.7 | arxiv |
| Bounded semantics | definition | definition 5.2 | arxiv |
| 59DJTWCBEH | statement | lemma 5.11 | arxiv |
| Computable $\eps$-enclosures | statement | theorem 4.6 | arxiv |
| 9JYBF4DZB3 | statement | theorem A.1 | arxiv |
| 9STN1FD7KJ | statement | theorem 4.18 | arxiv |
| Non-robust sentence | example | example 5.8 | arxiv |
| Characterization of robustness | statement | theorem 5.5 | arxiv |
| Proof-producing $\delta$-decidability | statement | theorem 4.20 | arxiv |
| $\delta$-perturbations | definition | definition 4.11 | arxiv |
| $\delta$-Completeness | statement | theorem 4.19 | arxiv |
| Pure formulas | definition | definition 5.1 | arxiv |
| Notations | definition | definition 4.1 | arxiv |
| Name | definition | definition 3.4 | arxiv |
| Symbolic Conditions for Lyapunov Functions \footnote{This example has been formally verified using the $\dL$ theorem prover KeYmaera X with exact arithmetic. | example | example 4.15 | arxiv |
| EEBVB66P9N | definition | definition 5.12 | arxiv |
| Robustness | definition | definition 5.3 | arxiv |
| Computable function | definition | definition 3.7 | arxiv |
| Existence of Lyapunov Functions in {$\R_D$ | example | example 4.3 | arxiv |
| Type-two computable number | definition | definition 3.5 | arxiv |
| Pure formulas are robust | statement | theorem 5.9 | arxiv |
| Duality of $\delta$-perturbations | statement | lemma 4.13 | arxiv |
| NEN22DE1K5 | statement | theorem 5.14 | arxiv |
| $\eps$-enclosures are provable | statement | theorem 4.7 | arxiv |
| Definable approximations | definition | definition 4.9 | arxiv |
| Perturbation of formulas | example | example 4.10 | arxiv |
| Domain of bounded formulas | definition | definition 4.4 | arxiv |
| V30VDKVT61 | statement | theorem 3.1 | arxiv |
| Computable space-filling curves | statement | lemma 5.15 | arxiv |
| VCAR2TJ5NY | statement | corollary 4.8 | arxiv |
| VEGB7CBQ7T | definition | definition 5.13 | arxiv |
| Provable $\delta$-Perturbations | statement | theorem 4.14 | arxiv |
| Admissible approximations | definition | definition 4.16 | arxiv |
| Stone-Weierstrass for Differentially-Defined Functions | statement | theorem 3.3 | arxiv |
| ZPRP9CPP7N | definition | definition 3.6 | arxiv |
Catalogue records
- arxiv: 2506.08233 (work)
- arxiv_text: 2506.08233 (work)
- zbmath_search: 902757447 (work)