IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2008 > Temporal Semantics of Co-Logic Programming

Remy Haemmerle

Tuesday, November 11, 2008

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

Remy Haemmerle, Post-doctoral Researcher, CLIP, Technical University of Madrid (UPM), Spain

Temporal Semantics of Co-Logic Programming

Abstract:

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*.