Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
 
 
DownloadE-Mail
 DetailsÜbersicht
  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

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-CF7A-B Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-CF7B-9
Genre: Hochschulschrift

Dateien

einblenden: Dateien
ausblenden: Dateien
:
Masterarbeit-Fulya-Horozal-2007.pdf (beliebiger Volltext), 572KB
 
Datei-Permalink:
-
Name:
Masterarbeit-Fulya-Horozal-2007.pdf
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Eingeschränkt (Max Planck Institute for Informatics, MSIN; )
MIME-Typ / Prüfsumme:
application/pdf
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Horazal, Fulya1, Autor
Siekmann, Jörg2, Ratgeber
Smolka, Gert2, Gutachter
Brown, Chad2, Gutachter
Affiliations:
1International Max Planck Research School, MPI for Informatics, Max Planck Society, Campus E1 4, 66123 Saarbrücken, DE, ou_1116551              
2External Organizations, ou_persistent22              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 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.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2007-072007
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: Saarbrücken : Universität des Saarlandes
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: BibTex Citekey: Horozal2007
 Art des Abschluß: Master

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle

einblenden: