IsaCoSy
From MaRDI portal
Software:5973367
No author found.
Related Items (14)
Proof mining with dependent types ⋮ Theory exploration powered by deductive synthesis ⋮ Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ Equivalence checking of two functional programs using inductive theorem provers ⋮ On the generation of quantified lemmas ⋮ Algorithmic introduction of quantified cuts ⋮ Quick specifications for the busy programmer ⋮ Recycling proof patterns in Coq: case studies ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ A computational framework for conceptual blending ⋮ Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery ⋮ Combining induction and saturation-based theorem proving ⋮ Hipster: Integrating Theory Exploration in a Proof Assistant ⋮ Inductive theorem proving based on tree grammars
This page was built for software: IsaCoSy
