Seminar for
Mathematical Logic
PROGRAM
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
PETAK, 14. maj 2004.G. U 16.15 SATI
PETAK, 21. maj 2004.G. U 16.15 SATI
PETAK, 28. april 2004.G. U 16.15 SATI
OBAVESTENJE:
Skrecemo paznju na jos dva zanimljiva predavanja
PETAK, 7. MAJ 2004.G. U 14:00 SATI (ODELJENJE ZA MATEMATIKU)
PETAK, 28. MAJ 2004.G. U 14 SATI - ODELJENJE ZA MATEMATIKU
U Beogradu, 01.05.2004.
Rukovodioci seminara:
Azurirani programi svih seminara Matematickog instituta SANU mogu se naci
na adresi www.mi.sanu.ac.yu.
Program Seminara za logiku za maj 2004
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.
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.
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.
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.
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.
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
Dr. Djordje Vukomanovic i Dr. Kosta Dosen.