Pith. sign in

REVIEW 3 major objections 6 minor 44 references

Approximate Axiomatization for Differentially-Defined Functions

T0 review · 3 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read True facts about sin, cos, and e^x become provable up to any numerical precision.

desk verdict A genuine extension of prior delta-completeness to arbitrary bounded quantifiers over 'differentially-defined' functions, with the main caveat being the imported provable Stone-Weierstrass theorem on which everything rests. read the letter →

arxiv 2506.08233 v1 pith:4VPTHRSS submitted 2025-06-09 cs.LO math.LO

André Platzer , Long Qian This is my paper
classification cs.LOmath.LO
keywords approximateaxiomatizationdifferentialdynamiclogicdifferentially-definedfunctionsdelta-perturbationsrobustnessquantifiereliminationreal-closedfieldspolynomialordinaryequations
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper's claim is that exactness is the only obstacle to a complete proof system for the real numbers expanded with special functions defined by polynomial differential equations, including sin, cos, and e^x. For every bounded first-order sentence $\varphi$ in this language and every rational tolerance $\delta > 0$, a purely arithmetic sentence $A_\exists(\varphi,\delta)$ can be computed so that if $\varphi$ is true then $A_\exists(\varphi,\delta)$ is provable in differential dynamic logic (dL), and if $\varphi$ is false then the negation of the dual approximation $A_\forall(\varphi,\delta)$ is provable. Because the approximations are ordinary formulas of real arithmetic, their truth is decidable by the quantifier-elimination procedure for real-closed fields, giving proof-producing approximate decision procedures that also work for formulas with free variables. For sentences whose only relation symbol is $>$, the approximations converge to the original truth value as $\delta \to 0$, so every true bounded $>$-pure sentence is provable exactly, without slack. The whole axiomatization is a finite fragment of dL, hence a finite addition to the real-closed field axioms that covers all such functions uniformly.

What carries the argument

The central object is the class of differentially-defined functions: univariate functions obtained as the first coordinate of a solution of a polynomial initial-value problem $x' = f(x)$, $x(0) = X$ with rational data and provably global existence; this includes $\sin$, $\cos$, $e^x$ and is universal for continuous functions. The load-bearing proof-theoretic resource is the provable uniform approximation theorem (Theorem 3.2): dL can prove, computably and uniformly, that a polynomial stays within any desired $\varepsilon$ of such an IVP solution on a compact interval. Around these, the paper constructs $\delta$-perturbations: each function term $f(e)$ in a formula is replaced by an interval $[F(e)-\delta, F(e)+\delta]$ around a first-order definable approximant $F$, with the quantified slack variable $w$ read universally (for $A_\forall$) or existentially (for $A_\exists$), producing real-arithmetic formulas that bracket $\varphi$ and whose provability is certified by the derived proof rules $(\delta\forall)$ and $(\delta\exists)$. Robustness is then analyzed through continuous 'margin' functions $r_\varphi$ and $m^I_\varphi$ that measure how much perturbation a true point tolerates, and the openness or closedness of pure-formula truth sets under bounded quantification supplies the convergence as $\delta\to 0$.

What would settle it

Attempt to construct and independently certify the dL proof promised by Theorem 3.2 for the elementary initial-value problem $x' = x$, $x(0) = 1$ on $[0,1]$ with $\varepsilon = 10^{-6}$; if no such proof can be produced or an independent proof checker rejects it, the approximate completeness results of Theorems 4.19 and 5.9 lose their foundation. Alternatively, search for a bounded $>$-pure sentence over a differentially-defined transcendental function whose universal perturbation truth values fail to converge to the original truth value as $\delta \to 0$; Theorem 5.9 predicts none exists.

Watch

Extended reading notes

Core claim

