Conjecture synthesis for inductive theories
From MaRDI portal
Publication:438543
DOI10.1007/S10817-010-9193-YzbMATH Open1243.68268OpenAlexW2014136929WikidataQ122961283 ScholiaQ122961283MaRDI QIDQ438543FDOQ438543
Authors: Moa Johansson, Lucas Dixon, Alan Bundy 
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/1842/4746
Recommendations
Cites Work
- The TPTP problem library. CNF release v1. 2. 1
- Edinburgh LCF. A mechanized logic of computation
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Title not available (Why is that?)
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theorem Proving in Higher Order Logics
- Experiments with proof plans for induction
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
Cited In (26)
- Equivalence checking of two functional programs using inductive theorem provers
- Algorithmic introduction of quantified cuts
- Into the Infinite - Theory Exploration for Coinduction
- IsaCoSy
- On the generation of quantified lemmas
- A theory of formal synthesis via inductive learning
- A computational framework for conceptual blending
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Proof mining with dependent types
- ASP, amalgamation, and the conceptual blending workflow
- Quantomatic: a proof assistant for diagrammatic reasoning
- Recycling proof patterns in Coq: case studies
- Goal-oriented conjecturing for Isabelle/HOL
- Incorporating hypothetical knowledge into the process of inductive synthesis
- Conjectures, tests and proofs: an overview of theory exploration
- Logic Based Program Synthesis and Transformation
- Dynamic rippling, middle-out reasoning and lemma discovery
- Theory exploration powered by deductive synthesis
- Machine Learning for Inductive Theorem Proving
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Hipster: integrating theory exploration in a proof assistant
- Induction and Skolemization in saturation theorem proving
- Automating Event-B invariant proofs by rippling and proof patching
- Quick specifications for the busy programmer
- Combining induction and saturation-based theorem proving
- Inductive theorem proving based on tree grammars
Uses Software
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)
