Into the Infinite - Theory Exploration for Coinduction

DOI10.1007/978-3-319-99957-9_5MaRDI QIDQ6108814zbMATH OpenOpenAlexFDO

Authors Moa Johansson, Johannes Åman Pohjola

Publication date 30 June 2023

Published in Artificial Intelligence and Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-99957-9_5

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
• Hipster: integrating theory exploration in a proof assistant
• Lemma discovery for induction. A survey
• Automating Inductive Proofs Using Theory Exploration
• scientific article; zbMATH DE number 1497748

Cites work

• A Hoare logic for the coinductive trace-based big-step semantics of While
• Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
• Automating Inductive Proofs Using Theory Exploration
• CIRC: A Behavioral Verification Tool Based on Circular Coinduction
• Coinduction All the Way Up
• Concrete stream calculus: an extended study
• Conjecture synthesis for inductive theories
• Foundational nonuniform (co)datatypes for higher-order logic
• Friends with benefits. Implementing corecursion in foundational proof assistants
• Hipster: integrating theory exploration in a proof assistant
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1064116 (Why is no real title available?)
• scientific article; zbMATH DE number 1822263 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Proof relevant corecursive resolution
• Quick specifications for the busy programmer
• The generic approximation lemma
• Truly modular (co)datatypes for Isabelle/HOL
• Well-founded recursion with copatterns and sized types

Cited in

(6)

• Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
• Non-well-founded deduction for induction and coinduction
• Hipster: integrating theory exploration in a proof assistant
• Quantifier-free induction for lists
• Conjectures, tests and proofs: an overview of theory exploration
• Theory exploration powered by deductive synthesis

This page was built for publication: Into the Infinite - Theory Exploration for Coinduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6108814)