Andrej Bauer: Formalizacija realnih števil

Datum objave: 28. 10. 2013
Seminar za temelje matematike in teoretično računalništvo
Torek, 29. 10. 2013, od 12h do 14h, Plemljev seminar, Jadranska 19

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!