IsaCoSy

swMATH44476MaRDI QIDQ5973367FDOQ5973367

Author name not available (Why is that?)

Official website: https://www.cse.chalmers.se/~jomoa/papers/ConjSynthesisJAR2011.pdf

Described by source

• Conjecture synthesis for inductive theories

Cited In (26)

• Equivalence checking of two functional programs using inductive theorem provers
• Algorithmic introduction of quantified cuts
• 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
• HipSpec
• Leon
• HR
• Hipster
• Cyclist
• QuickSpec
• InKa
• TIP
• Angelic Verification
• MATHsAiD
• QuodLibet
• TRANSIT
• Recycling proof patterns in Coq: case studies
• Dynamic rippling, middle-out reasoning and lemma discovery
• Theory exploration powered by deductive synthesis
• Hipster: integrating theory exploration in a proof assistant
• 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