We address the decision problem for a fragment of real analysis involving differentiable functions with continuous first derivatives. The proposed theory, besides the operators of Tarski's theory of reals, includes predicates for comparisons, monotonicity, convexity, and derivative of functions over bounded closed intervals or unbounded intervals. Our decision algorithm is obtained by showing that satisfiable formulae of our theory admit canonical models in which functional variables are interpreted as piecewise exponential functions. These can be implicitly described within the decidable Tarski's theory of reals. Our satisfiability test generalizes previous decidability results not involving derivative operators.

翻译：本文研究涉及具有连续一阶导数的可微函数的实数分析片段的可判定性问题。所提出的理论除包含塔斯基实数理论的算子外，还引入了有界闭区间或无界区间上函数比较、单调性、凸性及导数的谓词。通过证明该理论的可满足公式允许将函数变量解释为分段指数函数的典范模型，我们得到了决策算法。这些函数可在可判定的塔斯基实数理论中进行隐式描述。我们的可满足性检验推广了先前不涉及导数算子的可判定性结果。