English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 DetailsSummary
  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

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-CF7A-B Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-CF7B-9
Genre: Thesis

Files

show Files
hide Files
:
Masterarbeit-Fulya-Horozal-2007.pdf (Any fulltext), 572KB
 
File Permalink:
-
Name:
Masterarbeit-Fulya-Horozal-2007.pdf
Description:
-
OA-Status:
Visibility:
Restricted (Max Planck Institute for Informatics, MSIN; )
MIME-Type / Checksum:
application/pdf
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Horazal, Fulya1, Author
Siekmann, Jörg2, Advisor
Smolka, Gert2, Referee
Brown, Chad2, Referee
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              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2007-072007
 Publication Status: Issued
 Pages: -
 Publishing info: Saarbrücken : Universität des Saarlandes
 Table of Contents: -
 Rev. Type: -
 Identifiers: BibTex Citekey: Horozal2007
 Degree: Master

Event

show

Legal Case

show

Project information

show

Source

show