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

Seminar for Mathematical Logic

 

PROGRAM Program Seminara za logiku za maj 2005

Sastanci Seminara za matematicku logiku Matematickog instituta SANU odrzavace se i u akademskoj 2004/2005. godini po pravilu petkom od 16:15 sati u sali 2 na I spratu zgrade SANU, Beograd, Kneza Mihaila 35.

PETAK, 03. jun 2005.G. U 12 SATI
Gerald J. Massey, University of Pittsburgh
SEMANTIC HOLISM: DOES INFERENCE DETERMINE SEMANTICS?

Poslednje iz serije od cetiri predavanja odrzava se u prostorijama Srpskog filozofskog drustva, Cika Ljubina 18-20, staro Kapetan Misino zdanje.

PETAK, 03. jun 2005.G. U 16.15 SATI
Filip Maric, Predrag Janicic (Matematicki fakultet Univerziteta u Beogradu)
ARGOLIB - genericka, objektno-orijentisana platforma za koriscenje procedura odlucivanja u automatskom dokazivanju teorema
(Argolib - a generic, object-oriented platform for decision procedures in automated theorem proving)


Platforma donosi klase za efikasno implementiranje formula/termova visesortne logike prvog reda, implementaciju unifikacije, prezapisivanja termova (ukljucujuci uredjenja svodjenja i algoritme upotpunjavanja), kao i algoritme odredjivanja konstantnog kongruentnog zatvorenja datog skupa jednakosti. Pored ovoga, implementirane su efikasne procedure odlucivanja za nekoliko teorija prvog reda, medju kojima su najznacajnije EUF (cista teorija jednakosti sa neinterpretiranim funkcijskim simbolima), PRA (Pesburgerova racionalna aritmetika) i ARRAYS (ekstenzionalna teorija nizova). Koristeci osnovni skup operacija koje platforma donosi, na jednostavan nacin su implementirane najkoriscenije sheme za kombinovanje procedura odlucivanja medju kojima je najznacajnija Nelson- Oppen-ova, kao i sheme za argumentaciju - prosirivanja domena procedura odlucivanja koriscenjem dodatnih hipoteza (lema). Platforma je projektovana na nacin koji omogucava jednostavnu integraciju u siri dokazivac teorema, imajuci pre svega u vidu dokazivace koji vrse kombinovanje procedura odlucivanja sa tehnikama iskaznog rezonovanja, jer u poslednje vreme ovaj pristup daje najbolje rezultate.

PETAK, 10. jun 2005.G. U 16.15 SATI

RAZGOVOR O LOGICKIM PROJEKTIMA

U Beogradu, 31.05.2005.

Rukovodioci seminara:
Dr. Djordje Vukomanovic i Dr. Kosta Dosen.

Ukoliko zelite da primate mesecni program ovog Seminara elektronskom postom, pisite na adresu: vdjordje@mi.sanu.ac.yu. Inace, programi svih seminara Matematickog instituta SANU mogu se naci na adresi www.mi.sanu.ac.yu. Seminar nastavlja rad u oktobru, ukoliko ne bude vanrednih sastanaka uprilicenih povodom gostovanja stranaca ili nasih ljudi koji zive i rade u inostranstvu.