Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Axiomatization of Compact Initial Value Problems: Open Properties

André Platzer, Long Qian

TL;DR

The article establishes a complete and computable axiomatization for compact IVPs within differential dynamic logic, bridging deductive proofs and numerical approximations. It introduces definable deflatable approximants (LDAs) and proves that error bounds and open safety, open liveness, and existence properties over compact time horizons are provable from symbolic axioms, even without global domain constraints. Central technical contributions include a continuous-dependence lemma, Taylor-exponential bounding techniques, and a Stone–Weierstrass-style approximation framework, all enabling effective, certifiable proofs of numerical error bounds. The results yield a unified framework where numerical outputs can be systematically certified by deductive proofs, enhancing trustworthiness for CPS verification on compact horizons. This work thus advances reliable reachability and invariant reasoning for polynomial IVPs, with implications for rigorous toolchains like KeYmaera X and related symbolic-numeric verification pipelines.

Abstract

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.

Axiomatization of Compact Initial Value Problems: Open Properties

TL;DR

The article establishes a complete and computable axiomatization for compact IVPs within differential dynamic logic, bridging deductive proofs and numerical approximations. It introduces definable deflatable approximants (LDAs) and proves that error bounds and open safety, open liveness, and existence properties over compact time horizons are provable from symbolic axioms, even without global domain constraints. Central technical contributions include a continuous-dependence lemma, Taylor-exponential bounding techniques, and a Stone–Weierstrass-style approximation framework, all enabling effective, certifiable proofs of numerical error bounds. The results yield a unified framework where numerical outputs can be systematically certified by deductive proofs, enhancing trustworthiness for CPS verification on compact horizons. This work thus advances reliable reachability and invariant reasoning for polynomial IVPs, with implications for rigorous toolchains like KeYmaera X and related symbolic-numeric verification pipelines.

Abstract

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.

Paper Structure

This paper contains 18 sections, 23 theorems, 72 equations.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Differential Dynamic Logic
  5. Syntax
  6. Semantics
  7. Proof calculus
  8. Computability and Computable analysis
  9. Completeness Under Domain Constraints
  10. Compact IVPs and Approximants
  11. Provable IVP Approximants
  12. Provable Taylor Bounds on Exponentials
  13. Proving Domain Constraints and Bounded Completeness
  14. Error Bounds Without Domain Constraints
  15. Symbolic Domain Constraints and Completeness on Compact Time Horizons
  16. ...and 3 more sections

Key Result

Theorem 3.1

$\text{\upshaped{}$\mathcal{L}$}\xspace$ is complete for differential invariants. For all $\text{FOL}_{\mathbb{R}}$ formulas $P, Q$ and ODE $x' = f(x)$, construct the corresponding $\text{\upshaped{}$\mathcal{L}$}\xspace$ formula as follows If the formula is valid, then one can effectively find a proof of it in $\text{\upshaped{}$\mathcal{L}$}\xspace$. We will make use of this result with the fol

Theorems & Definitions (49)

  • Theorem 3.1: Completeness of Differential Invariants DBLP:journals/jacm/PlatzerT20
  • Definition 3.2: Name
  • Definition 3.3: Type-two computable number
  • Definition 3.4
  • Definition 3.5: Weihrauch_2000
  • Theorem 3.6
  • Definition 3.7: Computable function
  • Theorem 3.8: Computable extreme value theorem Weihrauch_2000
  • Definition 4.1: Notation
  • Definition 4.2: Compact IVP
  • ...and 39 more