Seminar za matematičku logiku i osnove matematike

 

Važno: za prijavu seminara je potrebno priložiti kratki abstract!

Sljedeći termin:

(nije dogovoren)

Seminari održani prošle akademske godine (2007./08.):

"Uvrnuti" teorem Čebotareva

7. srpnja 2008. — Ivan Tomašić, University of Queen Mary, London

Poznati teorem koji je Čebotarev nazivao svojim najboljim teoremom
je rezultat o poljima brojeva. Naravno, postoji i analogon za polja
funkcija, koji može poslužiti za prebrojavanje točaka na specijalnim
(definabilnim) podskupovima algebraskih mnogostrukosti nad konačnim
poljima.
Bit će izloženo poopćenje tog rezultata koje služi za određivanje broja
točaka na specijalnim (definabilnim) podskupovima diferencijskih
mnogostrukosti nad poljima s potencijama Frobeniusovog automorfizma. Ti se podskupovi mogu izraziti pomoću uvrnutih Galoisovih natkrivanja diferencijskih mnogostrukosti.


Kada su dva algoritma jednaka?

9. lipnja 2008., 15:00, predavaonica 109 — Paola Glavan, FSB

Algoritmi se obično smatraju apstaktnijima od programa koji ih implemetiraju. Prirodna formalizacija te ideje je: algoritmi su klase ekvivalencije programâ u odnosu na neku relaciju ekvivalencije.
Koja relacija ekvivalencije "hvata" taj pojam i postoji li ona uopće?

ponedjeljak, 12. svibnja 2008., 15:00; predavaonica 109 — Andre Scedrov

Collaborative planning with privacy

Collaboration among organizations or individuals is common. While these participants are often unwilling to share all their information with each other, some information sharing is unavoidable when achieving a common goal. The need to share information and the desire to keep it private/secret are two competing notions which affect the outcome of a collaboration. This joint work with Kanovich and Rowe proposes a formal model of collaboration which addresses privacy/secrecy concerns. We draw on the notion of a plan which originates in the AI literature. We consider transition systems in which actions have pre- and post-conditions of the same size. We show it is PSPACE-complete to decide whether a given such system protects the privacy/secrecy of its participants and whether it contains a plan leading from a given initial state to a desired goal state.


ponedjeljak, 5. svibnja 2008., 15:00; predavaonica 109 — Andre Scedrov

Formal Analysis of the Kerberos 5 Authentication Protocol

The design and security analysis of protocols that use cryptographic primitives is one of the most fundamental and challenging areas of computer security research. Relatively succinct but subtle authentication, key exchange, negotiation, authorization, and related protocols are the building blocks for secure distributed systems. Protocol analysis is a successful scientific area with two important but historically independent foundations, one based on symbolic computation and one based on computational complexity theory.

Here we highlight joint work with Cervesato, Jaggard, Tsay, and Walstad on the formal analysis of the Kerberos 5 authentication protocol suite. This work discovered a serious vulnerability in the Kerberos public-key extension and caused a Microsoft security patch for Windows 2000 and Windows XP operating systems. The work contributed to the reformulation of the IETF standard for Kerberos public-key extension and provided security proofs of the corrected version of the protocol, the latter jointly with Backes. The flaw discovered is not a flaw in implementation or in cryptography, but a protocol-level, structural flaw, which is present even when the underlying cryptographic operations and network infrastructure operate normally. The methodology developed in this work is applicable to a wide range of network security protocols. We also discuss current joint work with Blanchet on mechanized proofs of authentication and key secrecy properties of Kerberos 5, both with and without its public-key extension.

ponedjeljak, 10. ožujka 2008., 17:15
ponedjeljak, 17. ožujka 2008., 17:15 — Domagoj Vrgoč

Random reals

Tehnički rezultati teorije iračunljivosti. Hijerarhije reducibilnosti (1, m, tt, wtt, sw, T). Aritmetička hijerarhija i Hijerarhija Ershova. hijerarhija jumpova i Postov teorem. Izračunljivi i rekurzivno prebrojivi realni brojevi.

Tri osnovna pristupa definiciji random broja. Preko teorije mjere(paradigma tipičnosti), nekompresibilnosti (prefix-free complexity) i teorije vjerojatnosti (nemogućnost uspješnog klađenja). Također raspravljamo i o Solovayevoj karakterizaciji, ukoliko postoji.

