Logic, Co-induction and Infinite Computation

Опубликовано 25 июля 2018, 22:29

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.

See more at microsoft.com/en-us/research/v...