de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Thesis

Towards a Natural Representation of Mathematics in Proof Assistants

MPS-Authors

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

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

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


Cite as: http://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.