Towards a Natural Representation of Mathematics in Proof Assistants

Horozal, Feryal Fulya

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Thesis

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

No external resources are shared

Fulltext (restricted access)

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

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

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

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

Abstract

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.