Formally, the paper establishes $\delta$-completeness and robustness for the bounded theory $\mathrm{Th}_B(\mathbb{R}_D)$. For every bounded sentence $\varphi$ in the language of $\mathbb{R}_D$ and every rational $\delta > 0$, there are computable syntactic perturbations $A_\forall(\varphi,\delta)$ and $A_\exists(\varphi,\delta)$ in first-order real arithmetic with the same free variables, satisfying the provable chain $A_\forall(\varphi,\delta) \to \varphi \to A_\exists(\varphi,\delta)$; if $\mathbb{R}_D \models \varphi$ then $\vdash_{\mathrm{dL}} A_\exists(\varphi,\delta)$, and if $\mathbb{R}_D \models \neg\varphi$ then $\vdash_{\mathrm{dL}} \neg A_\forall(\varphi,\delta)$. These perturbations replace each special-function term $f(e)$ by an interval around a polynomial approximant, with universal or existential quantification over the slack variable, and their provability rests on an internally provable uniform polynomial-approximation theorem for polynomial initial-value problems. The paper then shows that $>$-pure bounded formulas are $\forall$-robust and $\geq$-pure bounded formulas are $\exists$-robust: the truth set of a $>$-pure formula is the union over $\delta>0$ of the truth sets of its universal $\delta$-perturbations, and dually for $\geq$-pure formulas. A consequence is that every true bounded $>$-pure sentence is provable in dL exactly, with zero perturbation. Finally, the paper proves a computability-theoretic limit: the bounded theory of all Type-Two computable functions is at least as hard as arithmetic ($\mathbf{0}^{(\omega)}$), so the restriction to differentially-defined functions is essential for these convergence results.

Load-bearing premise

The load-bearing premise is that differential dynamic logic can internally prove arbitrarily accurate polynomial approximations of every polynomial initial-value problem that avoids blow-up on a compact interval; if that provable uniform-approximation theorem fails, the $\delta$-completeness and robustness results collapse.

Editorial extensions

If this is right

  • Every bounded sentence in the language of $\mathbb{R}_D$ becomes the subject of a proof-producing $\delta$-decision procedure: compute the real-arithmetic approximation, decide it by quantifier elimination, and if the strengthened version holds, output a dL proof of the original sentence.
  • The same finite axiomatization works uniformly for all differentially-defined functions, so no per-function axioms or trusted external numerical oracles are required; soundness reduces to the soundness of dL.
  • For bounded $>$-pure sentences, exact completeness holds: every true sentence is provable in dL with zero perturbation, not merely up to $\delta$.
  • Formulas with free variables can be provably under-approximated by quantifier-free real-arithmetic formulas, enabling symbolic constraint synthesis — for instance, explicit rational ranges for Lyapunov-function coefficients — beyond the reach of closed-sentence decision procedures.
  • The robustness guarantee cannot be extended to all Type-Two computable functions, whose bounded theory is at least as hard as truth in arithmetic, so the polynomial-ODE definition of functions is essential to the convergence results.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural next question is which classes beyond pure formulas are robust: any bounded formula whose truth set is open in the product topology is a candidate for $\forall$-robustness, and the paper's distance-based proof suggests a more general criterion in terms of a continuous margin function.
  • The pair $A_\forall(\varphi,\delta) \to \varphi \to A_\exists(\varphi,\delta)$ is a proof-theoretic analogue of interval arithmetic; combining it with interval constraint solving could yield verification methods in which the bracketing is a certified proof artifact rather than a numerical assumption.
  • If the provable uniform-approximation step is made fully explicit and efficient, the same machinery could turn polynomial-ODE reachability analyses into uniform proof generators for transcendental differential equations within a single sound system.
  • The arithmetic lower bound for Type-Two computable functions suggests that symbolic structure — not continuity alone — is what buys approximability; a similar dichotomy may hold for other function classes with suitable symbolic representations, such as analytic functions given by convergent power series.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. This paper presents an approximate axiomatization for the bounded first-order theory of the real closed field expanded with 'differentially-defined' functions, i.e., solutions of polynomial initial-value problems, using differential dynamic logic (dL). The authors define syntactic universal and existential δ-perturbations A∀(φ,δ) and A∃(φ,δ) that replace special-function terms by polynomial approximations with an interval slack of δ, prove that these are provable strengthenings/weakenings of the original formula (Theorem 4.14), and conclude δ-completeness for bounded sentences (Theorem 4.19), proof-producing δ-decidability (Theorem 4.20), and robustness of pure formulas, which yields exact completeness for true >-pure bounded sentences (Theorem 5.9). A computability-theoretic lower bound shows that the analogous bounded theory for all type-two computable functions is at least as hard as arithmetic (Theorem 5.14).

