Towards a Natural Representation of Mathematics in Proof Assistants

Horozal, Feryal Fulya

アイテム詳細

登録内容を編集ファイル形式で保存

一時保存へ追加

タグ情報を表示リリース履歴を表示詳細要約

公開

学位論文

Towards a Natural Representation of Mathematics in Proof Assistants

MPS-Authors

/persons/resource/persons44644

Horozal, Feryal Fulya
International Max Planck Research School, MPI for Informatics, Max Planck Society;

External Resource

There are no locators available

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

フルテキスト (公開)

公開されているフルテキストはありません

付随資料 (公開)

There is no public supplementary material available

引用

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

引用: https://hdl.handle.net/11858/00-001M-0000-0027-CF7A-B

要旨

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.