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.

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