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