  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.
