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.
Meeting ID: 858 4037 9195
Strada le Grazie 15
Partita IVA 01541040232
Codice Fiscale 93009870234
© 2022 | Università degli studi di Verona | Credits