Hostname: page-component-7b7567c8c-fvjsw Total loading time: 0 Render date: 2026-11-15T20:23:51.240Z Has data issue: false hasContentIssue false

Strong equivalence made easy: nested expressions andweight constraints

Published online by Cambridge University Press:  31 July 2003

HUDSON TURNER
Affiliation:
Computer Science Department, University of Minnesota, Duluth, MN, USA (e-mail: hudson@d.umn.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Logic programs $P$ and$Q$ are stronglyequivalent if, given any program $R$, programs $P\cup R$ and $Q \cupR$ are equivalent (that is, have the sameanswer sets). Strong equivalence is convenient for the study ofequivalent transformations of logic programs: one can prove that alocal change is correct without considering the whole program.Lifschitz, Pearce and Valverde showed that Heyting's logic ofhere-and-there can be used to characterize strong equivalence forlogic programs with nested expressions (which subsume thebetter-known extended disjunctive programs). This note considers asimpler, more direct characterization of strong equivalence for suchprograms, and shows that it can also be applied without modificationto the weight constraint programs of Niemelä and Simons. Thus, thischaracterization of strong equivalence is convenient for the studyof equivalent transformations of logic programs written in the inputlanguages of answer set programming systems dlv and SMODELS. The noteconcludes with a brief discussion of results that can be used toautomate reasoning about strong equivalence, including a novelencoding that reduces the problem of deciding the strong equivalenceof a pair of weight constraint programs to that of deciding theinconsistency of a weight constraint program.

Information

Type
Regular Papers
Copyright
© 2003 Cambridge University Press