zbMATH — the first resource for mathematics

Foundational (co)datatypes and (co)recursion for higher-order logic. (English) Zbl 06821624
Dixon, Clare (ed.) et al., Frontiers of combining systems. 11th international symposium, FroCoS 2017, Brasília, Brazil, September 27–29, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-66166-7/pbk; 978-3-319-66167-4/ebook). Lecture Notes in Computer Science 10483. Lecture Notes in Artificial Intelligence, 3-21 (2017).
Summary: We describe a line of work that started in 2011 towards enriching Isabelle/HOL’s language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.
For the entire collection see [Zbl 1369.68021].

68Txx Artificial intelligence
Full Text: DOI