Seminar for
Mathematical Logic
PROGRAM
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
PETAK, 03. jun 2005.G. U 16.15 SATI
PETAK, 10. jun 2005.G. U 16.15 SATI
U Beogradu, 31.05.2005.
Rukovodioci seminara:
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.
Program Seminara za logiku za maj 2005
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.
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.
RAZGOVOR O LOGICKIM PROJEKTIMA
Dr. Djordje Vukomanovic i Dr. Kosta Dosen.