Projekat 144013

Reprezentacije logičkih struktura i njihove primene u računarstvu

Rukovodilac: dr Zoran Ognjanović

Rezime

U poslednjih nekoliko decenija matematička logika je postala račun računarstva i veštačke inteligencije, a takođe pružila i teorijske osnove za mnoge njihove oblasti. Prateći ta dostignuća, u ovom projektu će biti sprovedena istraživanja koja će biti interesantna i sa teorijskog aspekta razvoja logike i sa aspekta razvoja oruđa za reprezentovanje i rezonovanje o značajnim konceptima izračunavanja: geometrijska reprezentacija dokaza i teorija kategorija sa primenama u semantici programskih jezika, model-teorijska i dokazno-teorijska analiza matematičkih logika za računarstvo koje su pogodne da daju teorijsku osnovu za za sve šire inteligentno rezonovanje koje zahtevaju realni problemi koje ljudi pokušavaju da reše pomoću računara kada je znanje nekompletno i/ili neizvesno (na primer: verovatnosne logike, konzervativna uopštenja klasične do [0,1]-vrednosne logike), razvoj odgovarajućih potpunih i polupotpunih procedura odlučivanja, procedura za aproksimativno rezonovanje, dokazivača teorema i drugih sistema za formalno rezonovanje sa primenama kod sistema za podršku donošenja odluka, reprezentacija i klasifikacija različitih algebarskih struktura itd.

Predmet istraživanja

U poslednjih nekoliko decenija matematička logika je postala račun računarstva i veštačke inteligencije, a takođe pružila i teorijske osnove za mnoge njihove oblasti. Prateći ta dostignuća, u ovom projektu će biti sprovedena istraživanja koja će biti interesantna i sa teorijskog aspekta razvoja logike i sa aspekta razvoja oruđa za reprezentovanje i rezonovanje o značajnim konceptima izračunavanja:

Opis i značaj istraživanja

Prvi deo projektnih aktivnosti odnosi se na kategorijalnu teoriju dokaza koja opisuje logičke sisteme koji se javljaju u teoriji dokaza. Posebno je interesantno pronaći konkretne kategorije koje služe kao modeli apstraktnih, "sintaksnih", kategorija inspirisanih logikom. Takve kategorije pojednostavljuju procedure normalizacije dokaza i procedure koje odlučuju jednakost dokaza. Ove procedure, koje su do sada razvijane na sintaksnim principima u teoriji dokaza i lambda računu, su značajne u računarstvu jer mogu poslužiti za izgradnju metoda za verifikaciju korektnosti programa, što je jedan od glavnih ciljeva semantike programskih jezika pošto se za većinu programa korektnost ne može ustanoviti empirijski. Familija neklasičnih logika pod imenom substrukturalne logike ima posebno značajne kategorijalne modele i mi ćemo se koncentrisati na njih. Geometrijski kategorijalni modeli su u vezi sa skejn prostorima i Temperli-Libovim algebrama i mogu imati primene u kvantnoj mehanici. Istraživanje će biti koncentrisano na sledeće teme: koherencija u bikartezijanskim kategorijama, koherencija u supstrukturalnim kategorijama, uopštenja prirodnih transformacija, aksiomatizacija kategorija spletova konačnih i beskonačnih skejn prostora i njihova veza sa pojmom samoadjungovane situacije, na postovskoj potpunosti monoida i drugih struktura koje se javljaju u tom kontekstu i na matričnoj reprezentaciji Temperli-Libovih algebri i grupa pletenica. U klasičnoj teoriji modela, radiće se na klasifikaciji prebrojivih struktura prvog reda. Biće istraživani i sistemi sa algebarskim aspektima, poput reprezentacije i klasifikacije algebarskih struktura (grupoidi i semigrupe) i opisivanje opštih i reproduktivnih rešenja sistema Bulovih (ne)jednačina i jednačina u Stonovim algebrama.

Drugi deo projektnih aktivnosti odnosi se na izučavanje sistema koji prevazilaze klasičnu iskaznu i predikatsku logiku, što uključuje logike za neizvesno i nemonotono rezonovanje, modalne logike itd., sa idejom da se obezbede logički sistemi dovoljno izražajni da pruže teorijsku osnovu za sve šire inteligentno rezonovanje koje zahtevaju problemi koje ljudi rešavaju pomoću računara (baze podataka, internet agenti sposobni za autonomni rad u složenim i nepredvidivim uslovima itd.). Posebno ćemo proučavati verovatnosne logike u kojima je moguće iskazati rečenice o verovatnoći, a takođe su pogodne i za modeliranje nemonotonog zaključivanja. Analiziraće se glavne osobine tih sistema (potpunost, odlučivost, složenost). Razmatraće se problemi kombinovanja i integrisanja procedura odlučivanja u dokazivače teorema. Biće istraživani stohastički ultra-grafovi i njihove primene na samoorganizujuće skupove distribuiranih agenata.

Očekivani rezultati