Mathematical Colloquim

PROGRAM

ODELJENJE ZA MATEMATIKU

MATEMATICKOG INSTITUTA SANU

OPSTI MATEMATICKI SEMINAR

Rukovodioci Odeljenja za matematiku Matematickog instituta SANU i Opsteg matematickog seminara na Matematickom fakultetu u Beogradu, Stevan Pilipovic i Sinisa Vrecica predlazu zajednicki program rada naucnih sastanaka.

Predavanja ce se odrzavati na Matematickom Institutu (sala 2), petkom sa pocetkom u 14 casova. Odeljenje za matematiku je opsti seminar sa najduzom tradicijom u Institutu.

Svakog meseca, jedno predavanje ce biti odrzano na Matematickom Fakultetu u terminu koji ce biti posebno odredjen.

Molimo sve zainteresovane ucesnike u radu naucnih sastanaka da posebno obrate paznju na vreme odrzavanja svakog sastanka. Na Matematickom fakultetu su moguce izmene termina.

Obavestenje o programu naucnih sastanaka ce biti objavljeno na oglasnim tablama MI (Beograd), MF (Beograd), PMF (Novi Sad), PMF (Nis) i PMF (Kragujevac).

Odeljenje za matematiku Matematickog instituta SANU

Stevan Pilipovic

Opsti matematicki seminar na Matematickom fakultetu u Beogradu,

Sinisa Vrecica

-- PROGRAM ZA MAJ 2004 --

Petak, 07. maj 2004. u 14h, sala 2 MI SANU :

Peter O'Hearn, Queen Mary Colledge, London University
SEPARATION LOGIC

Abstract: Separation logic is an extension of Hoare's logic to programs than mutate data structures with pointers. The main novelty of the logic is the "separating conjunction" P*Q, which holds when the program state can be partitioned into two portions, one of which makes P true and the other of which makes Q true. The separating conjunction allows local reasoning about portions of state to be done in isolation, and then combined in a modular way. Separation logic has been developed in a series of papers by Reynolds, O'Hearn, Yang and others; this will be an introductory talk that describes its central ideas.

Petak, 14. maj 2004. u 14h, sala 2 MI SANU:

TOPOLOSKA TEORIJA GRAFOVA

Rezime: Bojenje grafova je zanimljiv problem, interesatan i sa teoretskog i prakticnog stanovista. Ovo pitanje se na primer pojavljuje u (pojednostavljenom) modelu alociranja frekvencija u mobilnoj telefoniji. Najslavniji matematicki problem u kategoriji bojenja grafova je svakako problem cetiri boje, resen od strane Haken-a i Appell-a 1977. sa najnovijim dokazom koji su dali Robertson, Sanders, Seymour i Thomas.

U predavanju ce biti prikazana ona grana teorije bojenja grafova koja se oslanja na upotrebu topoloskih metoda primenjenih na tzv. (simplicijalne) graf-komplekse. Osnovni rezultat u oblasti je znamenito resenje Kneser-ove hipoteze (L. Lovasz, 1978) a najnoviji prodor su ostvarili E. Babson i D. Kozlov, resenjem tzv. Lovasz-ove hipoteze. Pokazuje se da su topoloske metode ne samo korisne, nego u nekim slucajevima i jedine poznate metode za nalazenje dobrih donjih ocena za hromatski broj vaznih klasa grafova.

Petak, 21. maj 2004. u 14h, sala 2 MI SANU:

SISTEMI HES - APELJROTOVOG TIPA

Rezime: Lagranzeva dvojna cigra je novi integrabilni sistem dinamike krutog tela na so(4) X so(4). Izucavanje dinamickih i geometrijskih svojstava ovog sistema motivise uvodjenje nove klase integrabilnih dinamickih sistema -- izoholomorfnih sistema. Odredjene perturbacije izoholomorfnih sistema daju prve primere visedimenzionih uopstenja klasicnog Hes-Apeljrotovog sistema.

Petak, 28. maj 2004. u 14h (MF):

NEKI NOVI REZULTATI U TEORIJI VEROVATNOSNIH LOGIKA

Rezime: U okviru projekta 1379 jedna grupa istrazivaca se bavi verovatnosnim logikama. U izlaganju ce biti prikazani rezultati ove grupe koji su publikovani ili prihvaceni za publikovanje tokom rada projekta. To se odnosi na razvoj: verovatnosnih logika sa intuicinostickom logikom kao baznom, verovatnosnih logika sa operatorima za uslovnu verovatnocu, kao i verovatnosnih logika kod kojig su kodomeni verovatnoca konacni.

OBAVESTENJA

U petak, 07.05. u 16h, sala 2 SANU, u okviru Seminara za logiku odrzace se drugi deo predavanja na temu SEPARATION LOGIC:

A DECIDABLE FRAGMENT OF SEPARATION LOGIC Josh Berdine (joint with Cristiano Calcagno and Peter O'Hearn)

ABSTRACT: A small fragment of separation logic and a procedure for deciding validity of entailments between formulae is described. The fragment includes only a single inductive predicate, describing segments of linked lists (essentially reachability), and restricts formulae to a special form whose main characteristic is the inability to express `unspecified sharing''. That is, general separation logic formulae are sometimes modeled by heaps (worlds) where some parts of a heap model multiple subformulae. The fragment rules out such formulae, roughly leaving only those whose models can be split into separate pieces for each subformula. While admittedly very small, the observation that the specifications of many list-manipulating pointer programs fit into this fragment motivated our investigation. The key to decidability is the inability of formulae in the fragment to distinguish between different models (of the inductive case) of the list segment predicate. This, together with separation logic's finite model property, allows ignoring all but a couple heaps in the search for a countermodel. Proof theoretically, this manifests as a rule which infers an inductive property from non-inductive premisses.

Ovo obavestenje mozete naci i na Internetu: www.mi.sanu.ac.yu

Ako zelite da se obavestenje o Vasim naucnim skupovima pojave u Newsletter of EMS (European Mathematical Society) i na Internetu na lokaciji EMS, onda se obratite na emsvesti@mi.sanu.ac.yu gde cete dobiti format obavestenja.