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:A compositional account of Herbrand's theorem via
concurrent games - Pierre Clairambault\, ENS Lyon
DTSTART;TZID=Europe/London:20161118T140000
DTEND;TZID=Europe/London:20161118T150000
UID:TALK67372AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/67372
DESCRIPTION:Herbrand's theorem\, often regarded as a cornersto
ne of proof theory\,\nexposes some of the construc
tive content of classical logic. In its\nsimplest
form\, it reduces the validity of a first-order pu
rely existential formula ∃x.φ(x) (with φ quantifi
er-free) to that of a finite disjunction φ(t₁) ∨ .
.. ∨ φ(tₙ). More generally\, it gives a reduction
of first-order validity to propositional validity\
, by understanding the structure of the assignment
of first-order terms to existential quantifiers\,
and the causal dependency between quantifiers.\n\
nIn this talk\, I will show that Herbrand's theore
m in its general form\ncan be elegantly stated as
a theorem in the framework of concurrent\ngames. T
he causal structure of concurrent strategies\, pai
red with\nannotations by first-order terms\, is us
ed to specify the dependency\nbetween quantifiers.
Furthermore concurrent strategies can be composed
\,\nyielding a compositional proof of Herbrand's t
heorem\, simply by interpreting classical sequent
proofs in a well-chosen denotational\nmodel. I ass
ume no prior knowledge of Herbrand's theorem or co
ncurrent\ngames.\n\nThis is joint work with Aurore
Alcolei\, Martin Hyland and Glynn Winskel.
LOCATION:SS03
CONTACT:Dominic Mulligan
END:VEVENT
END:VCALENDAR