实数分析片段的判决算法。III：可微函数理论（半）开区间

本文丰富了针对无量词语言的满足性测试，这些测试反过来又增强了 Tarski 初等代数的一个片段，加入具有连续一阶导数的 unary 实函数。可用的两种变量类型，一种取值范围为实数，另一种取值范围为感兴趣的函数。数值项是通过实变量的基本算术运算以及通过函数应用构造 $f(t)$ 和 $D[\,f\,](t)$ 构建的，其中 $f$ 代表函数变量，$t$ 代表数值项，$D[\,\sqdot\,]$ 代表微分算子。可以在数值项之间放置比较关系。还可用的谓词符号数组也可用于表示各种函数之间的关系以及函数属性，这些属性可能在实数轴上的区间内成立；这些包括：（点wise）函数比较、严格和非严格的单调性/凸性/凹性属性、函数导数与实数的比较——就此而言，相对于之前的研究，这些被扩展到（半）开区间。我们提出的判决方法包括预处理给定公式，转换为等价无量词的初等代数公式，其满足性随后可以通过 Tarski 的判决方法来检查。目标公式中不会直接出现函数，每个函数变量都被取代为一组虚拟实变量；因此，为了证明所提出的翻译是满足性保持的，我们必须弄清一个足够灵活的 $C^1$ 函数家族，能够容纳源公式的模型。