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.
翻译:在回答设定编程理论中,如果非正式地说,这两组规则在任何情况中具有相同的含义,它们被称为“强烈等同”规则。强对等规则与此处和此处的假设逻辑之间的关系使我们能够通过从另一组规则中推导出各组规则来确立强烈等同规则。在这一过程中,规则被改写为“建议公式”。我们将这种证明强烈等同规则的方法推广到包含整数操作的回答设定编程语言。这一语言中代表规则的公式是一种第一级公式,可能包含其前置常数之间的比较符号,以及其函数常数之间的算术操作符号。该文件正在审议供TPLP接受。