Campus Event Calendar
Event Entry
What and Who
Field: Information Retrieval
Alexandru Chitea
IMPRS
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 6 December 2006
13:00
60 Minutes
E1 4
024
Saarbrücken
Abstract
The notion of formalized mathematics serves a basis for interactive theorem
provers/proof assistants to provide mathematical assistance to their users.
By now there are several systems offering mathematical assistance and
their foundations of formal mathematics vary depending on the formal logic
and the type theory they possess. We present a work on formalizing
mathematics from the field of Real Analysis in the framework of the proof
assistant Scunak [Brown06]. Scunak's foundations of formal mathematics is
set theory encoded in a dependent type theory. We focus on the
characteristics of the formalizations under this new foundation by
illustrating a representative piece of mathematics formalized. We then
present a comparison of the formalizations in Scunak to two other systems:
the Mizar System and the generic proof assistant Isabelle to discuss which
formal approach is more suitable and natural to represent mathematics in
proof assistants.
provers/proof assistants to provide mathematical assistance to their users.
By now there are several systems offering mathematical assistance and
their foundations of formal mathematics vary depending on the formal logic
and the type theory they possess. We present a work on formalizing
mathematics from the field of Real Analysis in the framework of the proof
assistant Scunak [Brown06]. Scunak's foundations of formal mathematics is
set theory encoded in a dependent type theory. We focus on the
characteristics of the formalizations under this new foundation by
illustrating a representative piece of mathematics formalized. We then
present a comparison of the formalizations in Scunak to two other systems:
the Mizar System and the generic proof assistant Isabelle to discuss which
formal approach is more suitable and natural to represent mathematics in
proof assistants.
Contact
IMPRS Office
9325 225
--email hidden
passcode not visible
logged in users only
Andrea Primm, 11/09/2006 15:31
Jennifer Gerling, 10/06/2006 09:53 -- Created document.
Jennifer Gerling, 10/06/2006 09:53 -- Created document.