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

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