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.

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