A biform theory is a combination of an axiomatic theory and an algorithmic
theory. It is used to integrate reasoning and computation in a common theory and
can include algorithms with precisely specified input-output relationships. Isabelle
is one of the leading interactive theorem provers. Isabelle includes locales, a module
system that uses theory morphisms to manage theory hierarchies, and that has a rich
and extensive library with multiple useful proof and formalization techniques. A case
study of eight biform theories of natural number arithmetic is described in the paper
“Formalizing Mathematical Knowledge as a Biform Theory Graph” by J. Carette
and W. M. Farmer. The biform theories form a graph linked by theory morphisms.
Seven of the biform theories are in first-order logic and one is in simple type theory.
The purpose of this thesis is to test how a theory graph of biform theories can be
formalized in Isabelle by attempting to formalize this case study. We work with
locales and sublocales in Isabelle to formalize the test case. The eight biform theories
are defined as regular axiomatic theories, while the algorithms are functions defined
on inductive types representing the syntax of the theories. / Thesis / Master of Science (MSc)
| Identifer | oai:union.ndltd.org:mcmaster.ca/oai:macsphere.mcmaster.ca:11375/28050 |
| Date | January 2022 |
| Creators | Ray, Lekhani |
| Contributors | Farmer, William. M., Computing and Software |
| Source Sets | McMaster University |
| Language | en_US |
| Detected Language | English |
| Type | Thesis |
Page generated in 0.002 seconds