Logic, Co-induction and Infinite Computation

Title: Logic, Co-induction and Infinite Computation
Speaker: Gopal Gupta
Time: 10:00 AM, June 21, 2011
Venue: Lecture Room, Level 3 Building #5, Institute of Software, CAS

Abstract:Coinduction is a powerful technique for reasoning about unfounded sets, unbounded structures, infinite automata, and interactive computations. Where induction corresponds to least fixed points semantics, co-induction corresponds to greatest fixed point semantics. In this talk I will give a tutorial introduction to co-induction and show how co-induction can be elegantly incorporated into logic programming to obtain the co-inductive logic programming (co-LP) paradigm. I will also discuss how co-LP can be elegantly used for sophisticated applications that include (i) model checking and verification, including of hybrid/cyber-physical systems and systems specified using the pi-calculus (ii) planning and goal-directed execution of answer set programs that perform non-monotonic reasoning.

Biography:
Gopal Gupta received his MS and Ph.D. in computer science from the University of North Carolina at Chapel Hill in 1987 and 1991 respectively, and his B. Tech. in Computer Science from IIT Kanpur in 1985. Currently he is Professor and Head of Computer Science at the University of Texas at Dallas. His research interests are in logic programming, programming languages semantics/implementation, and assistive technology. He has published extensively in these areas. He serves as an area editor of the journal Theory and Practice of Logic Programming. He has served in the program committees of numerous conferences, and since January 2010, has served as the President of the Association for Logic Programming. His work on logic programming has been the basis of two tartup companies.