Approximate Axiomatization for Differentially-Defined Functions

2025/06/09 by André Platzer, Platzer, André, Qian, Long
Computer Science · #Logic, Reasoning, and Knowledge #Formal Methods in Verification #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2506.08233

Abstract

This article establishes a complete approximate axiomatization for the real-closed field ℝ expanded with all differentially-defined functions, including special functions such as sin(x), cos(x), e^x, …. Every true sentence is provable up to some numerical approximation, and the truth of such approximations converge under mild conditions. Such an axiomatization is a fragment of the axiomatization for differential dynamic logic, and is therefore a finite extension of the axiomatization of real-closed fields. Furthermore, the numerical approximations approximate formulas containing special function symbols by FOL_ℝ formulas, improving upon earlier decidability results only concerning closed sentences.

Citations

• Axiomatization of Compact Initial Value Problems: Open Properties
• Differential Equation Invariance Axiomatization
• Delta-Decision Procedures for Exists-Forall Problems over the Reals
• Proof Generation from Delta-Decisions
• Delta-Complete Analysis for Bounded Reachability of Hybrid Systems
• Quasi-decidability of a Fragment of the First-order Theory of Real Numbers
• Efficient Solving of Quantified Inequality Constraints over the Real Numbers

Related

• Calculus: a limitless perspective
• Differential Equation Invariance Axiomatization
• A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
• Operations for D-Algebraic Functions
• General approach to function approximation