Učitavanje video playera...
00:57:20
Vedran Čačić: Ovjereni algoritam za stratifikaciju (2)
Quineova teorija Novih temelja, obogaćena Jensenovim atomima, plodno je tlo za razvoj novih metoda bavljenja matematikom u suradnji čovjeka i računala, budući da objedinjuje ljudsku intuiciju teorije skupova s računalnom strogošću teorije tipova. Osnovni alat za postizanje toga je definicija novih pojmova kao skupova, koristeći komprehenziju po stratificiranim formulama. Ipak, potreba za iteriranjem takve konstrukcije (novi pojmovi često se definiraju koristeći već prethodno definirane pojmove) iziskuje karakterizaciju stratificiranih formula obogaćenih termima dobivenih komprehenzijama.
Tri su uobičajena pristupa: eliminacija (svođenjem na osnovne formule), pridjeljivanje tipova (shvaćajući ih kao nove varijable s posebnim uvjetima stratifikacije) i imenovanje (proširenjem signature novim konstantskim i funkcijskim simbolima). Prije dvije godine pojavila se ideja usklađivanja ta tri pristupa, pokazujući da svi vode do "istog" skupa stratificiranih formula u proširenom jeziku.
Na studijskom boravku u Edinburghu, u suradnji s Markom Dokom razvijen je ovjereni (formalno dokazano korektni) algoritam za stratifikaciju, i dokazano je da (do na zanimljiv izuzetak s konstantskim termima) eliminacija komprehenzijskih terma vodi do istih stratificiranih formula kao njihova tipizacija. Na seminaru će biti prikazani ti rezultati.
