Publications
Detailed Information
A Construction of the Reals from an Intuitive and Formal Perspective : 직관적 관점과 형식적 관점에서의 실수 건설
| DC Field | Value | Language |
|---|---|---|
| dc.contributor.advisor | Otto van Koert | - |
| dc.contributor.author | 남도윤 | - |
| dc.date.accessioned | 2023-06-29T02:35:36Z | - |
| dc.date.available | 2023-06-29T02:35:36Z | - |
| dc.date.issued | 2023 | - |
| dc.identifier.other | 000000175912 | - |
| dc.identifier.uri | https://hdl.handle.net/10371/194349 | - |
| dc.identifier.uri | https://dcollection.snu.ac.kr/common/orgView/000000175912 | ko_KR |
| dc.description | 학위논문(석사) -- 서울대학교대학원 : 자연과학대학 수리과학부, 2023. 2. Otto van Koert. | - |
| dc.description.abstract | Based on intuitive facts about a straight line, we define what a straight line is with the help of R. Dedekind. And we introduce a proof assistant program Coq. After that, adding two operations - addition and multiplication to the reals, we show that the reals is a Dedekind-complete ordered field by complementing natural language and Coq. | - |
| dc.description.abstract | 이 논문에서는 리하르트 데데킨트의 업적을 바탕으로 직선에 대한 직관적인 사실에 근거하여 직선이 무엇인지 정의한다. 그리고 증명보조기의 한 예인 Coq를 소개한다. 더불어 직선과 대응하는 대수적 구조인 실수에 두 연산, 덧셈과 곰셈을 정의한다. 마지막으로 이렇게 정의한 실수 구조가 완비순서체임을 Coq를 이용해서 보인다. | - |
| dc.description.tableofcontents | 1. Introduction 1
2. Strengths for using Coq 2 3. Characterization of a straight line 4 3.1 Dense linearly ordered sets without endpoints 4 3.2 Dedekind-complete 7 4. Construction of the reals 1 12 4.1 Existence of the reals 12 4.2 Uniqueness of the reals 16 5. Coq proof checking 1 19 6. Construction of the reals 2 30 6.1 Nested intervals 30 6.2 Addition of nested intervals 35 6.3 Multiplication of nested intervals 35 7. Coq proof checking 2 38 8. Conclusion 50 | - |
| dc.format.extent | iii, 53 | - |
| dc.language.iso | eng | - |
| dc.publisher | 서울대학교 대학원 | - |
| dc.subject | Real numbers | - |
| dc.subject | Dedekind-completeness | - |
| dc.subject | Proof assistant program | - |
| dc.subject | Coq | - |
| dc.subject.ddc | 510 | - |
| dc.title | A Construction of the Reals from an Intuitive and Formal Perspective | - |
| dc.title.alternative | 직관적 관점과 형식적 관점에서의 실수 건설 | - |
| dc.type | Thesis | - |
| dc.type | Dissertation | - |
| dc.contributor.AlternativeAuthor | NAM Doyun | - |
| dc.contributor.department | 자연과학대학 수리과학부 | - |
| dc.description.degree | 석사 | - |
| dc.date.awarded | 2023-02 | - |
| dc.identifier.uci | I804:11032-000000175912 | - |
| dc.identifier.holdings | 000000000049▲000000000056▲000000175912▲ | - |
- Appears in Collections:
- Files in This Item:
Item View & Download Count
Items in S-Space are protected by copyright, with all rights reserved, unless otherwise indicated.