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 using coinduction to check inclusion in the greatest fixed-point. The resulting coinductive logic programming language is syntactically identical to, yet semantically subsumes logic programming with rational terms and lazy evaluation. We present a novel formal operational semantics that is based on synthesizing a coinductive hypothesis for 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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Simon, L., Mallya, A., Bansal, A., & Gupta, G. (2006). Coinductive logic programming. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4079 LNCS, pp. 330–345). Springer Verlag. https://doi.org/10.1007/11799573_25
Mendeley helps you to discover research relevant for your work.