This paper describes a generalization of Clark's completion that is applicable to logic programs containing arithmetic operations and produces syntactically simple, natural looking formulas. If a set of first-order axioms is equivalent to the completion of a program then we may be able to find standard models of these axioms by running an answer set solver. As an example, we apply this "reverse completion" procedure to the Sum and Product Puzzle.

翻译：本文提出了一种克拉克完备化的推广形式，该推广适用于包含算术运算的逻辑程序，并能生成句法简洁且形式自然的公式。若一组一阶公理等价于某程序的完备化，则可通过运行回答集求解器来寻找这些公理的标准模型。作为示例，我们将此"逆向完备化"方法应用于和积谜题。