The following pages link to IsaCoSy (Q5973367):
Displaying 14 items.
- Algorithmic introduction of quantified cuts (Q402115) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Automating Event-B invariant proofs by rippling and proof patching (Q667526) (← links)
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (Q1640636) (← links)
- A computational framework for conceptual blending (Q1748468) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- Inductive theorem proving based on tree grammars (Q2344621) (← links)
- Proof mining with dependent types (Q2364689) (← links)
- Equivalence checking of two functional programs using inductive theorem provers (Q2410575) (← links)
- On the generation of quantified lemmas (Q2417949) (← links)
- Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery (Q3058453) (← links)
- Quick specifications for the busy programmer (Q5371995) (← links)
- Hipster: Integrating Theory Exploration in a Proof Assistant (Q5495917) (← links)