Definiramo četiri osnovne klase random brojeva: Martin-Löf randoms, computable randoms, Schnorr randoms i Kurtz randoms, te uspostavljamo njihovu hijerarhiju. Poopćenja bazirana na aritmetičkoj hijerarhiji i hijerarhiji Ershova.

ponedjeljak, 11. veljače 2008., 17:15 — Darko Biljaković

Nefaktorizabilnost kvocijentnog prstena generaliziranih redova potencija s nepozitivnim eksponentima po Berarduccijevom idealu

Na prethodnom seminaru ustanovljena je pogreška u dokazu Pitteloudove tvrdnje da se svaka klasa generaliziranih redova iz navedenog prstena može prikazati kao produkt ireducibilnih elemenata tog prstena.
Sada dajemo kontraprimjer za tu tvrdnju.
Osim toga, koliko je nama poznato, po prvi puta su prikazani neki ireducibilni te prosti elementi našeg prstena.

ponedjeljak, 4. veljače 2008., 17:15 — Zvonimir Šikić

Neka poopćenja Schröder, Bernsteinovog teorema

ponedjeljak, 28. siječnja 2008., 17:15 — Zvonimir Šikić

Freilingovo opovrgnuće hipoteze kontinuuma

&

Indukcija bez uređaja

ponedjeljak, 3. prosinca 2007., 15:00
— Ružica Piskač, Swiss Federal Institute of Technology (EPFL)

Decision Procedures for Multisets with Cardinality Constraints

Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these applications. Multisets arise in these applications for analogous reasons as sets: abstracting the content of linked data structure with duplicate elements leads to multisets. Interactive theorem provers such as Isabelle specify theories of multisets and prove a number of theorems about them to enable their use in interactive verification. However, the decidability and complexity of constraints on multisets is much less understood than for constraints on sets.

The first contribution of this paper is a polynomial-space algorithm for deciding expressive quantifier-free constraints on multisets with cardinality operators. Our decision procedure reduces in polynomial time constraints on multisets to constraints in an extension of quantifier-free Presburger arithmetic with certain ``unbounded sum'' expressions. We prove bounds on solutions of resulting constraints and describe a polynomial-space decision procedure for these constraints.

The second contribution of this paper is a proof that adding quantifiers to a constraint language containing subset and cardinality operators yields undecidable constraints. The result follows by reduction from Hilbert's 10th problem.

ponedjeljak, 22. listopada 2007., 17:15 (slideovi)
ponedjeljak, 29. listopada 2007., 17:15 (slideovi) — Vedran Čačić

Dekorirani uređaji i teorija konkatenacije

Interpretacija teorije konkatenacije (TC) A. Grzegorczyka u strukturama dekoriranih uređajnih tipova. TC je nepotpuna za tu interpretaciju. Interpretacija aritmetike unutar konkretnih konkatenacijskih strukturâ. Svako proširenje od TC ima model koji nije izomorfan nijednoj strukturi dekoriranih uređajnih tipova.


Seminari održani akademske godine 2006./07.:

ponedjeljak, 11. lipnja 2007., 17:15 — Marko Doko

Nepotpunost kao posljedica slučajnosti

Definicija kompleksnosti i algoritamske vjerojatnosti, i veza između ta dva pojma. Definicija slučajnosti preko kompleksnosti. Dokaz da iz činjenice da je halting probability slučajan broj slijedi nepotpunost.

ponedjeljak, 4. lipnja 2007., 16:00 — Matko Botinčan

Distribuirani algoritmi — studijski primjer memorijskog modela Jave

(zajednički rad s Paolom Glavan i Davorom Runje)

U ovom seminaru dat ćemo matematički preciznu specifikaciju memorijskog modela Jave (JMM-a), te diskutirati njegovu interpretaciju u kontekstu strojeva s apstraktnim stanjima (ASM-ova). Izvorna specifikacija JMM-a refaktorizirana je na način kako bi bilo jasno vidljivo na koji način JMM uvjetuje ponašanje okoline. Pri tome, svaka nit višenitnog Java programa predstavlja obični interaktivni small-step algoritam, a sam Java program distribuirani obični interaktivni small-step ASM. Obzirom da JMM predstavlja relaksirani memorijski model, ovakvi ASM-ovi manifestiraju ponašanje koje je nemoguće opaziti u sekvencijalno konzistentnom slučaju. Obzirom da svi dosadašnji modeli izvršavanja distribuiranih ASM-ova pretpostavljaju sekvencijalnu konzistentnost, smatramo da naš model koji jasno razdvaja koncept izvršavanja, okolinu izvršavanja, te opravdanje za okolinu izvršavanja daje koristan uvid u dio onoga što bi trebalo uzeti u obzir prilikom daljnjeg razvoja teorije distribuiranih algoritama (unutar ASM konteksta).


