简化强等价性：嵌套表达式和权重约束
Strong Equivalence Made Easy: Nested Expressions and Weight Constraints
摘要：
逻辑程序P和Q是强等价的，如果给定任何程序R，程序P并集R和程序Q并集R是等价的（即，具有相同的答案集）。强等价性便于研究逻辑程序的等价变换：人们可以证明一个局部变换是正确的，而不需要考虑整个程序。Lifschitz，Pearce和Valverde证明了Heyting的Here-and-There逻辑可以用来刻画带有嵌套表达式的逻辑程序的强等价性（它取代了更著名的扩展析取程序）。本文考虑了这类程序强等价性的一个更简单、更直接的特征，并表明它也可以不加修改地应用于Niemela和Simons的权约束程序。因此，强等价性的这一特征便于研究用回答集程序设计系统dlv和smodels的输入语言编写的逻辑程序的等价变换。该说明的结论是一个简短的讨论的结果，可用于自动推理强等价，包括一种新的编码，减少了问题的决定强等价的一对权重约束程序的决定不一致的权重约束程序。
英文摘要：
Logic 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
