Search: onr:"swepub:oai:research.chalmers.se:be2553b4-06a2-4241-b965-46bce5d60e4a" >
Hipster: Integratin...
Hipster: Integrating theory exploration in a proof assistant
-
- Johansson, Moa, 1981 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Rosén, Dan, 1988 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Smallbone, Nicholas, 1986 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
show more...
-
- Lindström Claessen, Koen, 1975 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
-
show less...
-
(creator_code:org_t)
- ISBN 9783319084336
- Cham : Springer International Publishing, 2014
- 2014
- English.
-
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319084336 ; 8543, s. 108-122
- Related links:
-
http://publications.... (primary) (free)
-
show more...
-
http://arxiv.org/pdf...
-
https://doi.org/10.1...
-
https://research.cha...
-
show less...
Table of contents
Abstract
Subject headings
Close
No table of content available
- 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.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Publication and Content Type
- kon (subject category)
- ref (subject category)
Find in a library
To the university's database