ponedjeljak, 28. svibnja 2007., 17:15
ponedjeljak, 21. svibnja 2007., 17:15 — Ljerka Jukić

Teorem o normalnoj formi za zatvoreni fragment logike interpretabilnosti


ponedjeljak, 14. svibnja 2007., 17:15
ponedjeljak, 7. svibnja 2007., 17:15 — Domagoj Vrgoč

Morleyev teorem


ponedjeljak, 26. veljače 2007., 17:15 — Zvonimir Šikić

Što je logicizam i je li propao?


ponedjeljak, 12. veljače 2007., 17:15 — Zvonimir Šikić

Arrowljev teorem

Nemogućnost pravednosti ili upitna pravednost


ponedjeljak, 13. studenog 2006., 17:15 — Marko Doko

Kardinalna aritmetika

Pojam kofinalnosti, regularni i singularni kardinali. Veza potenciranja, kofinalnosti i beskonačnih sumâ i produkata. Ograničenja koja ZFC postavlja na funkciju kontinuuma.

Jaki granični kardinali, Jechov teorem. Bukovsky-Hechlerov teorem. Neki rezultati uz pretpostavku da vrijedi Hipoteza singularnih kardinalâ ili Generalizirana hipoteza kontinuuma.


ponedjeljak, 9. listopada 2006., 17:15 — Darko Biljaković

Primjedbe na rad D. Pittelouda "Algebraic properties of rings of generalized power series", APAL 16, 2002, 39-66

U navedenom radu autor dokazuje da je ideal J prstena generaliziranih redova k((G≤0)), generiran monomima s negativnim eksponentom, prost, služeći se izvjesnom procjenom dobivenom mukotrpnim računom. U drugom rezultatu tvrdi pomoću iste procjene kako svaki element kvocijentnog prstena k((G≤0))/J ima bar jednu faktorizaciju na ireducibilne faktore.

Pokazat ćemo kako se prva tvrdnja može dokazati mnogo jednostavnije, a da druga tvrdnja ne stoji te ćemo negativno odgovoriti na pitanje Berarduccija, S. Kuhlmann i F.-V. Kuhlmann je li k((G≤0)) faktorizacijski prsten.

Održani seminari akademske godine 2005./06.:


ponedjeljak, 25. rujna 2006., 17:15 — Vedran Čačić

Nezavisnost aksioma izbora

Nakon što je razvijena tehnika forcinga, i njome dokazana nezavisnost hipoteze kontinuuma od ZFC, možemo otići i korak dalje, i dokazati nezavisnost aksioma izbora od preostalih aksiomâ, dakle od ZF. U tu svrhu razvit ćemo teoriju simetričnih skupova, i izgraditi međumodel M⊆N⊆M[G], u kojem će vrijediti ZF, ali ne AC.

ponedjeljak, 18, rujna 2006., 17:15
ponedjeljak, 11. rujna 2006., 17:15
ponedjeljak, 29. svibnja 2006., 18:15,
ponedjeljak, 12. lipnja 2006.,
ponedjeljak, 19. lipnja 2006. — Vedran Čačić

Nezavisnost hipoteze kontinuuma

Osnove metode forcinga. Generički skupovi. Osnovni i prošireni model. Aksiomi koji vrijede u proširenom modelu. Prošireni model kao model za ZF. Leme istinitosti i definabilnosti.


ponedjeljak, 5. lipnja 2006. — Tamas Mihalydeak, University of Debrecen

Tarskian and Husserlian models


(otkazan) ponedjeljak, 29. svibnja 2006. — Sanja Balenović

Teorija korespondencije

Osnovne definicije, standardne translacije, modalna saturacija pomoću ultrafilter-proširenja; van Benthemov teorem karakterizacije, iskaz i dokaz.


