非表示:
キーワード:
-
要旨:
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.
