论文标题
逻辑程序具有有序分离的强大等效性：逻辑观点
Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective
论文作者
论文摘要
带有有序分离的逻辑程序（LPOD）扩展了经典逻辑程序，并具有在程序规则的负责人中表达优先分离的能力。 LPOD的最初语义虽然简单且直观，但并不是纯粹的模型理论。结果是，程序的某些属性似乎是非平凡的，无法用纯粹的逻辑术语形式化。这种情况的一个例子是表征LPOD的强度等价概念。尽管Faber等人的结果。 （2008年）是准确开发的，在某些特定逻辑中，它们没有将LPOD的强效率表征为逻辑等效性。与Lifschitz等人证明的那样，这与经典逻辑程序的强度相同的众所周知的表征形成鲜明对比。 （2001年），与此处的逻辑相吻合。在本文中，我们获得了纯粹的逻辑表征，将LPOD的强等效性作为四值逻辑中的逻辑等效性。此外，我们提供了一个新的证明，证明了LPOD的强大等价性的综合性，因为它依赖于此类程序的特殊结构，因此对自己的权利产生了兴趣。我们的结果基于Charalambidis等人引入的LPOD的最新逻辑语义。 （2021），我们认为这一事实表明，这种新语义可能被证明是进一步研究LPOD的有用工具。
Logic Programs with Ordered Disjunction (LPODs) extend classical logic programs with the capability of expressing preferential disjunctions in the heads of program rules. The initial semantics of LPODs, although simple and quite intuitive, is not purely model-theoretic. A consequence of this is that certain properties of programs appear non-trivial to formalize in purely logical terms. An example of this state of affairs is the characterization of the notion of strong equivalence for LPODs. Although the results of Faber et al. (2008) are accurately developed, they fall short of characterizing strong equivalence of LPODs as logical equivalence in some specific logic. This comes in sharp contrast with the well-known characterization of strong equivalence for classical logic programs, which, as proved by Lifschitz et al. (2001), coincides with logical equivalence in the logic of here-and-there. In this paper we obtain a purely logical characterization of strong equivalence of LPODs as logical equivalence in a four-valued logic. Moreover, we provide a new proof of the coNP-completeness of strong equivalence for LPODs, which has an interest in its own right since it relies on the special structure of such programs. Our results are based on the recent logical semantics of LPODs introduced by Charalambidis et al. (2021), a fact which we believe indicates that this new semantics may prove to be a useful tool in the further study of LPODs.
