Temporal Semantics of Co-Logic Programming

November 11, 2008

Remy Haemmerle


Temporal Semantics of Co-Logic Programming

Time:   11:00am
Location:   Meeting room 302 (Mountain View), level 3

Co-Logic Programming (co-LP) is a paradigm recently introduced that combines both inductive and coinductive logic programming. While semantics of classical LP is based on an induction principle i.e. a least fixpoint computation, coinductive LP is based on an coinduction principle i.e. a greatest fixpoint computation. Some of the promising applications of co-LP are then handling of rational structures, concurrent LP, and model checking of infinite state automata. Because coinductive LP is founded on the perhaps nonintuitive notion of coinduction, it is somehow difficult to apprehend its semantics. It is even more hazardous in the general case of co-LP that nests coinduction with induction, weakening the confidence of a programmer into both co-LP interpreters and co-LP programs.In order to improve intuitive understanding of co-LP we will describe its semantics using mu-calculus, a well-known class of temporal logics with explicit fixpoint operators that generalizes many temporal logics as LTL, CTL and CTL*.