BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Logic programming: laxness and saturation - John Power (University
  of Bath)
DTSTART:20170124T141500Z
DTEND:20170124T151500Z
UID:TALK69907@talks.cam.ac.uk
CONTACT:Tamara von Glehn
DESCRIPTION:(joint with Ekaterina Komendantskaya)\n\nA propositional logic
  program P may be identified with a (Pf Pf)-coalgebra on the set of atomic
  propositions in the program. The corresponding C-coalgebra\, where C is t
 he cofree comonad on Pf Pf\, describes derivations by resolution. That cor
 respondence has been developed to model first-order programs in two ways\,
  with lax semantics and saturated semantics\, based on locally ordered cat
 egories and right Kan extensions respectively. We unify the two approaches
 \, exhibiting them as complementary rather than competing\, reflecting the
  theorem-proving and proof-search aspects of logic programming.\nWhile mai
 ntaining that unity\, we further refine lax semantics to give finitary mod
 els of logic progams with existential variables\, and to develop a precise
  semantic relationship between variables in logic programming and worlds i
 n local state.
LOCATION:MR5\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR