Theory Exploration on Infinite Structures
| dc.contributor.author | Einarsdóttir, Sólrún Halla | |
| dc.contributor.department | Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers) | sv |
| dc.contributor.department | Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers) | en |
| dc.date.accessioned | 2019-07-03T14:38:33Z | |
| dc.date.available | 2019-07-03T14:38:33Z | |
| dc.date.issued | 2017 | |
| dc.description.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. | |
| dc.identifier.uri | https://hdl.handle.net/20.500.12380/252478 | |
| dc.language.iso | eng | |
| dc.setspec.uppsok | Technology | |
| dc.subject | Data- och informationsvetenskap | |
| dc.subject | Computer and Information Science | |
| dc.title | Theory Exploration on Infinite Structures | |
| dc.type.degree | Examensarbete för masterexamen | sv |
| dc.type.degree | Master Thesis | en |
| dc.type.uppsok | H | |
| local.programme | Computer science – algorithms, languages and logic (MPALG), MSc |
Ladda ner
Original bundle
1 - 1 av 1
Hämtar...
- Namn:
- 252478.pdf
- Storlek:
- 594.37 KB
- Format:
- Adobe Portable Document Format
- Beskrivning:
- Fulltext