Coinduction is a powerful technique for reasoning about unbounded sets, unbounded structures, infinite automata, and interactive computations. Where induction corresponds to least fixed points semantics, coinduction corresponds to greatest fixed point semantics. In this talk I will give a tutorial introduction to coinduction and show how coinduction can be elegantly incorporated into logic programming to obtain the coinductive 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 (ii) planning and goal-directed execution of answer set programs that perform non-monotonic reasoning.