Conjecture synthesis for inductive theories

DOI10.1007/s10817-010-9193-yzbMath1243.68268OpenAlexW2014136929WikidataQ122961283 ScholiaQ122961283MaRDI QIDQ438543

Moa Johansson, Alan Bundy, Lucas Dixon

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

zbMATH Keywords

synthesistheorem provinginductiontheory formationlemma discovery

Mathematics Subject Classification ID

Related Items (21)

Proof mining with dependent types ⋮ Theory exploration powered by deductive synthesis ⋮ ASP, Amalgamation, and the Conceptual Blending Workflow ⋮ Quantomatic: A Proof Assistant for Diagrammatic Reasoning ⋮ 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 ⋮ Automated theory exploration for interactive theorem proving: an introduction to the Hipster system ⋮ Into the Infinite - Theory Exploration for Coinduction ⋮ Machine Learning for Inductive Theorem Proving ⋮ 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 ⋮ IsaCoSy ⋮ Hipster: Integrating Theory Exploration in a Proof Assistant ⋮ Induction and Skolemization in saturation theorem proving ⋮ Inductive theorem proving based on tree grammars

Uses Software

• Isabelle
• Theorema
• IsaPlanner
• TPTP
• HR
• MATHsAiD

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Experiments with proof plans for induction
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• The TPTP problem library. CNF release v1. 2. 1
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Theorem Proving in Higher Order Logics

This page was built for publication: Conjecture synthesis for inductive theories