Advertisement
Published in:
2014 | OriginalPaper | Chapter
Hipster: Integrating Theory Exploration in a Proof Assistant
Authors : Moa Johansson, Dan Rosén, Nicholas Smallbone, Koen Claessen
Published in: Intelligent Computer Mathematics
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
This paper describes Hipster, a system integrating theory exploration with the proof assistant Isabelle/HOL. Theory exploration is a technique for automatically discovering new interesting lemmas in a given theory development. Hipster can be used in two main modes. The first is
exploratory mode
, used for automatically generating basic lemmas about a given set of datatypes and functions in a new theory development. The second is
proof mode
, used in a particular proof attempt, trying to discover the missing lemmas which would allow the current goal to be proved. Hipster’s proof mode complements and boosts existing proof automation techniques that rely on automatically selecting existing lemmas, by inventing new lemmas that need induction to be proved. We show example uses of both modes.