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.

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