Скачать или смотреть A. Popescu, "Inductive and coinductive theorem proving in Isabelle" VeTSS Summer School 23.

Talk by Andrei Popescu, University of Sheffield, a the VeTSS Summer School, August 2023, University of Surrey.

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus.

Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide. See the Isabelle overview for a brief introduction on this link https://www.cl.cam.ac.uk/research/hvg...

This talk illustrates the induction and coinduction facilities of the Isabelle/HOL proof assistant, covering inductive and coinductive datatypes and predicates, as well as recursion and corecusion.