Cited in
(27)- Inductive theorem proving based on tree grammars
- Quick specifications for the busy programmer
- Algorithmic introduction of quantified cuts
- Equivalence checking of two functional programs using inductive theorem provers
- 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
- IsaPlanner
- HipSpec
- Leon
- HR
- Hipster
- Cyclist
- QuickSpec
- InKa
- TIP
- Angelic Verification
- MATHsAiD
- QuodLibet
- TRANSIT
- Recycling proof patterns in Coq: case studies
- Theory exploration powered by deductive synthesis
- Dynamic rippling, middle-out reasoning and lemma discovery
- Automating Event-B invariant proofs by rippling and proof patching
- Hipster: integrating theory exploration in a proof assistant
- Combining induction and saturation-based theorem proving
This page was built for software: IsaCoSy
