Projekat 174026
Reprezentacije logičkih struktura i formalnih jezika i njihove primene u računarstvu
Rukovodilac: profesor Silvia Ghilezan
Rezime
Matematička logika obuhvata matematička istraživanja logičkih sistema i primene formalne logike na ostale oblasti matematike. Pored svoje fundamentalne uloge u razvoju matematike, u poslednjih nekoliko decenija matematička logika postaje teorijska osnova računarstva i veštačke inteligencije. Istraživanja u ovom projektu će biti usmerena ka fundamentalnim istraživanjima i relevantnim primenama u računarstvu.
Osnovni istraživački pravci projekta će biti:
(a) Reprezentacija logičkih struktura,
(b) Spektralne reprezentacije diskretnih funkcija i
(c) Logički i formalni sistemi za sekvencijalno i distribuirano računarstvo.
Teme istraživanja na projektu će biti:
(a) Koherencijski rezultati za kategorije u teoriji dokaza, srodni rezultati za algebru, geometriju i topologiju. Model-teoretska i dokaz-teoretska analiza logičkih sistema. Sistemi za aproksimativno i formalno rezonovanje. Reprezentacija i klasifikacija algebarskih struktura.
(b) Primene algebarskih struktura u predstavljanju diskretnih signala sa primenama u modeliranju i opisivanju digitalnih sistema. Spektralne reprezentacije digitalnih sistema i njihova složenost.
(c) Računarske interpretacije logičkih sistema za sekvencijalno računarstvo. Formalni modeli distribuiranih računarskih sistema.
Sveobuhvatni istraživački tim ima istaknute naučne rezultate prepoznatljive u međunarodnom naučnom okruženju. Istraživači su uključeni u rad evropskih naučnih projekata, što će omogućiti uključivanje rezultata projekta u aktuelna međunarodna istraživanja.
Opis projekta
Istraživanja u ovom projektu će biti usmerena ka funadamentalnim istraživanjima u svim osnovnim oblastima matematičke logike: teoriji dokaza, teoriji modela, teoriji skupova, teoriji tipova, kao i ka relevantnim primenama logike u računarstvu i logičkom dizajnu. Projekat obuhvata povezana istraživanja i aktivnosti na tri potprojekta:
(a) Reprezentacija logičkih struktura sa primenama,
(b) Spektralne reprezentacije diskretnih funkcija i njihova primena i
(c) Logički i formalni sistemi za sekvencijalno i distribuirano računarstvo.
Osnovni istraživački pravci potprojekata će biti:
(a) Reprezentacija logičkih struktura sa primenama - rukovodilac potprojekta Z. Petrić.
- Fundamentalna istraživanja na ovom i ostalim potprojektima će biti u svim osnovnim oblastima matematičke logike: teoriji dokaza, teoriji modela, teoriji skupova, teoriji tipova i sistemima za formalno rezonovanje. Prateći najsavremenija dostignuća, u ovom projektu će biti sprovedena istraživanja značajna i sa teorijskog aspekta razvoja logike i sa aspekta njene primene u reprezentovanju i rezonovanju o važnim konceptima matematike i računarstva. Kategorijalna teorija dokaza, posebno koherencijski rezultati u teoriji kategorija, kao i srodni rezultati interesantni za algebru, geometriju i topologiju. Primene van oblasti logike, u teoriji politipova i semantici dokaza. Model-teoretska i dokaz-teoretska analiza sistema za različite fragmente intuicionističke, klasične, intermedijalnih, substrukturalnih i verovatnosnih logika. Procedure za aproksimativno rezonovanje i sistemi za formalno rezonovanje sa primenama kod sistema za podršku donošenja odluka. Reprezentacija i klasifikacija različitih algebarskih beskonačnih i konačnih struktura. Algebarske teorije kvazi grupa i sistema jednačina i nejednačina u Bulovim i Postovim algebrama.
(b) Spektralne reprezentacije diskretnih funkcija i njihova primena - rukovodilac potprojekta R. Stanković.
- Mnogi savremeni digitalni sistemi se mogu posmatrati kao organizovani skupovi posebno i svrsishodno izabranih algoritama za obradu signala koji su međusobno tako povezani da izvršavaju različite složene zadatke. Osnovne manje celine (blokovi) u ovakvim sistemima, kao i algoritmi, postaju sve složeniji i složeniji, a specificiranje veza između njih u smislene sisteme zahteva nove strukture podataka, kakvi su, na primer, dijagrami odlučivanja, kao i na njima zasnovane posebne metode obrade podataka. Da bi se moglo odgovoriti zahtevima složenosti sistema, neophodno je da nivo apstrakcije u modeliranju i opisivanju digitalnih sistema radi njihove implementacije bude visok. Na tom nivou apstrakcije koriste se složene algebarske strukture za precizno modeliranje i istovremeno kompaktan opis digitalnih sistema. Osnovni zadatak u ovom području biće posvećen primeni različitih algebarskih struktura u predstavljanju diskretnih signala sa primenama u modeliranju i opisivanju digitalnih sistema. Nameravamo da ispitujemo spektralne reprezentacije, kako na nivou bitova, tako i na nivou reči (u računaru) na konačnim grupama. Istraživački zadatak je pronaći koje od struktura i reprezentacija su najpogodnije za zadatu konkretnu primenu.
(c) Logički i formalni sistemi za sekvencijalno i distribuirano računarstvo - rukovodilac potprojekta J. Pantović.
- Formalni sistemi matematičke logike predstavljaju teorijsku osnovu računarstva. Matematička osnova za mnoge sekvencijalne programske jezike je lambda račun, čije važne primene uključuju verifikaciju softvera i kompleksnih informacionih sistema. Glavni cilj istraživanja su računarske interpretacije intucionističke, klasične logike, substrukturalnih, intermedijalnih i verovatnosnih logika. Glavni cilj projekta u oblasti razvoja formalizama za konkurentne procese je analiza i unapređivanje postojećih i razvoj novih formalnih modela distribuiranih sistema kao što su web aplikacije i servisi. Jedan od osnovnih koraka u upravljanju distribuiranim sistemima je administriranje prava pristupa podacima u tim mrežama. Kontrola prava pristupa bazirana na ulogama je tehnologija koja se oslanja na pojam uloga, poznatom standardu u domenu bezbednosti informacionih sistema. Naš istraživački tim, primenom metoda teorije tipova razvija sisteme za dinamičko modeliranje kontrole prava pristupa u mrežama bazirane na ulogama. U daljem radu ćemo unapređivati postojeće i razvijati nove sisteme sa kontrolom prava pristupa web servisima i ispitivati moguća pojednostavljenja koja neće dovesti do gubitka ekspresivnosti.
Fundamentalna istraživanja potprojekta (a) će biti koordinisana sa primenjenim istraživanjima u potprojektima (b) i (c), čiji će rezultati, zauzvrat, motivisati nova fundamentalna istraživanja.
Očekivani ključni rezultati
Istraživanja u ovom projektu su usmerena ka fundamentalnim istraživanjima u svim ključnim oblastima matematičke logike i ka relevantnim primenama u računarstvu. Očekivani rezultati su:
(a) Reprezentacije logičkih stuktura sa primenama:
- Koherencijski rezultati za kategorije u teoriji dokaza. Srodni rezultati za algebru, geometriju i topologiju
- Novi pristup semantici dokaza u klasičnoj logici
- Eliminacije sečenja u sekventnim sistemima i maksimalni segmenti u prirodno-dedukcijskim sistemima
- Potpunost, odlučivost i kompleksnost logičkih sistema za rezonovanje u odsustvu informacija, verovatnosnih, temporalnih i drugih modalnih logika
- Cilindrične i verovatnosne algebre
- Karakterizacija parcijalno uređenih skupova sa verovatnosnim merama
- Klasifikacija prebrojivih struktura
- Strukturni opis, tračna i polumrežna razlaganja novih klasa polugrupa
- Jednačine i nejednačine u viševrednosnim logikama, Bulovim, Postovim i Stonovim algebrama
- Teorija uređenja u Bišopovoj konstruktivnoj matematici
- Metoda tabloa za modalne i substrukturalne logike sa primenama u automatskom dokazivanju
- Klase kvazi grupa sa primenama u šifrovanju
(b) Spektralna reprezentacija diskretnih funkcija i njihova primena:
- Modeliranje i opisivanje digitalnih sistema primenom algebarskih struktura
- Spektralne reprezentacije na konačnim grupama
- Složenost reprezentacije
- Veza strukture i reprezentacije za konkretnu primenu
- Optimizacija modeliranja i projektovanja digitalnih sistema i regularnost struktura
- Brzi algoritmi za računanje na velikim diskretnim funkcijama
(b) Logički i formalni sistemi za sekvencijalno i distribuirano računarstvo:
- Kontrola resursa u intuicionističkoj logici
- Dijagramatska reprezentacija dokaza
- Nove računarske interpretacije substrukturnih, intermedijalnih i verovatnosnih logika
- Terminacija predloženih sistema
- Kontrola bezbednosti i pouzdanosti u distribuiranim sistemima
- Kontrola prava pristupa podacima pomoću uloga
- Razvoj tipskih sistema i metoda teorije tipova za kontrolu bezbednosti komunikacije
- Opis ponašanja sistema pomoću odgovarajućih relacija ekvivalencije
Značaj predloženog istraživanja
Predložene istraživačke teme obuhvataju veoma širok spektar fundamentalnih istraživanja u matematičkoj logici u svim osnovnim oblastima: teoriji dokaza, teoriji modela, teoriji skupova, teoriji tipova. Njihova primenjivost je ugrađena u osnove računarstva, programskih jezika, veštačke inteligencije, verifikacije softvera, logičkog dizajna, a takođe i razvija nove koncepte računarstva kao što su paralelnost i konkurentnost. Aktivan rad međunarodnih naučno-istraživačkih timova u okviru svih projektnih tema ilustruje aktuelnost predloženog projekta. Sveobuhvatni tim ovog projekta, preko 40 istraživača, je sačinjen od istraživača sa jedinog istraživačkog matematičkog instituta u Srbiji i od istraživača sa sva četiri najveća državna univerziteta u Srbiji: univerziteta u Beogradu, Novom Sadu, Nišu i Kragujevcu. Renomirani tim ima istaknute naučne rezultate prepoznatljive u međunarodnom naučnom okruženju. Značajan je broj mladih istraživača, više od 20%, koji započinju istrazivački rad u ovom timu. Istraživači su uključeni u rad evropskih naučnih projekata, kao što su FP, COST, bilateralni i multilateralni projekti, što će osigurati uključivanje rezultata projekta u aktuelna međunarodna istraživanja. U radu projekta će učestvovati tri istaknuta naučnika iz insotranstva S. Krstić (Intel, SAD), I.Farah (Univerzitet u Torontu, Kanada) i V. Kunčak (EPFL, Švajcarska), koji su svoja prva istraživanja započeli u Beogradu i Novom Sadu. Njihove ekpertize će doprineti značaju projekta. Značajan aspekt je i nastavak i proširivanje međunarodne naučno-istraživačke saradnje sa renomiranim stručnjacima sa vodećih univerziteta, Univerzitet Paris 7, EPFL Lozana, Univerzitet u Torontu, Torinu, Firenci, ENS Lion, Ecole Polytechnique Pariz, McGill University Montreal, Univerzitet Tampere, kao i sa renomiranim istraživačima iz istraživačkog centra INRIA-Sophia Antipolis, Francuska i razvojne kompanije Intel SAD.
