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:Applications of Finite Model Theory in Graph Isomo
rphism Testing and Propositional Proof Complexity
- Wied Pakusa\, University of Oxford
DTSTART;TZID=Europe/London:20170616T140000
DTEND;TZID=Europe/London:20170616T150000
UID:TALK71493AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/71493
DESCRIPTION:In this talk we present new applications of finite
model theory in the\nareas of graph isomorphism t
esting and propositional proof complexity.\n\nIn t
he first part\, we will discuss that the solvabili
ty of systems of \nlinear equations and related li
near algebraic properties are definable \nin a fra
gment of fixed-point logic with counting that only
allows \npolylogarithmically many iterations of t
he fixed-point operators.\nThis allows us to separ
ate the descriptive complexity of solving linear \
nequation systems from full fixed-point logic with
counting by logical means. \nWe then draw a conne
ction from this work in descriptive complexity\nth
eory to graph isomorphism testing and propositiona
l proof complexity. \n\nIn the second part\, we es
tablish further connections between\npropositional
proof complexity and finite model theory.\nSpecif
ically\, we explain how the power of several propo
sitional proof systems\, \nsuch as Horn resolution
\, bounded width resolution\, and the polynomial \
ncalculus of bounded degree\, can be characterised
in a precise sense by \nvariants of fixed-point l
ogics that are of fundamental importance in finite
model theory.
LOCATION:FW26
CONTACT:Dominic Mulligan
END:VEVENT
END:VCALENDAR