Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact complete for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explains why they fail when they fail, and the precise role that user help plays in making proofs succeed.

翻译：多种自动验证函数式程序的实用工具（例如，用于Scala程序的Liquid Haskell和Leon）依赖于一种启发式方法，该方法通过展开递归函数定义，然后使用SMT求解器进行无量词推理。我们揭示了该启发式方法的基础理论特性，证明其可以推广并形式化为一种完整的技术，用于对代数数据类型与背景理论的组合一阶理论进行推理，其中背景理论支持可判定的无量词推理。本文发展的理论解释了这些启发式方法成功时的有效性、失败时的原因，以及用户帮助在确保证明成功中的精确作用。