Deciding Predicate Logical Theories of Real-Valued Functions
Stefan Ratschan
TL;DR
The paper advances predicate logic for real-valued functions by formulating a first-order language that includes multi-dimensional smooth functions, evaluation via $\mathit{app}$, and differentiation via $\partial_i$. It proves decidability for the quantifier-free, function-algebraic fragment and, more broadly, semi-decidability or robustness-based termination for fragments with scalar quantification and even transcendental symbols, using translations to $\mathcal{RU}$ and polynomial approximations. A central theme is robustness: by restricting to stable satisfiability notions and leveraging density of polynomial functions, the authors turn otherwise intractable functional constraints into computable procedures, potentially enabling SMT-like tooling for real-valued function theories. The framework is designed to be instantiated with specific application classes (e.g., Lyapunov functions for polynomial ODEs) and to generalize to combinations of fragments, bridging formal logic, computable analysis, and verification of dynamical systems. Overall, the work lays a principled foundation for algorithmic reasoning about real-valued functions, derivatives, and computable transcendental symbols, with implications for verification, synthesis, and certificates in continuous domains.
Abstract
The notion of a real-valued function is central to mathematics, computer science, and many other scientific fields. Despite this importance, there are hardly any positive results on decision procedures for predicate logical theories that reason about real-valued functions. This paper defines a first-order predicate language for reasoning about multi-dimensional smooth real-valued functions and their derivatives, and demonstrates that - despite the obvious undecidability barriers - certain positive decidability results for such a language are indeed possible.