Automated Discovery of Conditional Lemmas in Hipster

Examensarbete för masterexamen

Please use this identifier to cite or link to this item:
Download file(s):
File Description SizeFormat 
225866.pdfFulltext1.29 MBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Automated Discovery of Conditional Lemmas in Hipster
Authors: Lobo Valbuena, Irene
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.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2015
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
Collection:Examensarbeten för masterexamen // Master Theses

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.