reprezentacija dokaza, posebno dokaza u supstrukturalnim logikama, u kategorijskim strukturama, i narocito kategorijskim strukturama bliskim geometriji, primena dobijenih rezultata u normalizaciji i odlucivanju jednakosti dokaza, sto je vazno za semantiku programskih jezika, istrazivanja u oblasti prebrojivih struktura (Votova hipoteza), eliminacija kvantifikatora konkretnih struktura, teorija kompaktnih prostora koji se mogu realizovati unutar prve Berove klase realnih funkcija, teorija aproksimativnih homomorfizama
Kategorijska teorija dokaza je disciplina matematicke logike koja koristi teoriju kategorija, jednu vrlo opstu algebarsku disciplinu, da bi pomocu nje opisala logicke sisteme koji se javljaju u teoriji dokaza. Posebno je zanimljivco naci konkretne kategorije koje sluze kao modeli apstraktnih, "sintaksickih", kategorija inspirisanih logikom. Takve konkretne kategorije, koje su cesto geometrijskog tipa, omogucuju da se znatno pojednostavi procedura normalizacije dokaza, i odlucivanje jednakosti dokaza. Te procedure, koje su do sada razvijane u teoriji dokaza i racunu lambda na sintaksicki nacin, su veoma vazne za racunarstvo, zato sto se na osnovu njih prave metode verifikacije korektnosti programa. Savremeni programski jezici zasnivaju se na logickim jezicima, i logicki rezultati se na njih neposredno prenose. Verifikacija programa je vodeci cilj semantike programskih jezika, iz prostog razloga sto se korektnost mnogih programa ne moze empirijski proveravati (na primer kod programa koji mogu ugroziti ljudske zivote). Supstrukturalne logike su jedna familija neklasicnih logika od kojih je najpoznatija linearna logika, inspirisana problemima iz racunarstva. Ove logike imaju posebno zanimljive kategorijske modele, i u ovom istrazivanju koncentrisali bismo se na te modele. (Ovde se radi o modelima za dokaze, a ne modelima za teoreme, u smislu klasicne teorije modela.) Posebno su zanimljivi geometrijski kategorijski modeli koji su u vezi sa skejn prostorima i Temperli-Libovim algebrama. Preko tih modela, pomenuta tema nalazi moguce primene i u kvantnoj fizici. Sadrzaj istrazivanja na projektu bi bio u okviru ovih oblasti a posebno bi se radilo na: koherenciji u bikartezijanskim kategorijama, koherenciji u supstrukturalnim kategorijama, uopstenjima prirodnih transformacija, aksiomatizaciji kategorija spletova (tangles) konacnih i beskonacnih skejn prostora, na njihovoj vezi sa pojmom samoadjungovane situacije, na postovskoj potpunosti monoida i drugih struktura koje se javljaju u tom kontekstu i na matricnoj reprezentaciji Temperli-Libovih algebri i grupa pletenica. Osim toga, istrazivao bi se lambda racun sa tipovima koji ukljucuju i presek tipova. U okviru klasicne teorije modela radilo bi se na Votovoj hipotezi, a u okviru beskonacne kombinatorike na gore pomenutoj teoriji kompaktnih prostora.
Originalan je pokusaj da se u okviru kategorijske teorije dokaza zasnuje geometrijska kategorijska teorija dokaza. To nije samo od teorijskog nego i od prakticnog interesa za verifikaciju programa.
Cilj istrazivanja je pre svega kompletna geometrizacija dokaza, sa njenim originalnim primenama u verifikaciji programa. Jednom ostvaren taj cilj bi bio od dalekoseznog znacaja. Omogucio bi semantici programskih jezika da napusti teren sintaksnih metoda, za koji je do sada bila vezana. Time bi bio prevaljen u obrnutom smeru put koji je u sedamnaestom veku izgradjen u analitickoj geometriji.
Kategorijskom teorijom dokaza se trenutno bavi jedna grupa algebrista i logicara u Americi, najvise u Monrealu, u Kebeku, i jos izvestan broj matematicara u Skotskoj, Australiji, Francuskoj, Rusiji, Italiji i Holandiji. Akcenat na povezivanju kategorijskih istrazivanja sa teorijom dokaza je, medjutim, najnaglaseniji u Monrealu i Beogradu. Supstrukturalnim logikama se bavi mnogo veci broj logicara i informaticara u celom svetu, narocito u Sjedinjenim drzavama, Australiji i Francuskoj. Ta istrazivanja nisu sve do devedesetih godina bila svrstana u istu kategoriju. Objedinjen pristup ovoj oblasti je tekovina devedesetih godina (u klasifikaciji matematickih predmeta Americkog matematickog drustva za 2000. godinu prvi put se pojavljuju dve stavke za supstrukturalne logike, i to 03B47 i 03F52; sam termin "supstrukturalne logike" je inace uveo predlagac ovog projekta 1990. godine). Klasifikacija struktura, drugi tematski okvir ovog projekta, je vodeca tema u klasicnoj teoriji modela, dominantnoj disciplini matematicke logike u drugoj polovini dvadesetog veka. Ona je tesno povezana sa algebrom. Istrazivanja u toj oblasti su pod velikim uticajem izraelskog matematicara Selaha, i na njegov rad se nadovezuju istrazivaci iz mnogih drugih zemalja: Sjedinjenih drzava, Francuske, Rusije, Kanade, itd. Beskonacna kombinatorika je pak jedan od najzivljih izdanaka teorije skupova, discipline koja karakterise matematiku dvadesetog veka.
Stanje istrazivanja u Srbiji u ovim oblastima je na zavidno visokom nivou. Tu se ne radi o prenosenju iskustava iz inostranstva na nas teren, nego u mnogo kom pokledu nasi matematicari predvode istrazivanja. Mnogi od njih su otisli van zemlje ne trbuhom za kruhom, nego zato su trazeni strucnjaci: strancima je potreban njihov rad (koji se u svetu dobro placa). U oblastima koje pokriva ovaj projekat trazi se da se postojeca istrazivanja, koja su vec afirmisana u svetu, jednostavno odrze. Trazi se da beogradske skole kategorijske teorije dokaza, teorije modela i teorije skupova nastave da postoje i zrace u svetu. Njihovo gasenje bi bio veliki gubitak za zemlju, a usteda nikakva.
Opis planiranih rezultata je dat ranije. Medjutim, korisnici tih rezultat se u sadasnjoj fazi ne mogu imenovati. Ti korisnici su i u teorijskim oblastima i u oblastima primenjene matematike. Dosadasnje, veoma dugo, iskustvo u matematici - a nema razloga da verujemo da ce se tu stvari promeniti - uci nas da je izmedju rezultata i njihovih primena potreban period znatno duzi od tri godine, koliko se trazi da ovaj projekat traje.