ὅδε οἶκος, ὦ ἑταῖρε, μνημεῖον ἐστιν ζῴων τῶν σοφῶν ἀνδρῶν, καὶ τῶν ἔργων αὐτῶν

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.