Coinductive Logic Programming

Coinductive Logic Programming
复制标题

归纳逻辑编程

DOI：
10.1007/11799573_25
复制
发表时间：
2006
期刊：
--
影响因子：
--
通讯作者：
G. Gupta
G. Gupta
中科院分区：
--
文献类型：
--
作者：
Luke Simon;A. Mallya;A. Bansal;G. Gupta

文献摘要

被引文献

相似文献

我们用传统Herbrand语义的语义对偶来扩展逻辑程序设计的语义，用最大不动点代替最小不动点。然后，执行逻辑程序涉及使用余归纳来检查最大定点中的包含。所得到的余归纳逻辑程序设计语言在语法上与逻辑程序设计语言相同，但在语义上包含了逻辑程序设计中的有理术语和懒惰求值。我们提出了一种新的形式化操作语义，它基于对这种共归纳逻辑程序设计语言的一个协归纳假设的综合。我们证明了这种新的操作语义等价于声明性语义。我们的操作语义有助于在存在合理的术语和证据的情况下进行优雅而有效的目标导向的证据搜索。我们描述了这种操作语义的一个原型实现以及协归纳逻辑编程的应用。
We extend logic programming’s semantics with the semantic dual of traditional Herbrand semantics by using greatest fixed-points in place of least fixed-points. Executing a logic program then involves usingcoinductionto check inclusion in the greatest fixed-point. The resultingcoinductive logic programming languageis syntactically identical to, yet semantically subsumes logic programming with rational terms and lazy evaluation. We present a novel formal operational semantics that is based onsynthesizing a coinductive hypothesisfor this coinductive logic programming language. We prove that this new operational semantics is equivalent to the declarative semantics. Our operational semantics lends itself to an elegant and efficient goal directed proof search in the presence of rational terms and proofs. We describe a prototype implementation of this operational semantics along with applications of coinductive logic programming.