Here and There with Arithmetic. Issue 6 (23rd November 2021)

• Record Type: Journal Article
• Authors: LIFSCHITZ, VLADIMIR
• Is Part Of: Theory and practice of logic programming. Volume 21:Issue 6(2021)
• Page Start: 735
• Page End: 749
• Publication Date: 2021-11-23
• Subjects: answer set programming -- stable models -- strong equivalence; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068421000338
• Languages: English
• ISSNs: 1471-0684

Abstract

Abstarct: 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.