Axiomatization of Compact Initial Value Problems: Open Properties
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866918226382815232 |
|---|---|
| author | Platzer, André Qian, Long |
| author_facet | Platzer, André Qian, Long |
| contents | This article proves the completeness of an axiomatization for initial value problems (IVPs) with compact initial conditions and compact time horizons for bounded open safety, open liveness and existence properties. Completeness systematically reduces the proofs of these properties to a complete axiomatization for differential equation invariants. This result unifies symbolic logic and numerical analysis by a computable procedure that generates symbolic proofs with differential invariants for rigorous error bounds of numerical solutions to polynomial initial value problems. The procedure is modular and works for all polynomial IVPs with rational coefficients and initial conditions and symbolic parameters constrained to compact sets. Furthermore, this paper discusses generalizations to IVPs with initial conditions/symbolic parameters that are not necessarily constrained to compact sets, achieved through the derivation of fully symbolic axioms/proof-rules based on the axiomatization. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_13836 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Axiomatization of Compact Initial Value Problems: Open Properties Platzer, André Qian, Long Logic in Computer Science Programming Languages Logic 03B70, 03D80, 03F03, 34C14, 34A38, 34C11, 65L70, 65G20 F.4.1; F.3.1; G.1.7; I.2.3 This article proves the completeness of an axiomatization for initial value problems (IVPs) with compact initial conditions and compact time horizons for bounded open safety, open liveness and existence properties. Completeness systematically reduces the proofs of these properties to a complete axiomatization for differential equation invariants. This result unifies symbolic logic and numerical analysis by a computable procedure that generates symbolic proofs with differential invariants for rigorous error bounds of numerical solutions to polynomial initial value problems. The procedure is modular and works for all polynomial IVPs with rational coefficients and initial conditions and symbolic parameters constrained to compact sets. Furthermore, this paper discusses generalizations to IVPs with initial conditions/symbolic parameters that are not necessarily constrained to compact sets, achieved through the derivation of fully symbolic axioms/proof-rules based on the axiomatization. |
| title | Axiomatization of Compact Initial Value Problems: Open Properties |
| topic | Logic in Computer Science Programming Languages Logic 03B70, 03D80, 03F03, 34C14, 34A38, 34C11, 65L70, 65G20 F.4.1; F.3.1; G.1.7; I.2.3 |
| url | https://arxiv.org/abs/2410.13836 |