Automatsko rezonovanje i istraživanje podataka

Istraživanja na projektu biće usmerena na razvoj i primene automatskih dokazivača teorema, formalnog dokazivanja teorema i tehnika istraživanja podataka. Na polju automatskih dokazivača teorema, planira se dalji razvoj SAT rešavača ArgoSAT, razvoj novog SMT rešavača ArgoSMT i novog dokazivača za koherentnu logiku ArgoCLP. Dokazivači ArgoSAT i ArgoSMT biće primenjivani na značajne praktične probleme planiranja, optimizacije, kao i verifikacije softvera. Dokazivač ArgoCLP biće primenjivan u formalizaciji geometrije, u automatskom rešavanju konstruktivnih problema, kao i u okviru geometrijskog softvera GCLC. Na polju formalnog dokazivanja teorema, planira se razvoj verifikovanih programa, kao i formalizacija nekih matematičkih teorija i udžbenika. Planiraju se razvoj i primene novih tehnika istraživanja podataka, od značaja za automatsko rezonovanje ali i za druge oblasti, pre svega bioinformatiku. Te tehnike biće korišćene, između ostalog, za popravljanje efikasnosti i za evaluaciju automatskih dokazivača teorema, za analize genomskih i proteinskih sekvenci i za predikcije nekih neuroloških oboljenja. Planira se publikovanje rezultata istraživanja na konferencijama i u časopisima, organizovanje naučnih seminara i konferencija, kao i održavanje postojećih i uspostavljanje novih saradnji sa drugim istraživačima. Izloženi plan rada je nastavak istraživanja koja su sprovođena u okviru tekućeg projekta 144030.