  In the theory of answer set programming, two groups of rules are called
strongly equivalent if, informally speaking, they have the same meaning in any
context. The relationship between strong equivalence and the propositional
logic of here-and-there allows us to establish strong equivalence by deriving
rules of each group from rules of the other. In the process, rules are
rewritten as propositional formulas. We extend this method of proving strong
equivalence to an answer set programming language that includes operations on
integers. The formula representing a rule in this language is a first-order
formula that may contain comparison symbols among its predicate constants, and
symbols for arithmetic operations among its function constants. The paper is
under consideration for acceptance in TPLP.
