To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Hipster: Integrating theo… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Hipster: Integrating theory exploration in a proof assistant

Conference paper
Authors Moa Johansson
Dan Rosén
Nicholas Smallbone
Koen Claessen
Published in Lecture Notes in Computer Science
Volume 8543
Pages 108-122
ISBN 978-3-319-08433-6
ISSN 0302-9743
Publication year 2014
Published at
Pages 108-122
Language en
Subject categories Computer Science


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.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?