We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover Vampire, extending the successful applicability of first-order proving to program synthesis. This is an extended version of an Automated Deduction -- CADE 29 paper with the same title and the same authors.

翻译：我们提出了一种基于饱和定理证明的自动化推理框架，用于合成无递归程序。给定一个编码为一阶逻辑公式的功能规约，我们使用一阶定理证明器来既验证该公式的有效性，又发现满足规约的程序片段。因此，在推导程序正确性证明的同时，我们还能合成出相对于给定规约正确的程序。我们描述了适用于合成的饱和证明器所应采用的演算性质，并相应地扩展了超归结演算。我们的工作在一阶证明器Vampire中实现，将一阶证明的成功应用扩展到程序合成领域。本文是同名同作者在Automated Deduction – CADE 29会议论文的扩展版本。