Here and There with Arithmetic

TL;DR

This paper extends the method of establishing strong equivalence in answer set programming to languages with integer operations, using propositional formulas and first-order logic.

Contribution

It introduces a way to prove strong equivalence for answer set programs with arithmetic by translating rules into first-order formulas.

Findings

Extended the strong equivalence method to integer operations

Rules are represented as first-order formulas with arithmetic and comparison symbols

Provides a framework for reasoning about answer set programs with arithmetic

Abstract

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.