For typical first-order logical theories, satisfying assignments have a straightforward finite representation that can directly serve as a certificate that a given assignment satisfies the given formula. For non-linear real arithmetic with transcendental functions, however, no general finite representation of satisfying assignments is available. Hence, in this paper, we introduce a different form of satisfiability certificate for this theory, formulate the satisfiability verification problem as the problem of searching for such a certificate, and show how to perform this search in a systematic fashion. This does not only ease the independent verification of results, but also allows the systematic design of new, efficient search techniques. Computational experiments document that the resulting method is able to prove satisfiability of a substantially higher number of benchmark problems than existing methods.

翻译：对于典型的一阶逻辑理论，满足赋值具有直接的有限表示形式，可直接用作证书来证明给定赋值满足给定公式。然而，对于含超越函数的非线性实数算术，尚无满足赋值的通用有限表示形式可用。因此，本文为该理论引入了一种不同形式的可满足性证书，将可满足性验证问题表述为搜索此类证书的问题，并展示了如何系统化地执行这一搜索过程。这不仅便于对结果进行独立验证，还支持系统化设计新型高效搜索技术。计算实验表明，与现有方法相比，本方法能够证明数量显著更多的基准问题具有可满足性。