Significance. The main claims, if fully supported, are significant: they replace per-function approximation axioms with a uniform dL axiomatization, lift approximate decidability from closed sentences to formulas with free variables, provide exact completeness for a nontrivial syntactic class, and give proof-producing decision procedures. The paper is explicit about the axioms used (Appendix A), defines the perturbations purely syntactically with no fitted constants, and reports a KeYmaera X verification of the running Lyapunov example. The negative result for the larger class R_C is a useful calibration. However, the entire numerical engine is imported from the companion preprint [31] and is not proved or formalized here, and the robustness proof in Section 5 has local gaps that need repair before the central theorem of that section is fully established.

major comments (3)
  1. [§3.1.3, Theorem 3.2] All of Theorems 4.7, 4.18, 4.19, and 5.9 rest on Theorem 3.2, imported from [31, Thm 5.5], an arXiv preprint whose proof is neither reproduced nor formalized in this manuscript. The proof of Theorem 3.3 in Appendix B reduces directly to that theorem, and no independent proof of the provable Stone-Weierstrass result is supplied. Because this is the load-bearing numerical foundation, the paper should either include a complete proof of Theorem 3.2 in the dL fragment of Appendix A or state explicitly that the results are conditional on [31] and give the exact statement and proof location of the imported theorem.
  2. [§5, Lemma 5.11] Definition 4.11 defines A∀_F(φ,δ) only for δ ∈ Q+, and Definition 4.16 restricts admissibility to δ ∈ Q+. Lemma 5.11(4), however, asserts membership in A∀_F(φ, m_I_φ(z)) for a real-valued continuous function m_I_φ, and Theorem 5.9 subsequently uses this for real δ. If m_I_φ(z) is irrational, the perturbed formula is not a well-formed FOL_R formula under the paper's own definitions. The lemma and its proof should be restated for rational δ, e.g., for all δ ∈ Q+ with 0 < δ ≤ m_I_φ(z), and the monotonicity step adjusted accordingly.
  3. [§5, Lemma 5.11 proof] In the proof of Lemma 5.11, case φ(x) ≡ ψ(f(e),x), step (3)=>(4), the inductive hypothesis (4) is applied to the approximation G at tolerance m_J_ψ(w,x) before the needed inequality m_I_φ(x) ≤ m_J_ψ(w,x) is established; since admissibility is defined by a strict inequality and is monotone with respect to the tolerance, the application is justified only after the inequality is proven. Additionally, in the universal-quantifier case the proof says the argument is identical to the existential case, but the existential argument selects one witness attaining the maximum, whereas the universal case must produce membership for every y in the interval. These issues are repairable, but the proof as written has a genuine gap in a theorem on which Theorem 5.9 depends.
minor comments (6)
  1. [§4, after Definition 4.5] The sentence 'Theorem 4.5 shows that ε-enclosures can always be computed' should refer to Theorem 4.6, since Definition 4.5 only defines ε-enclosures.
  2. [§5, Example 5.8] The displayed universal perturbation uses a single variable w for the three occurrences of e^x, whereas Definition 4.11 introduces separate fresh variables for each atomic occurrence. The falsifiability argument remains valid, but the displayed formula is a simplification and should be labeled as such.
  3. [§1, technical results] The introductory statement that the chain A∀(φ,δ) → φ → A∃(φ,δ) is provable for every δ omits the admissibility condition on the approximation F; the precise statement in Theorem 4.14 should be referenced here.
  4. [Appendix B, proof of Theorem 3.3] The proof combines the approximations to obtain the bound |p(t)-h(t)| < 3ε/4, which is indeed < ε, but the text should explicitly note that the final stated bound follows because 3ε/4 < ε.
  5. [§4, Definition 4.11] The notation ∀_{F(e)+[-δ,δ]} w is used before the interval-quantifier shorthand is explained; a brief clarification in Definition 4.1 would improve readability.
  6. [§1] There is a typo: 'trignometric' should be 'trigonometric'.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the δ-completeness and robustness theorems depend on the imported Stone-Weierstrass theorem [31] as a lemma, but do not reduce to their own inputs by construction.

