Cyclic (Co)Inductive Reasoning

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.

Link a Zoom

Meeting ID: 858 4037 9195

Passcode: 383761