Program synthesis is the task of automatically deriving a program that has been specified by a user in advance. Combining automated theorem proving with program synthesis enables the automated construction of proven-to-be-correct programs, thereby ensuring software reliability. In this paper, we consider the superposition-based calculus extended to support synthesis of recursion-free programs allowing reasoning with uncomputable symbols. We present cases where the calculus fails and refine it to solve them. We prove that the refined calculus is sound. Finally, we also prove completeness in the following sense: if at least one computable program satisfying the given specification exists, we show that the modified calculus finds one.

翻译：程序合成是自动推导用户预先指定程序的任务。将自动定理证明与程序合成相结合，能够自动构建经证明的正确程序，从而确保软件可靠性。本文研究了扩展至支持无递归程序合成的基于重叠演算系统，该系统允许对不可计算符号进行推理。我们展示了该演算系统失效的情形，并通过改进使其能够解决这些问题。证明了改进后演算系统的可靠性。最后，我们还证明了以下意义上的完备性：若存在至少一个满足给定规范的可计算程序，则该改进演算系统能够发现这样一个程序。