Seminar for
Mathematical Logic
PROGRAM
Plan rada Seminara za logiku za maj 2009.
Seminar za matematicku logiku Matematickog instituta SANU nastavlja rad u letnjem semestru 2008/2009. na novoj adresi: Kneza Mihaila 36/III sprat, soba 305 - Biblioteka instituta. Cetvrtkom posle podne, ali od 14:30 sati, odrzavace se predavanja na pratecem Seminaru iz verovatnosnih logika pod rukovodstvom Profesora Miodraga Raskovica koji je u decembru 2007. dobio akreditaciju Naucnog veca Instituta. Na taj nacin, ponovo, kao pre vise decenija, postoje dva logicka seminara.
Petak, 08.05.2009. U 16:00 sati
Filip Marić (Matematički fakultet Univerziteta u
Beogradu)
Savremeni SAT resavaci (Modern SAT solvers)
Problem ispitivanja iskazne zadovoljivosti (SAT problem) je jedan od
najznacajnijih problema teorijskog racunarstva. U poslednjih
petnaestak godina svedoci smo izuzetno velikog napretka u oblasti
resavanja SAT problema. Danasnji SAT resavaci su u
stanju da ispitaju zadovoljivost KNF formula koje sadrze stotitne
hiljada promenljivih i milione klauza. Zahvaljujuci ovome, SAT
resavaci se uspesno primenjuju u oblastima kao sto su
verifikacija softvera i hardvera, vestacka inteligencija i
optimizacija. U okviru ovog predavanja, ukratko ce biti prikazane
osnove savremenih SAT resavaca. Resavaci ce biti
prikazani u apstraktnom matematickom obliku kao sistemi promena
stanja.
(The propositional satisfiability problem (SAT problem) is one of
the most important problem of theoretical computer science. I the
last fifteen years, we have been witnessing a tremendous advance in
propositional solving technology. State-of-the-art SAT solvers are
capable of checking the satisfiability of CNF formulae with hundreds
thousands of variables and millions of clauses. Thanks to this, SAT
solvers are successfully applied in areas such as software and
hardware verification, artificial intelligence and operational
research. In this talk, basic techniques of state-of-the-art SAT
solvers will be presented. Solvers will be presented in an abstract
mathematical form as state transition systems.)
Petak, 15.05.2009. U 16:15 SATI
Veljko Vujičić (Matematički institut SANU, Beograd)
(Ne)smisao Njutnovih aksioma mehanike po astrofizicarima
(The (non)sense of Newton's axioms according to astrophysicists)
Sadrzaj: Matematicko-logicka struktura nauke o kretanju
tela. Vrednovanje Njutnovih definicija, aksioma i teorema s
dalekoseznim nesaglasnim posledicama u matematickoj fizici.
Nedorecena uopstenja i razgranicenja teorije brojeva,
geometrije i mehanike. "Prostori" koji ne postoje. Matematicko
verovanje u autoritete naspram osmisljavanja opisa realnog sveta.
Petak, 22.05.2009. u 16:15 sati
Filip Marić (Matematički fakultet Univerziteta u Beogradu)
Formalizacija iskazne logike u okviru sistema Isabelle/HOL
(Formalization of Propositional Logic Within the System Isabelle/HOL)
Formalno dokazivanje teorema predstavlja granu matematike koja u
poslednje vreme sve vise dobija na znacaju. Matematicke
teorije se formalizuju u okviru programskih sistema za automatsko i
poluautomatsko formalno dokazivanje teorema i dokazi se izvode tako
da se njihova korektnost proverava uz pomoc racunara, sto
znacajno uvecava veru u njihovu ispravnost. Iako savremeni
alati donose veliki stepen automatizacije u proces dokazivanja, i
dalje je neophodno da znacajne korake u dokazima ljudi manuelno
sprovode. U ovom predavanju ce, kroz primer formalizacije iskazne
logike KNF formula, biti prikazan proces formalnog dokazivanja
teorema u sistemu Isabelle/HOL. Ova formalizacija je deo sireg
projekta formalne verifikacije savremenih SAT resavaca.
(Formal theorem proving is a branch of mathematics that gains in importance in recent times. Mathematical theories are formalized within automatic theorem provers and semiautomatic proof assistants and proofs are constructed so that their correctness can be mechanically checked by computers which significantly increases their level of confidence. Although these state-of-the-art tools introduce significant automatization in the proving process, it is still necessary that many proof steps are manually performed. This talk will present an example formalization of propositional logic for CNF formulae within the proof assistant Isabelle/HOL. This formalization is a part of a wider project of formal verification of state-of-the-art SAT solvers.)
Petak, 29.05.2009. U 16:15 sati
Zoran Petrić (Matematički institut SANU, Beograd)
Trijunkcija (Trijunction)
Trijunkcija je poseban slucaj dvostruke adjunkcije, koju imamo
kod proizvoda i koproizvoda.
(Trijunction is a special case of double adjunction, which we have with products and coproducts.)
Ukoliko zelite mesecne programe ovog Seminara u elektronskom
obliku, obratite se: vdjordje@mi.sanu.ac.rs. Programi svih seminara
Matematickog instituta SANU nalaze se na sajtu: www.mi.sanu.ac.rs
Beograd, 6. februar 2009.g.
Rukovodioci Seminara: Kosta Dosen i Djordje Vukomanovic