Seminar for Mathematical Logic
PROGRAM Program Seminara za logiku za maj 2004
Sastanci Seminara za matematicku logiku Matematickog instituta SANU odrzavace se i u akademskoj 2003/2004. godini po pravilu petkom od 16:15 sati u sali 2 na I spratu zgrade SANU, Beograd, Kneza Mihaila 35.
PETAK, 07. maj 2004.G. U 16.15 SATI
Josh Berdine (joint with Cristiano Calcagno and Peter O'Hearn)
A DECIDABLE FRAGMENT OF SEPARATION LOGIC
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.
PETAK, 14. maj 2004.G. U 16.15 SATI
Boris Sobot (Departman za matematiku i informatiku PMF, Univerzitet u Novom Sadu)
ULTRAPROIZVODI DOBRIH UREDJENJA (Ultraproducts of well orderings)
Rezime: Uvode se fiksne tacke viseg reda normalnih funkcija i primenjuju se da bi se dobili rezultati iz ultraproizvoda dobrih uredjenja.
PETAK, 21. maj 2004.G. U 16.15 SATI
Petar Markovic (Departman za matematiku i informatiku PMF, Univerzitet u Novom Sadu)
SKORO JEDNOGLASNI TERMI I DUALIZABILNOST (Near unanimity terms and dualizability)
Rezime: Daje se pregled aktuelnih rezultata povezanih s temom iz naslova.
PETAK, 28. april 2004.G. U 16.15 SATI
Dragic Bankovic (PMF Univerziteta u Kragujevcu)
POSTOVE JEDNACINE (Post`s equations)
Rezime: Postove algebre su uopstenje Booleovih algebri. Resavanje jednacina na postovim algebrama je slicno resavanju Booleovih jednacina, ali mnogo komplikovanije. Na predavanju ce biti prikazani novi objavljeni i neobjavljeni rezultati predavaca.
OBAVESTENJE:
Skrecemo paznju na jos dva zanimljiva predavanja
PETAK, 7. MAJ 2004.G. U 14:00 SATI (ODELJENJE ZA MATEMATIKU)
SEPARATION LOGIC Peter O'Hearn
Separation logic is an extension of Hoare's logic to programs that 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, 28. MAJ 2004.G. U 14 SATI - ODELJENJE ZA MATEMATIKU
Miodrag Raskovic (Uciteljski fakultet Univerziteta u Beogradu), Radoslav Djordjevic (PMF Univerziteta u Kragujevcu), Zoran Markovic i Zoran Ognjanovic (Matematicki institut SANU, Beograd)
NEKI NOVI REZULTATI U TEORIJI VEROVATNOSNIH LOGIKA (Some new results in probabilistic logics)
B
U Beogradu, 01.05.2004.
Rukovodioci seminara:
Dr. Djordje Vukomanovic i Dr. Kosta Dosen.
Azurirani programi svih seminara Matematickog instituta SANU mogu se naci na adresi www.mi.sanu.ac.yu.