full rationale

The paper's derivation chain is not circular. The δ-perturbations A∀(φ,δ) and A∃(φ,δ) are purely syntactic (Definition 4.11), and the admissibility norm ∥F∥_I = max_{f(e)} ∥F_{f(e)}−f∥_{I_e} < δ (Definition 4.16) is an error condition imposed on the approximants before any perturbation conclusion is drawn. Theorem 4.14 derives ⊢∀x(A∀(φ,δ)→φ) and ⊢∀x(φ→A∃(φ,δ)) from provable admissibility premises by structural induction; it does not assume the approximate-completeness conclusion. Theorem 4.19 then obtains ⊢ A∃(φ,δ) for true φ by combining the provable weakening φ→A∃ with soundness and the decidability of the resulting FOL_R sentence. The load-bearing external input is Theorem 3.2, imported from the same authors' prior work [31, Thm 5.5]: 'for all ε∈Q_+, there (computably) exists some θ(t)∈Q^n[t] such that ... is provable in dL.' Theorems 3.3, 4.7, and 4.18 reduce to this theorem, and the global-existence precondition for each function symbol is imported from [40]. These are genuine proof dependencies: the imported theorem concerns polynomial IVPs, has stated assumptions that do not include the target results, and is not fitted to the truth values whose provability is claimed. The failure to reproduce or machine-check [31] is a correctness risk, not a circularity; the central claims are not equivalent to their inputs by construction.

Assumptions & free parameters 1 free parameters · 5 assumptions · 0 invented entities

The central claim rests on the soundness of dL, the imported provable Stone-Weierstrass theorem, and the global-existence condition; no new entities are postulated. The delta-perturbations and polynomial approximations are constructed objects, not fitted parameters.

free parameters (1)
  • delta (perturbation tolerance) = user-specified rational > 0
    The theorems hold for every delta>0; delta is an input precision parameter, not a value fitted to data to make a conclusion true. The choice of delta does not affect the validity of the axiomatization.
assumptions (5)
  • domain assumption Soundness of the differential dynamic logic axiomatization, including the ODE and differential-induction axioms (Theorem A.1 from [29,32,40])
    The paper's provability claims are relative to dL; unsoundness in dL would invalidate the derivations. dL soundness is standard and has been formalized in prior work [3,4,38].
  • domain assumption Provable Stone-Weierstrass: dL can prove uniform polynomial approximations of polynomial-IVP solutions on compact intervals (Theorem 3.2, from [31, Theorem 5.5])
    This is the numerical engine for the paper; Theorem 3.3, provable enclosures (Theorem 4.7), and admissibility existence (Theorem 4.18) all rely on it. The result is imported from a co-authored prior preprint and not reproduced here. It is a theorem about dL, not a standard mathematical result.
  • domain assumption All differentially-defined functions considered have provable global existence of their defining IVP (Section 3.1.1)
    Function symbols are only admitted when the defining existence formula is provable in dL; the paper relies on earlier work [40] that sin, cos, e^x and functions with definable bounds satisfy this.
  • standard math Tarski quantifier elimination and completeness for real-closed fields (R rule)
    Used so that FOL_R perturbed sentences are decidable and provable; standard background.
  • standard math Standard computable-analysis facts used in Section 5: TTE computability, computable space-filling curves, extension theorems for computable functions
    Used for the lower bound on ThB(R_C) (Theorem 5.14, Lemmas 5.15, 5.16).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Approximate Axiomatization for Differentially-Defined Functions." pith.science (2026). https://pith.science/paper/4VPTHRSS

@misc{pith2026250608233,
  author       = {Pith},
  title        = {Pith review of: Approximate Axiomatization for Differentially-Defined Functions},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4VPTHRSS}},
  note         = {Machine review of arXiv:2506.08233}
}
abstract

