Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4942134 | Artificial Intelligence | 2017 | 12 Pages |
Abstract
Strong equivalence is an important concept in the theory of answer set programming. Informally speaking, two sets of rules are strongly equivalent if they have the same meaning in any context. Equilibrium logic was used to prove that sets of rules expressed as propositional formulas are strongly equivalent if and only if they are equivalent in the logic of here-and-there. We extend this line of work to formulas with infinitely long conjunctions and disjunctions, show that the infinitary logic of here-and-there characterizes strong equivalence of infinitary formulas, and give an axiomatization of that logic. This is useful because of the relationship between infinitary formulas and logic programs with local variables.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Artificial Intelligence
Authors
Amelia Harrison, Vladimir Lifschitz, David Pearce, AgustÃn Valverde,