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

**Harvard**

Lobo Valbuena, I. (2015) *Automated Discovery of Conditional Lemmas in Hipster*. Göteborg : Chalmers University of Technology

** BibTeX **

@mastersthesis{

Lobo Valbuena2015,

author={Lobo Valbuena, Irene},

title={Automated Discovery of Conditional Lemmas in Hipster},

abstract={Hipster is a tool for theory exploration and automation of inductive proofs
for the proof assistant Isabelle/HOL. The purpose of theory exploration is to
automate the discovery (and proof) of new lemmas of interest within a theory
development, enriching the background theory and providing necessary missing
lemmas that might be required for other automated tactics to succeed.
Hipster has so far succeeded in incorporating automated discovery of equational
conjectures and lemmas. This work presents an extension of Hipster
adding support for conditional lemmas, required, for example, when reasoning
about sorting algorithms and treating different branches of a proof along with
their specific conditions.
The main focus is the implementation of a tactic for automated inductive
proving via recursion induction, accompanied by an evaluation of the tool’s
capabilities. Recursion induction succeeds at automatically proving many of
the discovered conditional conjectures, whereas a previously existing tactic was
unable to. Additionally, recursion induction manages to set up inductive steps in
a proof to render more immediately realisable subgoals by following computation
order. Results show proving capabilities are increased not only with respect to
conditional lemmas but also for more general equational lemmas.},

publisher={Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola},

place={Göteborg},

year={2015},

keywords={conditional lemmas, theory exploration, inductive theorem proving },

note={54},

}

** RefWorks **

RT Generic

SR Electronic

ID 225866

A1 Lobo Valbuena, Irene

T1 Automated Discovery of Conditional Lemmas in Hipster

YR 2015

AB Hipster is a tool for theory exploration and automation of inductive proofs
for the proof assistant Isabelle/HOL. The purpose of theory exploration is to
automate the discovery (and proof) of new lemmas of interest within a theory
development, enriching the background theory and providing necessary missing
lemmas that might be required for other automated tactics to succeed.
Hipster has so far succeeded in incorporating automated discovery of equational
conjectures and lemmas. This work presents an extension of Hipster
adding support for conditional lemmas, required, for example, when reasoning
about sorting algorithms and treating different branches of a proof along with
their specific conditions.
The main focus is the implementation of a tactic for automated inductive
proving via recursion induction, accompanied by an evaluation of the tool’s
capabilities. Recursion induction succeeds at automatically proving many of
the discovered conditional conjectures, whereas a previously existing tactic was
unable to. Additionally, recursion induction manages to set up inductive steps in
a proof to render more immediately realisable subgoals by following computation
order. Results show proving capabilities are increased not only with respect to
conditional lemmas but also for more general equational lemmas.

PB Institutionen för data- och informationsteknik (Chalmers), Chalmers tekniska högskola,

LA eng

LK http://publications.lib.chalmers.se/records/fulltext/225866/225866.pdf

OL 30