ponedjeljak, 15. svibnja 2006. — Mirko Mihaljinec

O HiparhPlutarhovim brojevima 103049 i 310952

Rekonstrukcija sintakse složenih sudova u logici stoičke škole

ponedjeljak, 8. svibnja 2006. — Darko Biljaković

Generalizirani redni brojevi i primjena na generalizirane redove potencijâ

Pokazuje se kako se generalizirane diferencije višeg reda generaliziranih redova potencijâ s nenegativnim eksponentima ponašaju slično diferencijama višeg reda običnih polinomâ. Pri tome su izvjesne klase generaliziranih rednih brojeva korisna reprezentacija običnih rednih brojeva.


ponedjeljak, 24. travnja 2006.Vedran Čačić

NuPRL i teorija tipova(2)

Pregled rekurzije, automatskog zaključivanja (inferencije) tipova, paradigme dokazivanja u NuPRLu, te nekih jednostavnih dokazâ. Pogledat ćemo to sve prvo na jednoj podteoriji, a zatim i u punom kontekstu. Vidjet ćemo da su ugrađeni tipovi i osnovni konstrukti NuPRLa pažljivo odabrani kako bi se zadovoljili i matematički i tehnički aspekti automatskog dokazivanja.


ponedjeljak, 10. travnja 2006. — Vedran Čačić

Sustav NuPRL i teorija tipova

Automatsko dokazivanje matematičkih tvrdnji nekada se činilo kao isključivo akademska djelatnost. No, kako se doseg matematičkih modela sve više širi, u computer scienceu ali i drugdje, javlja se potreba za snažnim softverskim alatima (proof assistants), kao i matematičkim teorijama koje su prilagođenije kompjuterskim dokazima nego što je to klasična logika prvog reda. NuPRL je pokušaj izgradnje takvog softverskog alata, dok se intuicionistička teorija tipova može upotrijebiti kao matematička pozadina.


ponedjeljak, 3. travnja 2006. — Matko Botinčan

Entanglement i thief-and-detectives

Entanglement predstavlja recentno predloženu mjeru složenosti konačnih usmjerenih grafova, koja intuitivno kazuje u kojoj mjeri su ciklusi u grafu međusobno isprepleteni. Definirana je pomoću thief-and-detectives igre, konceptualno slične onoj koja se javlja u karakterizaciji tree-widtha. Ipak, njihova svojstva su u mnogočemu različita. Također, entanglement je usko povezan s računskom i deskriptivnom složenosti modalnog μ-računa i pripadajućih igara parnosti. U ovom seminaru pogledat ćemo osnovna svojstva entanglementa i pokazati da su igre parnosti na klasi grafova omeđenog entanglementa rješive u polinomnom vremenu.


ponedjeljak, 27. ožujka 2006. — Matko Botinčan

Tree-width i robber-and-cops

Stablasta dekompozicija, i uz nju vezan pojam stablaste širine (tree-width), od velike je važnosti u teoriji grafova. Jedan od fundamentalnih rezultatâ kaže da MSO-definabilni problemi (u koje spadaju mnogi NP-potpuni problemi na grafovima) postaju rješivi u linearnom vremenu na klasi grafova omeđene stablaste širine. Također, interesantnom se pokazala i karakterizacija stablaste širine pomoću robber-and-cops igre. U ovom seminaru dat ćemo pregled važnijih rezultatâ i primjenâ na neke probleme u verifikaciji.



Uobičajeni termin sastanaka:
ponedjeljkom, 17:15, soba 203

Sa seminarom za teorijsko računarstvo:
ponedjeljkom, 15:15, soba 109


Seminari održani ove akademske godine (2008./09.):

  • Kanonska konstrukcija konkretnih reprezentacija konkatenacijskih struktura (V. Čačić, 2008-11-10 i 2008-11-17)
  • Prirodni stringovi (V. Čačić, 2008-12-01)
  • Odlučivost i složenost modalnih logika (D. Vrgoč, 2008-12-08)
  • O jednom problemu sumabilnosti redova (Z. Šikić, 2009-01-26)

Voditelji:

  • dr. Zvonimir Šikić
  • dr. Mladen Vuković

Tajnik:

  • mr. Vedran Čačić

