Theory Exploration on Infinite Structures

Typ
Examensarbete för masterexamen
Master Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2017
Författare
Einarsdóttir, Sólrún Halla
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Data- och informationsvetenskap , Computer and Information Science
Citation
Arkitekt (konstruktör)
Geografisk plats
Byggnad (typ)
Byggår
Modelltyp
Skala
Teknik / material
Index