Automated Discovery of Conditional Lemmas in Hipster

dc.contributor.authorLobo Valbuena, Irene
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)sv
dc.contributor.departmentChalmers University of Technology / Department of Computer Science and Engineering (Chalmers)en
dc.description.abstractHipster 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.
dc.subjectData- och informationsvetenskap
dc.subjectComputer and Information Science
dc.titleAutomated Discovery of Conditional Lemmas in Hipster
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster Thesisen
local.programmeComputer science – algorithms, languages and logic (MPALG), MSc
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
1.26 MB
Adobe Portable Document Format