Theory Exploration on Infinite Structures

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/252478
Download file(s):
File Description SizeFormat 
252478.pdfFulltext594.37 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Theory Exploration on Infinite Structures
Authors: Einarsdóttir, Sólrún Halla
Abstract: Hipster is a theory exploration system for the interactive theorem prover Isabelle/HOL which has previously been used to discover and prove inductive properties. In this thesis we present our extension to Hipster which adds the capability to discover and prove coinductive properties, allowing the exploration of infinite structures that Hipster could not handle before. We have extended Hipster with a coinductive proof tactic, allowing it to discover and prove coinductive lemmas. As Hipster’s theory exploration relies on generating terms and testing their equality, exploring infinite types whose equality cannot be determined presents a challenge. To solve this we have added support for observational equivalence to test the equivalence of infinite terms. We have evaluated our extension on a number of examples and found that it is capable of proving a variety of coinductive theorems and discovering useful coinductive lemmas. To the best of our knowledge, Hipster is the first theory exploration system to be capable of handling infinite structures and discovering coinductive properties about them.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2017
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/252478
Collection:Examensarbeten för masterexamen // Master Theses



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