This article establishes a complete approximate axiomatization for the real-closed field $\mathbb{R}$ expanded with all differentially-defined functions, including special functions such as $\sin(x), \cos(x), e^x, \dots$. 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 $\text{FOL}_{\mathbb{R}}$ formulas, improving upon earlier decidability results only concerning closed sentences.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

44 extracted references · 20 canonical work pages

  1. [31]

    André Platzer and Long Qian. 2024. Axiomatization of Compact Initial Value Problems: Open Properties. arXiv:2410.13836 [cs.LO] https://arxiv.org/abs/2410.13836

    work page arXiv 2024

  2. [1]

    Behzad Akbarpour and Lawrence C. Paulson. 2010. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions.J. Autom. Reason.44, 3 (2010), 175–205. https://doi.org/10.1007/S10817-009-9149-2

    doi:10.1007/s10817-009-9149-2 2010

  3. [2]

    Batyrshin, Nikolay Bazhenov, Dmitry Bushtets, Marina Dorzhieva, Heer Tern Koh, Ruslan Kornev, Alexander G

    Ramil Bagaviev, Ilnur I. Batyrshin, Nikolay Bazhenov, Dmitry Bushtets, Marina Dorzhieva, Heer Tern Koh, Ruslan Kornev, Alexander G. Melnikov, and Keng Meng Ng. 2025. Computably and punctually universal spaces.Ann. Pure Appl. Log.176, 1 (2025), 103491. https://doi.org/10.1016/J.APAL.2024.103491

    arXiv 2025

  4. [3]

    Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer. 2017. Formally Verified Differential Dynamic Logic. InCertified Programs and Proofs - 6th ACM SIGPLAN Conference, CPP 2017, Paris, France, January 16-17, 2017, Yves Bertot and Viktor Vafeiadis (Eds.). ACM, 208–221. https://doi.org/10.1145/3018610.3018616

    arXiv 2017

  5. [4]

    Rose Bohrer. 2017. Differential Dynamic Logic.Archive of Formal Proofs(February 2017). https://isa-afp.org/entries/ Differential_Dynamic_Logic.html, Formal proof development

    work page 2017

  6. [5]

    Olivier Bournez, Riccardo Gozzi, Daniel Silva Graça, and Amaury Pouly. 2023. A continuous characterization of PSPACE using polynomial ordinary differential equations.J. Complex.77 (2023), 101755. https://doi.org/10.1016/J.JCO. 2023.101755

    arXiv 2023

  7. [6]

    Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. 2018. Incremental Lin- earization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions.ACM Trans. Comput. Logic19, 3, Article 19 (Aug. 2018), 52 pages. https://doi.org/10.1145/3230639

    doi:10.1145/3230639 2018

  8. [7]

    Peter Franek, Stefan Ratschan, and Piotr Zgliczynski. 2011. Satisfiability of Systems of Equations of Real Analytic Functions Is Quasi-decidable. InMathematical Foundations of Computer Science 2011 (LNCS), Filip Murlak and Piotr Sankowski (Eds.). Springer, Berlin, Heidelberg, 315–326. https://doi.org/10.1007/978-3-642-22993-0_30

    work page doi:10.1007/978-3-642-22993-0_30 2011

