Formalizing Relations in Type Theory
| aut.relation.endpage | 162 | |
| aut.relation.issue | 1 | en_NZ |
| aut.relation.journal | Journal of Mathematics and Statistics | en_NZ |
| aut.relation.startpage | 148 | |
| aut.relation.volume | 18 | en_NZ |
| aut.researcher | Kachapova, Farida | |
| dc.contributor.author | Kachapova, F | en_NZ |
| dc.date.accessioned | 2022-10-31T22:35:48Z | |
| dc.date.available | 2022-10-31T22:35:48Z | |
| dc.date.copyright | 2022-10-30 | en_NZ |
| dc.date.issued | 2022-10-30 | en_NZ |
| dc.description.abstract | Type theory plays an important role in the foundations of mathematics as a framework for formalizing mathematics and a base for proof assistants providing semi-automatic proof checking and construction. Derivation of each theorem in type theory results in a formal term encapsulating the whole proof process. This study uses a variant of type theory, namely the Calculus of Constructions with Definitions, to formalize the standard theory of binary relations. This includes basic operations on relations, criteria for special properties of relations, invariance of these properties under the basic operations, equivalence relation, well-ordering, and transfinite induction. Definitions and proofs are presented as flag-style derivations. | |
| dc.identifier.citation | Journal of Mathematics and Statistics, 18(1), 148-162. https://doi.org/10.3844/jmssp.2022.148.162 | |
| dc.identifier.doi | 10.3844/jmssp.2022.148.162 | en_NZ |
| dc.identifier.issn | 1549-3644 | en_NZ |
| dc.identifier.issn | 1558-6359 | en_NZ |
| dc.identifier.uri | https://hdl.handle.net/10292/15568 | |
| dc.publisher | Science Publications | en_NZ |
| dc.relation.uri | https://thescipub.com/abstract/10.3844/jmssp.2022.148.162 | en_NZ |
| dc.rights | © 2022 Farida Kachapova. This is an open access article distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited. | |
| dc.rights.accessrights | OpenAccess | en_NZ |
| dc.subject | Type Theory; Calculus of Constructions; Binary Relation; Transfinite Induction; Flag-Style Derivation | |
| dc.title | Formalizing Relations in Type Theory | en_NZ |
| dc.type | Journal Article | |
| pubs.elements-id | 482127 | |
| pubs.organisational-data | /AUT | |
| pubs.organisational-data | /AUT/Faculty of Design & Creative Technologies | |
| pubs.organisational-data | /AUT/Faculty of Design & Creative Technologies/School of Engineering, Computer & Mathematical Sciences | |
| pubs.organisational-data | /AUT/PBRF | |
| pubs.organisational-data | /AUT/PBRF/PBRF Design and Creative Technologies | |
| pubs.organisational-data | /AUT/PBRF/PBRF Design and Creative Technologies/ECMS PBRF 2018 |