
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Multi-Agent Systems and Negotiation · Semantic Web and Ontologies
