Into the Infinite - Theory Exploration for Coinduction

DOI10.1007/978-3-319-99957-9_5zbMath1515.68343OpenAlexW2888385076MaRDI QIDQ6108814

Johannes Åman Pohjola, Unnamed Author, Moa Johansson

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

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

Related Items (2)

Theory exploration powered by deductive synthesis ⋮ Non-well-founded deduction for induction and coinduction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Conjecture synthesis for inductive theories
• Isabelle/HOL. A proof assistant for higher-order logic
• The generic approximation lemma
• Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
• Proof Relevant Corecursive Resolution
• Truly Modular (Co)datatypes for Isabelle/HOL
• CIRC: A Behavioral Verification Tool Based on Circular Coinduction
• Friends with Benefits
• Concrete stream calculus: An extended study
• A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While
• Coinduction All the Way Up
• Automating Inductive Proofs Using Theory Exploration
• Well-founded recursion with copatterns and sized types
• Quick specifications for the busy programmer
• Hipster: Integrating Theory Exploration in a Proof Assistant

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