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.

翻译：实值函数的概念在数学、计算机科学及众多其他科学领域中具有核心地位。尽管其重要性不言而喻，但关于实值函数推理的谓词逻辑理论判定程序，几乎不存在任何积极的研究成果。本文定义了一种一阶谓词语言，用于对多维光滑实值函数及其导数进行推理，并证明——尽管存在明显的不可判定性障碍——针对此类语言的某些正向可判定性结果确实是可能实现的。