日本語
 
Help Privacy Policy ポリシー/免責事項
  詳細検索ブラウズ

アイテム詳細

登録内容を編集ファイル形式で保存
一時保存へ追加
 詳細要約
  Towards a Natural Representation of Mathematics in Proof Assistants

Horazal, F. (2007). Towards a Natural Representation of Mathematics in Proof Assistants. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is

 

表示: 全項目 非表示: 全項目

基本情報

表示: 非表示:
アイテムのパーマリンク: https://hdl.handle.net/11858/00-001M-0000-0027-CF7A-B 版のパーマリンク: https://hdl.handle.net/11858/00-001M-0000-0027-CF7B-9
資料種別: 学位論文

ファイル

表示: ファイル
非表示: ファイル
:
Masterarbeit-Fulya-Horozal-2007.pdf (全文テキスト（全般）), 572KB
 
ファイルのパーマリンク:
-
ファイル名:
Masterarbeit-Fulya-Horozal-2007.pdf
説明:
-
OA-Status:
閲覧制限:
制限付き (Max Planck Institute for Informatics, MSIN; )
MIMEタイプ / チェックサム:
application/pdf
技術的なメタデータ:
著作権日付:
-
著作権情報:
-
CCライセンス:
-

関連URL

表示:

作成者

表示:
非表示:
 作成者:
Horazal, Fulya1, 著者
Siekmann, Jörg2, 学位論文主査
Smolka, Gert2, 監修者
Brown, Chad2, 監修者
所属:
1International Max Planck Research School, MPI for Informatics, Max Planck Society, Campus E1 4, 66123 Saarbrücken, DE, ou_1116551              
2External Organizations, ou_persistent22              

内容説明

表示:
非表示:
キーワード: -
 要旨: In this thesis we investigate the proof assistant Scunak in order to explore the relationship between informal mathematical texts and their Scunak counterparts. The investigation is based on a case study in which we have formalized parts of an introductory book on real analysis. Based on this case study, we illustrate significant aspects of the formal representation of mathematics in Scunak. In particular, we present the formal proof of the example lim(1/n) = 0. Moreover, we present a comparison of Scunak with two well-known systems for formalizing mathematics, the Mizar System and Isabelle/HOL. We have proved the example lim(1/n) = 0 in Mizar and Isabelle/HOL as well and we relate certain features of formal mathematics in Mizar and Isabelle/HOL to corresponding features of the Scunak type theory in light of this example.

資料詳細

表示:
非表示:
言語: eng - English
 日付: 2007-072007
 出版の状態: 出版
 ページ: -
 出版情報: Saarbrücken : Universität des Saarlandes
 目次: -
 査読: -
 識別子（DOI, ISBNなど）: BibTex参照ID: Horozal2007
 学位: 修士号 (Master)

関連イベント

表示:

訴訟

表示:

Project information

表示:

出版物

表示: