The combination of uninterpreted function symbols and universal quantification occurs in many applications of automated reasoning, for example, due to their ability to reason about arrays. Yet the satisfiability of such formulas is, in general, undecidable. In practice, SMT solvers are often successful in the unsatisfiable case, using heuristics. However, in the satisfiable case, they rely on explicit model construction, which fails for formulas whose smallest model is not small enough. We introduce an alternative approach that certifies satisfiability using induction arguments, and apply it to the case of linear integer arithmetic. The resulting algorithm is able to prove satisfiability of formulas that are out of reach for current SMT solvers.

翻译：未解释函数符号与全称量词的结合在自动推理的诸多应用场景中频繁出现，例如因其能够对数组进行推理的特性。然而，此类公式的可满足性在一般情况下是不可判定的。实践中，SMT求解器常能通过启发式方法成功处理不可满足的情形。但对于可满足的情形，现有方法依赖于显式的模型构造，当公式的最小模型规模过大时，该方法将失效。本文提出一种基于归纳论证的可满足性证明替代方案，并将其应用于线性整数算术领域。所得到的算法能够证明当前SMT求解器无法处理的一类公式的可满足性。