Theory Exploration on Infinite Structures

Publicerad

Typ

Examensarbete för masterexamen
Master Thesis

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

item.page.endorsement

item.page.review

item.page.supplemented

item.page.referenced