Show all 44 references
  1. [8]

    Peter Franek, Stefan Ratschan, and Piotr Zgliczynski. 2016. Quasi-decidability of a Fragment of the First-Order Theory of Real Numbers.Journal of Automated Reasoning57, 2 (Aug. 2016), 157–185. https://doi.org/10.1007/s10817-015-9351-3 , Vol. 1, No. 1, Article . Publication dat...

    2016 doi

  2. [9]

    Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and André Platzer. 2015. KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. InAutomated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015,...

    2015 doi

  3. [10]

    James Gallicchio, Yong Kiam Tan, Stefan Mitsch, and André Platzer. 2022. Implicit Definitions with Differential Equations for KeYmaera X - (System Description). InAutomated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedin...

    2022 doi

  4. [12]

    Sicun Gao, Jeremy Avigad, and Edmund M. Clarke. 2012. Delta-Decidability over the Reals. In2012 27th Annual IEEE Symposium on Logic in Computer Science. 305–314. https://doi.org/10.1109/LICS.2012.41

    2012 doi

  5. [13]

    Sicun Gao, Soonho Kong, Wei Chen, and Edmund Clarke. 2014. Delta-Complete Analysis for Bounded Reachability of Hybrid Systems. arXiv:1404.7171 (Apr 2014). http://arxiv.org/abs/1404.7171 arXiv:1404.7171 [cs]

    2014 arXiv

  6. [14]

    Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2013. dReal: An SMT Solver for Nonlinear Theories over the Reals. InAutomated Deduction – CADE-24, Maria Paola Bonacina (Ed.). Springer, Berlin, Heidelberg, 208–214. https: //doi.org/10.1007/978-3-642-38574-2_14

    2013 doi

  7. [15]

    Sicun Gao, Soonho Kong, and Edmund M. Clarke. 2014. Proof Generation from Delta-Decisions. In2014 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. 156–163. https://doi.org/10.1109/SYNASC. 2014.29

    2014 doi

  8. [16]

    Kurt Gödel. 1931. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.Monatsh. Math. Phys.38, 1 (1931), 173–198. https://doi.org/10.1007/BF01700692

    1931 doi

  9. [17]

    Daniel Graça, Ning Zhong, and Jorge Buescu. 2009. Computability, noncomputability and undecidability of maximal intervals of IVPs.Trans. Amer. Math. Soc.361, 6 (Jan 2009), 2913–2927. https://doi.org/10.1090/S0002-9947-09-04929-0

    2009 doi

  10. [18]

    Wolfram Research, Inc. [n. d.]. Mathematica, Version 14.2. https://www.wolfram.com/mathematica Champaign, IL, 2024

    2024

  11. [19]

    Mats Jirstrand. 1997. Nonlinear Control System Design by Quantifier Elimination.J. Symb. Comput.24, 2 (1997), 137–152. https://doi.org/10.1006/JSCO.1997.0119

    1997

  12. [20]

    Deshmukh, Sriram Sankaranarayanan, and Nikos Aréchiga

    James Kapinski, Jyotirmoy V. Deshmukh, Sriram Sankaranarayanan, and Nikos Aréchiga. 2014. Simulation-guided lyapunov analysis for hybrid dynamical systems. In17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC’14, Berlin, Germany, ...

    2014

  13. [21]

    Akitoshi Kawamura and Stephen A. Cook. 2012. Complexity Theory for Operators in Analysis.ACM Trans. Comput. Theory4, 2 (2012), 5:1–5:24. https://doi.org/10.1145/2189778.2189780

    2012

  14. [22]

    Soonho Kong, Armando Solar-Lezama, and Sicun Gao. 2018. Delta-Decision Procedures for Exists-Forall Problems over the Reals. InComputer Aided Verification - 30th International Conference, CA V 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14...

    2018 doi

  15. [23]

    Katherine Kosaian, Yong Kiam Tan, and André Platzer. 2023. A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. InProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 202...

    2023

  16. [24]

    Enrico Lipparini and Stefan Ratschan. 2025. Satisfiability of Non-linear Transcendental Arithmetic as a Certificate Search Problem: Satisfiability of Non-linear Transcendental...J. Autom. Reason.69, 1 (Jan. 2025), 35 pages. https: //doi.org/10.1007/s10817-024-09716-3

    2025 doi

  17. [25]

    Sean McLaughlin and John Harrison. 2005. A Proof-Producing Decision Procedure for Real Arithmetic. InAutomated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings (Lecture Notes in Computer Science, Vol. 36...

    2005

  18. [26]

    André Platzer. 2008. Differential Dynamic Logic for Hybrid Systems.J. Autom. Reason.41, 2 (2008), 143–189. https://doi.org/10.1007/S10817-008-9103-8

    2008 doi

  19. [28]

    André Platzer. 2012. The Complete Proof Theory of Hybrid Systems. In2012 27th Annual IEEE Symposium on Logic in Computer Science. 541–550. https://doi.org/10.1109/LICS.2012.64 , Vol. 1, No. 1, Article . Publication date: September 20yy. 34 André Platzer and Long Qian

    2012 doi

  20. [29]

    André Platzer. 2012. Logics of Dynamical Systems. InProceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. IEEE Computer Society, 13–24. https://doi.org/10. 1109/LICS.2012.13

    2012

  21. [30]

    André Platzer. 2017. A Complete Uniform Substitution Calculus for Differential Dynamic Logic.J. Autom. Reason.59, 2 (2017), 219–265. https://doi.org/10.1007/S10817-016-9385-1

    2017 doi

  22. [32]

    André Platzer and Yong Kiam Tan. 2020. Differential Equation Invariance Axiomatization.J. ACM67, 1 (2020), 6:1–6:66. https://doi.org/10.1145/3380825

    2020 doi

  23. [33]

    Amaury Pouly and Olivier Bournez. 2020. A Universal Ordinary Differential Equation.Logical Methods in Computer ScienceVolume 16, Issue 1 (Feb 2020). https://doi.org/10.23638/LMCS-16(1:28)2020

    2020 doi

  24. [34]

    Pour-El and J

    Marian B. Pour-El and J. Ian Richards. 2017.Computability in Analysis and Physics. Cambridge University Press, Cambridge. https://doi.org/10.1017/9781316717325

    2017 doi

  25. [35]

    Stefan Ratschan. 2002. Quantified Constraints Under Perturbation.J. Symb. Comput.33, 4 (2002), 493–505. https: //doi.org/10.1006/JSCO.2001.0519

    2002

  26. [36]

    Stefan Ratschan. 2006. Efficient solving of quantified inequality constraints over the real numbers.ACM Trans. Comput. Log.7, 4 (2006), 723–748. https://doi.org/10.1145/1183278.1183282

    2006

  27. [37]

    Daniel Richardson. 1968. Some Undecidable Problems Involving Elementary Functions of a Real Variable.J. Symb. Log. 33, 4 (1968), 514–520. https://doi.org/10.2307/2271358

    1968 doi

  28. [38]

    Tanner Slagel, Mariano M

    J. Tanner Slagel, Mariano M. Moscato, Lauren M. White, César A. Muñoz, Swee Balachandran, and Aaron Dutle

  29. [39]

    Robert I. Soare. 2016.Turing Computability: Theory and Applications. Springer, Heidelberg. https://doi.org/10.1007/978- 3-642-31933-4

    2016 doi

  30. [40]

    Yong Kiam Tan and André Platzer. 2021. An axiomatic approach to existence and liveness for differential equations. Formal Aspects Comput.33, 4-5 (2021), 461–518. https://doi.org/10.1007/S00165-020-00525-0

    2021 doi

  31. [41]

    1948.A Decision Method for Elementary Algebra and Geometry

    Alfred Tarski. 1948.A Decision Method for Elementary Algebra and Geometry. The Rand Corporation, Santa Monica, Calif

    1948

  32. [42]

    Rick Voßwinkel and Klaus Röbenack. 2019. A Control Lyapunov Function Approach Using Quantifier Elimination. In 23rd International Conference on System Theory, Control and Computing, ICSTCC 2019, Sinaia, Romania, October 9-11,

    2019

  33. [43]

    Paul S. Wang. 1974. The Undecidability of the Existence of Zeros of Real Elementary Functions.J. ACM21, 4 (1974), 586–589. https://doi.org/10.1145/321850.321856

    1974

  34. [44]

    2000.Computable Analysis: An Introduction

    Klaus Weihrauch. 2000.Computable Analysis: An Introduction. Springer, Heidelberg. https://doi.org/10.1007/978-3- 642-56999-9 , Vol. 1, No. 1, Article . Publication date: September 20yy

    2000 doi

  35. [2019]

    https://doi.org/10.1109/ICSTCC.2019.8885848

    IEEE, 186–191. https://doi.org/10.1109/ICSTCC.2019.8885848

    2019

  36. [2023]

    Embedding Differential Dynamic Logic in PVS. InProceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis, LSFA/HCVS 2023, and 10th Workshop on Horn Clauses for Verification and...

    2023 doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.