de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Hochschulschrift

Towards a Natural Representation of Mathematics in Proof Assistants

MPG-Autoren

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-0027-CF7A-B
Zusammenfassung
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.