IsaCoSy
From MaRDI portal
Cited in
(27)- IsaPlanner
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- A computational framework for conceptual blending
- HipSpec
- Leon
- HR
- Combining induction and saturation-based theorem proving
- Hipster
- Inductive theorem proving based on tree grammars
- Proof mining with dependent types
- Equivalence checking of two functional programs using inductive theorem provers
- On the generation of quantified lemmas
- Cyclist
- Dynamic rippling, middle-out reasoning and lemma discovery
- TIP
- QuickSpec
- InKa
- MATHsAiD
- Angelic Verification
- QuodLibet
- Algorithmic introduction of quantified cuts
- TRANSIT
- Recycling proof patterns in Coq: case studies
- Quick specifications for the busy programmer
- Hipster: integrating theory exploration in a proof assistant
- Automating Event-B invariant proofs by rippling and proof patching
- Theory exploration powered by deductive synthesis
This page was built for software: IsaCoSy
