Cyclic (Co)Inductive Reasoning
Ben-Gurion University
Abstract:
Non-well-founded (cyclic) proof theory provides an alternative,
more robust approach for formalizing implicit (co)inductive
reasoning. This approach has been extremely successful in recent
years in supporting implicit inductive reasoning, but is not as
well-developed in the context of coinductive reasoning. In this
talk I will review the general method of non-well-founded proofs,
and put forward a concrete natural framework for (co)inductive
reasoning, based on (co)closure operators. This offers a concise
framework in which inductive and coinductive reasoning are
captured as we intuitively understand and use them. Using this
framework I will aim to demonstrate the enormous potential of
non-well-founded deduction, both in the foundational theoretical
exploration of (co)inductive reasoning and in the provision of
proof support for (co)inductive reasoning within (semi-)automated
proof tools.