### Skapa referens, olika format (klipp och klistra)

**Harvard**

Johansson, M. (2017) *Automated theory exploration for interactive theorem proving: An introduction to the hipster system*.

** BibTeX **

@conference{

Johansson2017,

author={Johansson, Moa},

title={Automated theory exploration for interactive theorem proving: An introduction to the hipster system},

booktitle={Lecture Notes in Computer Science: 8th International Conference on Interactive Theorem Proving, ITP 2017; Brasilia; Brazil; 26 September 2017 through 29 September 2017},

isbn={978-331966106-3},

pages={1-11},

abstract={Theory exploration is a technique for automatically discovering new interesting lemmas in a mathematical theory development using testing. In this paper I will present the theory exploration system Hipster, which automatically discovers and proves lemmas about a given set of datatypes and functions in Isabelle/HOL. The development of Hipster was originally motivated by attempts to provide a higher level of automation for proofs by induction. Automating inductive proofs is tricky, not least because they often need auxiliary lemmas which themselves need to be proved by induction. We found that many such basic lemmas can be discovered automatically by theory exploration, and importantly, quickly enough for use in conjunction with an interactive theorem prover without boring the user.},

year={2017},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 252360

A1 Johansson, Moa

T1 Automated theory exploration for interactive theorem proving: An introduction to the hipster system

YR 2017

T2 Lecture Notes in Computer Science: 8th International Conference on Interactive Theorem Proving, ITP 2017; Brasilia; Brazil; 26 September 2017 through 29 September 2017

SN 978-331966106-3

SP 1

OP 11

AB Theory exploration is a technique for automatically discovering new interesting lemmas in a mathematical theory development using testing. In this paper I will present the theory exploration system Hipster, which automatically discovers and proves lemmas about a given set of datatypes and functions in Isabelle/HOL. The development of Hipster was originally motivated by attempts to provide a higher level of automation for proofs by induction. Automating inductive proofs is tricky, not least because they often need auxiliary lemmas which themselves need to be proved by induction. We found that many such basic lemmas can be discovered automatically by theory exploration, and importantly, quickly enough for use in conjunction with an interactive theorem prover without boring the user.

LA eng

DO 10.1007/978-3-319-66107-0_1

LK http://dx.doi.org/10.1007/978-3-319-66107-0_1

OL 30