BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Global Realisations of Local Specifications - Mart
in Otto\, Technische Universität Darmstadt\, Germa
ny
DTSTART;TZID=Europe/London:20151106T140000
DTEND;TZID=Europe/London:20151106T150000
UID:TALK62250AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/62250
DESCRIPTION:The following situation is typical of several task
s of model\nconstruction that arise\, e.g.\, in co
nnection with finite model\nproperties and finite
controllability: Given a finite set of local\ntemp
lates\, together with specifications of required a
nd permitted\npairwise overlaps between them\, the
task is to find finite global\nrealisations.\n\nW
e approach this finite realisation task via a gene
ric construction of\nreduced products with suitabl
e groupoids. Due to strong acyclicity\nproperties\
, these groupoids can serve as structural backbone
s in the\nconstruction of finite realisations\, si
milar to the use of free groups\nin standard const
ructions of infinite realisations. The constructio
n\nis sufficiently generic as to be compatible wit
h symmetries of the\nspecification while also allo
wing us to avoid incidental cycles of\noverlaps up
to any specified finite length. The resulting fin
ite\nrealisations can be forced\n\n-- to realise s
ymmetries built into the specification\, and\n-- t
o admit local homomorphisms into any (finite or in
finite)\n\nrealisation and in particular into the
canonical free realisation. As\none consequence w
e obtain a new proof of the finite-model-assertion
in\na theorem of Herwig and Lascar\, which allows
us to lift local\nsymmetries of finite structures
to global symmetries within classes\ndefined by f
orbidden homomorphisms. This in turn proves\, e.g.
\, finite\ncontrollability for UCQ vs. guarded spe
cifications.
LOCATION:FW26
CONTACT:Ohad Kammar
END:VEVENT
END:VCALENDAR