Recommendations
Cites work
- scientific article; zbMATH DE number 5909822 (Why is no real title available?)
- scientific article; zbMATH DE number 4072439 (Why is no real title available?)
- scientific article; zbMATH DE number 3754084 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- Edinburgh LCF. A mechanized logic of computation
- Experiments with proof plans for induction
- Isabelle/HOL. A proof assistant for higher-order logic
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- The TPTP problem library. CNF release v1. 2. 1
- Theorem Proving in Higher Order Logics
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
Cited in
(26)- Equivalence checking of two functional programs using inductive theorem provers
- Logic Based Program Synthesis and Transformation
- Quick specifications for the busy programmer
- A theory of formal synthesis via inductive learning
- IsaCoSy
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Dynamic rippling, middle-out reasoning and lemma discovery
- Combining induction and saturation-based theorem proving
- Theory exploration powered by deductive synthesis
- Hipster: integrating theory exploration in a proof assistant
- Induction and Skolemization in saturation theorem proving
- Conjectures, tests and proofs: an overview of theory exploration
- Proof mining with dependent types
- A computational framework for conceptual blending
- Algorithmic introduction of quantified cuts
- Automating Event-B invariant proofs by rippling and proof patching
- Inductive theorem proving based on tree grammars
- On the generation of quantified lemmas
- Goal-oriented conjecturing for Isabelle/HOL
- Quantomatic: a proof assistant for diagrammatic reasoning
- Incorporating hypothetical knowledge into the process of inductive synthesis
- ASP, amalgamation, and the conceptual blending workflow
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Into the Infinite - Theory Exploration for Coinduction
- Recycling proof patterns in Coq: case studies
- Machine Learning for Inductive Theorem Proving
This page was built for publication: Conjecture synthesis for inductive theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438543)
