Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/26272
Title: | Leveraging Information Contained in Theory Presentations |
Authors: | Sharoda, Yasmine |
Advisor: | Carette, Jacques Farmer, William |
Department: | Computer Science |
Keywords: | formal methods;algebra library;theorem provers;theory development |
Publication Date: | 2021 |
Abstract: | Building a large library of mathematical knowledge is a complex and labour-intensive task. By examining current libraries of mathematics, we see that the human effort put in building them is not entirely directed towards tasks that need human creativity. Instead, a non-trivial amount of work is spent on providing definitions that could have been mechanically derived. In this work, we propose a generative approach to library building, so definitions that can be automatically derived are computed by meta-programs. We focus our attention on libraries of algebraic structures, like monoids, groups, and rings. These structures are highly inter-related and their commonalities have been well-studied in universal algebra. We use theory presentation combinators to build a library of algebraic structures. Definitions from universal algebra and programming languages meta-theory are used to derive library definitions of constructions, like homomorphisms and term languages, from algebraic theory presentations. The result is an interpreter that, given 227 theory expressions, builds a library of over 5000 definitions. This library is, then, exported to Agda and Lean. |
URI: | http://hdl.handle.net/11375/26272 |
Appears in Collections: | Open Access Dissertations and Theses |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Sharoda_Yasmine_2021March_PhD.pdf | 1.82 MB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.