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:Category Theory Seminar
SUMMARY:Logic programming: laxness and saturation - John P
ower (University of Bath)
DTSTART;TZID=Europe/London:20170124T141500
DTEND;TZID=Europe/London:20170124T151500
UID:TALK69907AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/69907
DESCRIPTION:(joint with Ekaterina Komendantskaya)\n\nA proposi
tional logic program P may be identified with a (P
f Pf)-coalgebra on the set of atomic propositions
in the program. The corresponding C-coalgebra\, wh
ere C is the cofree comonad on Pf Pf\, describes d
erivations by resolution. That correspondence has
been developed to model first-order programs in tw
o ways\, with lax semantics and saturated semantic
s\, based on locally ordered categories and right
Kan extensions respectively. We unify the two appr
oaches\, exhibiting them as complementary rather t
han competing\, reflecting the theorem-proving and
proof-search aspects of logic programming.\nWhile
maintaining that unity\, we further refine lax se
mantics to give finitary models of logic progams w
ith existential variables\, and to develop a preci
se semantic relationship between variables in logi
c programming and worlds in local state.
LOCATION:MR5\, Centre for Mathematical Sciences
CONTACT:Tamara von Glehn
END:VEVENT
END:VCALENDAR