DC FieldValueLanguage
dc.contributor.author賴廷彥zh_TW
dc.contributor.author穆信成zh_TW
dc.contributor.author楊武zh_TW
dc.contributor.authorLuā, Tîng-Giānen_US
dc.contributor.authorMu, Shin-Chengen_US
dc.contributor.authorYang, Wuuen_US
dc.date.accessioned2018-01-24T07:39:14Z-
dc.date.available2018-01-24T07:39:14Z-
dc.date.issued2017en_US
dc.identifier.urihttp://etd.lib.nctu.edu.tw/cdrfb3/record/nctu/#GT070356008en_US
dc.identifier.urihttp://hdl.handle.net/11536/140398-
dc.description.abstract日常生活中充滿了數值，而位值計數系統是最常見的數值表示方式。 在這篇論文中我們探討並研究各種計數系統的有趣性質與應用，並且在 Agda 裡去建構並且驗證我們發展的一種一般化位值計數系統的方法。我們不只會去探索我們的計數系統與皮亞諾公理的自然數之間的關係，也會發展一套方法去自動轉換彼此之間的定理與證明。zh_TW
dc.description.abstractNumbers are everywhere in our daily lives, and positional numeral systems are arguably the most important and common representation of numbers. In this work, we will investigate interesting properties and applications of some variations of positional numeral systems and construct a generalized positional numeral system to model and formalize them in Agda. We will not only examine properties of our representation and its relationship with the classical unary representation of natural numbers but also demonstrate how to translate propositions and proofs between them.en_US
dc.language.isoen_USen_US
dc.subject構造性數學zh_TW
dc.subject計數系統zh_TW
dc.subject定理證明zh_TW
dc.subject一階邏輯zh_TW
dc.subjectAgdazh_TW
dc.subjectConstructive mathematicsen_US
dc.subjectNumeral systemsen_US
dc.subjectTheorem provingen_US
dc.subjectAgdaen_US
dc.subjectFirst-order logicen_US
dc.title一般化位值計數系統zh_TW
dc.titleGeneralizing Positional Numeral Systemsen_US
dc.typeThesisen_US
dc.contributor.department資訊科學與工程研究所zh_TW
Appears in Collections:Thesis