Strong Equivalence Made Easy: Nested Expressions and Weight Constraints

Simple item page
dc.creatorTurner, Hudson
dc.date2003-12-15
dc.date.accessioned2026-07-07T03:20:43Z
dc.date.available2026-07-07T03:20:43Z
dc.descriptionLogic programs P and Q are strongly equivalent if, given any program R, programs P union R and Q union 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 Niemela 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.
dc.identifierhttps://arxiv.org/abs/cs/0312029
dc.identifierhttp://arxiv.org/abs/cs/0312029
dc.identifierTheory and Practice of Logic Programming, vol 3 (4&5), pages 609-622, 2003
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/31927
dc.subjectLogic in Computer Science
dc.subjectArtificial Intelligence
dc.subjectD.1.6
dc.titleStrong Equivalence Made Easy: Nested Expressions and Weight Constraints
dc.typetext

Files

Collections

arXiv