IsaCoSy

swMATH44476MaRDI QIDQ5973367FDOQ5973367

Author name not available (Why is that?)

Described by source

• Conjecture synthesis for inductive theories

Cited In (14)

• Equivalence checking of two functional programs using inductive theorem provers
• Algorithmic introduction of quantified cuts
• Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery
• On the generation of quantified lemmas
• A computational framework for conceptual blending
• Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
• Proof mining with dependent types
• Recycling proof patterns in Coq: case studies
• Hipster: Integrating Theory Exploration in a Proof Assistant
• Theory exploration powered by deductive synthesis
• Automating Event-B invariant proofs by rippling and proof patching
• Quick specifications for the busy programmer
• Combining induction and saturation-based theorem proving
• Inductive theorem proving based on tree grammars

This page was built for software: IsaCoSy