Co-Logic Programming

Luke Simon, Ajay Bansal, Ajay Mallya and Gopal Gupta Co-Logic Programming: Extending Logic Programming with Coinduction 2007

In this paper we present the theory and practice of co-logic programming (co-LP for brevity), a paradigm that combines both inductive and coinductive logic programming. Co-LP is a natural generalization of logic programming and coinductive logic programming, which in turn generalizes other extensions of logic programming, such as infinite trees, lazy predicates, and concurrent communicating predicates. Co-LP has applications to rational trees, verifying infinitary properties, lazy evaluation, concurrent LP, model checking, bisimilarity proofs, etc.

It is nice to see that coinduction is making its way into Logic Programming.

I couldn't find a free link to this paper [Edit: The link now points directly to the paper], but I found the following useful slides on Gopal Gupta's webpage. Slides from ICLP'07

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Will we be talking about

Will we be talking about this three years from now? I guess it is more like ten.

Why not now?

Circularity and greatest-fixpoints are important tools which make logic programming more useful. As a consequence this paper should be interesting to anyone using logic programming. Without these features things like streams and other infinite co-data structures can not be expressed directly.

But this paper should also be of interest to those who aren't already using logic-programming since new applications become available with these features.

For example, model-checking, since transition systems are very easily expressed in prolog and with the addition of greatest fixpoints, interpreters of temporal logics capable of expressing both liveness and safety properties can be easily encoded.