On dual programs in co-logic programming and the Horn mu-calculus
On dual programs in co-logic programming and the Horn mu-calculus
复制标题
协同逻辑规划和 Horn mu 演算中的对偶规划
DOI：
10.1007/s00165-016-0404-0
复制
发表时间：
2017
影响因子：
1
通讯作者：
Hirohisa Seki
中科院分区：
文献类型：
--
作者：
Masahiro Nagao;Hirohisa Seki;Hirohisa Seki
我们考虑一些扩展的协同逻辑编程和研究它的关系Horn演算Charatonik等人。首先，我们否定消除（NE），一个熟悉的技术，程序转换，共逻辑程序。给定一个程序P，NE导出它的对偶程序，它定义了P的“补”。当我们应用NE的逻辑程序与否定，我们表明，分层的限制，语法条件施加在逻辑程序，变得过于限制性的一般，霍恩演算可以作为一个扩展的逻辑程序处理“非分层”的逻辑程序。然后，我们考虑一些应用程序的非分层共逻辑程序的良基语义（WFS）和答案集编程。特别是，我们给出了新的迭代不动点特征的WFS以及答案集通过对偶程序。我们还讨论了一些应用程序转换的非分层共逻辑程序，如部分演绎，和WFS的证明过程。
We consider some extensions of co-logic programming and study its relationship with the Horn-calculus by Charatonik et al. We first considernegation elimination (NE), a familiar technique of program transformation, for co-logic programs. Given a programP, NE derives itsdualprogramwhich defines the “complement” ofP. When we apply NE to co-logic programs with negation, we show that the stratification restriction, a syntactic condition imposed on co-logic programs, becomes too restrictive in general, and that the Horn-calculus can be used as an extension of co-logic programming for handling “non-stratified” co-logic programs. We then consider some applications of non-stratified co-logic programs to the well-founded semantics (WFS) and Answer Set Programming. In particular, we give new iterated fixpoint characterizations of the WFS as well as answer sets via dual programs. We also discuss some applications of non-stratified co-logic programs to program transformation such as partial deduction, and a proof procedure for the WFS.