Hipster: Integrating Theory Exploration in a Proof Assistant

DOI10.1007/978-3-319-08434-3_9zbMath1304.68157arXiv1405.3426OpenAlexW2234299051MaRDI QIDQ5495917

Nicholas Smallbone, Koen Claessen, Moa Johansson, Dan Rosen

Publication date: 7 August 2014

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1405.3426

Mathematics Subject Classification ID

Related Items (10)

Proof mining with dependent types ⋮ Theory exploration powered by deductive synthesis ⋮ TIP: Tons of Inductive Problems ⋮ Automated theory exploration for interactive theorem proving: an introduction to the Hipster system ⋮ Into the Infinite - Theory Exploration for Coinduction ⋮ Quick specifications for the busy programmer ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ Hipster ⋮ Unprovability results for clause set cycles ⋮ Induction and Skolemization in saturation theorem proving

Uses Software

• Isabelle
• Theorema
• Isabelle/HOL
• IsaPlanner
• Metis_
• Sledgehammer
• QuickCheck
• HipSpec
• MaSh
• QuickSpec
• IsaCoSy

Cites Work

• Unnamed Item
• Unnamed Item
• Conjecture synthesis for inductive theories
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Productive use of failure in inductive proof
• Proof-Pattern Recognition and Lemma Discovery in ACL2
• Code Generation via Higher-Order Rewrite Systems
• Automating Inductive Proofs Using Theory Exploration
• MaSh: Machine Learning for Sledgehammer
• Theorem Proving in Higher Order Logics

This page was built for publication: Hipster: Integrating Theory Exploration in a Proof Assistant