Ostali članovi:

  • dr. Darko Biljaković
  • Matko Botinčan
  • Marko Doko
  • mr. Svitan Gaborovič
  • mr. Paola Glavan
  • Petar Gregorek
  • Ljerka Jukić
  • Vedran Novaković 
  • Neva Slani
  • Siniša Miličić
  • Domagoj Vrgoč 
  • Marko Horvat
  • Tin Perkov

Studenti koji prate seminar 

  • Radan Skorić
  • Marko Živković
  • Sandro Skansi
  • Filip Nikšić

Bivši članovi:

  • dr. Vladimir Kirin
  • dr. Luka Krnić
  • dr. Kajetan Šeper
  • mr. Boris Čulina
  • dr. Igor Urbiha
  • dr. Siniša Žampera
  • dr. Dean Rosenzweig
  • dr. Mirko Mihaljinec
  • Mladen Vedriš
  • Zlatko Klanac
  • Kata Tadić
  • Kazimir Majorinc
  • Ante Đerek
  • Ružica Piskač
  • Dora Predrijevac
  • Mirna Kuzmić
  • Tajana Ban-Kirigin
  • Goran Bokun
  • Boris Golub
  • Vedran Šego
  • Aleksandar Hadži-Veljković
  • Marcel Maretić


Seminari održani na FSBu:

  • Goodsteinov teorem (Snježana Majstorović; 2007-05-22; 1h)
  • Cantorova normalna forma (Ivana Kuzmanović; 2007-05-22; 1h)
  • Chaitinov dokaz nepotpunosti (Marko Doko; 2007-05-15; 2h) 
  • Karakterizacija sustava SS (Gordan Radobolja; 2007-05-05; 1h) 
  • Različitost modalnih logikâ (Martina Barberić; 2007-05-05; 1h)
  • Metoda semantičkih stabala u modalnim logikama (Ivan Matić; 2007-05-05; 1h)
  • Dokazi nepotpunosti bez dijagonalne leme (Nenad Šuvak; 2007-04-03; 2h)
  • Gödelizacija aritmetičkih teorijâ (Ljerka Jukić; 2007-03-27; 1h)
  • Ehrenfeucht-Fraïsseove igre (Vedran Novaković; 2007-03-13 i 03-20; 3h)
  • Reprezentabilnost eksplicitnih funkcijâ (Ivan Vazler; 2007-03-06; 1h)
  • Eksplicitnost rekurzivnih funkcijâ (Sarah Rajtmajer; 2007-03-06; 1h)

Održani seminari akademske godine 2004./05.:

  • Proširenje modalne logike (Vedran Šego; 2005-06-27)
  • Generalizirane diferencije generaliziranih redova potencijâ i primjena (Darko Biljaković; 2005-06-20)
  • Konstruktibilni skupovi (Vedran Čačić; 2005-05-30, 06-06 i 06-13)
  • The Verification of a Checker for Priority Queues (Ružica Piskač, University of Saarbrücken; 2005-05-23)
  • Surealni brojevi (Aleksandar Hadži-Veljković; 2005-04-18, 04-25 i 05-09)
  • Igre s povratom i inflatorne fiksne točke (Matko Botinčan; 2005-02-28)
  • Verifikacija modelâ za logike s operatorom najveće (najmanje) čvrste točke (Matko Botinčan; 2005-02-21)
  • Algoritmi za igre parnosti (Matko Botinčan; 2005-02-14)
  • Beskonačne igre (Matko Botinčan; 2005-01-24 i 01-17)
  • Model-checking igre u deskriptivnoj teoriji složenosti (Matko Botinčan; 2005-01-10)
  • Nula-jedan zakoni (Matko Botinčan; 2004-11-15 i 11-22)
  • Fragmenti logike prvog reda s konačno mnogo varijablî (Zvonimir Bujanović; 2004-11-04 i 11-08)
  • Teorija konačnih modelâ (Mladen Vuković; 2004-10-25) 

Seminari održani prethodnih akademskih godinâ
(tajnik: V. Čačić):

Davno održani seminari
(tajnik: M. Vuković):

2001./02. ,
2000./01.
1999./00.
1998./99. ,
1997./98. ,
1996./97. ,
1995./96. ,
1994./95. ,
1993./94. ,
1992./93. ,
1991./92. ,
1990./91. ,
1989./90. .