BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Applications of Finite Model Theory in Graph Isomorphism Testing a
 nd Propositional Proof Complexity - Wied Pakusa\, University of Oxford
DTSTART:20170616T130000Z
DTEND:20170616T140000Z
UID:TALK71493@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:In this talk we present new applications of finite model theor
 y in the\nareas of graph isomorphism testing and propositional proof compl
 exity.\n\nIn the first part\, we will discuss that the solvability of syst
 ems of \nlinear equations and related linear algebraic properties are defi
 nable \nin a fragment of fixed-point logic with counting that only allows 
 \npolylogarithmically many iterations of the fixed-point operators.\nThis 
 allows us to separate the descriptive complexity of solving linear \nequat
 ion systems from full fixed-point logic with counting by logical means. \n
 We then draw a connection from this work in descriptive complexity\ntheory
  to graph isomorphism testing and propositional proof complexity. \n\nIn t
 he second part\, we establish further connections between\npropositional p
 roof complexity and finite model theory.\nSpecifically\, we explain how th
 e power of several propositional proof systems\, \nsuch as Horn resolution
 \, bounded width resolution\, and the polynomial \ncalculus of bounded deg
 ree\, can be characterised in a precise sense by \nvariants of fixed-point
  logics that are of fundamental importance in finite model theory.
LOCATION:FW26
END:VEVENT
END:VCALENDAR