Strong equivalence made easy: Nested expressions and weight constraints

Hudson Turner

Research output: Contribution to journalArticlepeer-review

120 Scopus citations

Abstract

Logic programs P and Q are strongly equivalent if, given any program R, programs P ∪ R and Q ∪ R are equivalent (that is, have the same answer sets). Strong equivalence is convenient for the study of equivalent transformations of logic programs: one can prove that a local change is correct without considering the whole program. Lifschitz, Pearce and Valverde showed that Heyting's logic of here-and-there can be used to characterize strong equivalence for logic programs with nested expressions (which subsume the better-known extended disjunctive programs). This note considers a simpler, more direct characterization of strong equivalence for such programs, and shows that it can also be applied without modification to the weight constraint programs of Niemelä and Simons. Thus, this characterization of strong equivalence is convenient for the study of equivalent transformations of logic programs written in the input languages of answer set programming systems dlv and SMODELS. The note concludes with a brief discussion of results that can be used to automate reasoning about strong equivalence, including a novel encoding that reduces the problem of deciding the strong equivalence of a pair of weight constraint programs to that of deciding the inconsistency of a weight constraint program.

Original languageEnglish (US)
Pages (from-to)609-622
Number of pages14
JournalTheory and Practice of Logic Programming
Volume3
Issue number4-5
DOIs
StatePublished - Jul 2003

Keywords

  • Answer sets
  • Nested expressions
  • Strong equivalence
  • Weight constraints

Fingerprint Dive into the research topics of 'Strong equivalence made easy: Nested expressions and weight constraints'. Together they form a unique fingerprint.

Cite this