Trustworthy Systems

Into the infinite - theory exploration for coinduction

Authors

Solrun Halla Einarsdottir, Moa Johansson and Johannes Åman Pohjola

DATA61

Chalmers University of Technology

UNSW Sydney

Abstract

Theory exploration is a technique for automating the discovery of lemmas in formalizations of mathematical theories, using testing and automated proof techniques. Automated theory exploration has previously been successfully applied to discover lemmas for inductive theories, about recursive datatypes and functions. We present an extension of theory exploration to coinductive theories, allowing us to explore the dual notions of corecursive datatypes and functions. This required development of new methods for testing infinite values, and for proof automation. Our work has been implemented in the Hipster system, a theory exploration tool for the proof assistant Isabelle/HOL.

BibTeX Entry

  @inproceedings{Einarsdottir_JA_18,
    address          = {Suzhou, China},
    author           = {Einarsdottir, Solrun Halla and Johansson, Moa and {\AA}man Pohjola, Johannes},
    booktitle        = {Artificial Intelligence and Symbolic Computation},
    doi              = {https://doi.org/10.1007/978-3-319-99957-9\_5},
    editor           = {{Fleuriot, Jacques D. and Wang, Dongming and Calmet, Jacques}},
    pages            = {70-86},
    paperurl         = {https://trustworthy.systems/publications/full_text/Einarsdottir_JA_18.pdf},
    publisher        = {Springer},
    series           = {Lecture Notes in Computer Science},
    title            = {Into the Infinite - Theory Exploration for Coinduction},
    volume           = {11110},
    year             = {2018}
  }

Download