Andrej Bauer: Formalizacija realnih števil

Seminar za osnove v akademskem letu 2013/14 začenjamo z manjšo zamudo. Tokrat si bomo ogledali, kako z dokazovalnim pomočnikom Coq formaliziramo realna števila s pomočjo Dedekindove konstrukcije.

Vse konstrukcije realnih števil zahtevajo preverjanje kopice lastnosti, kot je komutativnost in asociativnost aritmetičnih operacij. Učbeniki in matematične monografije skoraj nikoli ne vsebujejo vseh podrobnosti. Namen formalizacije je torej predstaviti celotno konstrukcijo in zares do vseh podrobnosti dokazati, da realna števila tvorijo poln urejen obseg.

Vabljeni!