Seminar for Mathematical Logic

 

PROGRAM


Plan rada Seminara za logiku za decembar 2012.

Seminar za matematicku logiku Matematickog instituta SANU nastavlja rad u letnjem semestru 2011/2012.g. na ovoj adresi: Kneza Mihaila 36/III sprat, soba 301f - sala za seminare. Cetvrtkom posle podne, ali od 15:00 sati, odrzavace se predavanja na 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, 7.12.2012. U 16:15
Sergej Solovjov, IRIT Touluse
GRAPH TRANSFORMATIONS AND PROOF THEORY

Abstract: In this talk we consider an approach to attributed graph transformations where attributes are logical sequents, lambda-terms, full typing judgements G|- t:A in type theory with inductive types (the latter can be used to model many logical and computational structures). The accent is on possible applications of graphs (instead of trees) to representation of proofs and proof transformations in proof theory, in connection with such problems as equivalence of proofs, categorical semantics and coherence.

PETAK, 21.12.2012. U 16:15 (MI SANU, 301f)
Filip Maric, Miodrag Zivkovic, Bojan Vuckovic, Matematicki fakultet, Beograd
FORMALNA ANALIZA FRANKLOVE HIPOTEZE: FC-FAMILIJE

apstrakt: Franklova hipoteza, postavljena jos 1979. godine, koja je i dalje otvorena, tvrdi da za svaku familiju skupova zatvorenu za unije postoji element koji se javlja bar u pola skupova familije. FC-familije su familije za koje je dokazano da svaka familija zatvorena za unije koja ih sadrzi zadovoljava Franklov uslov (na primer, svaka familija zatvorena za unije koja sadrzi jednoclan skup {a}, je Franklova jer se element a javlja u bar pola skupova te je {{a}} FC familija). FC-familije imaju vaznu ulogu u razresavanju Franklove hipoteze jer omogucavaju znacajno odsecanje prostora pretrage. Predstavljamo formalizaciju pristupa zasnovanog na racunarskoj pretrazi za dokazivanje da je neka familija FC-familija. Koristi se paradigma dokazivanja-putem-izracunavanja i interaktivni dokazivac Isabelle/HOL se koristi da bi se proverio sav matematicki sadrzija i izveo (verifikovanu) kombinatornu pretragu na kojoj se ovi dokazi zasnivaju. Potvrdjene su FC-familije ranije opisane u literaturi i pronadjene su nove FC-familije.

OBAVESTENJA:

Ukoliko zelite mesecne programe ovog Seminara u elektronskom obliku, obratite se: zpetric@mi.sanu.ac.rs ili tane@mi.sanu.ac.rs. Programi svih seminara Matematickog instituta SANU nalaze se na sajtu: www.mi.sanu.ac.rs



Beograd,
Srdacan pozdrav,

rukovodioci seminara Zoran Petric i Predrag Tanovic