BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
Proof complexity of deep inference: past\, present and futur
e
STATUS:CONFIRMED
ATTENDEE;CN="Anupam Das
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk I will survey the current state of research on
the complexity of deep inference proofs in classical proposi
tional logic\, and also introduce a program of research prop
osing to further develop this subject. Deep inference calcul
i\, due to Guglielmi and others\, differ from traditional sy
stems by allowing proof rules to operate on any connective o
ccurring in a formula\, as opposed to just the main connecti
ve. Consequently such calculi are more fine-grained and admi
t smaller proofs of benchmark tautologies\, including the pi
geonhole principle. As well as plainly theoretical motivatio
ns\, this is advantageous from the point of view of proof co
mmunication\, allowing for compact and easy-to-check certifi
cates for proofs. I present a graph-based formalism called '
atomic flows' and a rewriting system on them that models pro
of normalisation while preserving complexity properties. I s
how how such an abstraction has been influential in work up
to now\, allowing the obtention of surprisingly strong upper
bounds and simulations in analytic deep inference. The bigg
est open question in the area is the relative complexity bet
ween the minimal system KS and a version that allows a form
of sharing\, KS+. To this end I will introduce a novel appro
ach using weak fragments of arithmetic to serve as uniform c
ounterparts to these nonuniform propositional systems\, insp
ired by the approach of bounded arithmetic. As well as assoc
iating a propositional system with an arithmetic theory in a
formal sense\, this also naturally identifies an associated
complexity class of functions\, and so tools and intuitions
from logic and complexity theory can thence be used to obta
in more powerful results in proof complexity. Due to the pec
uliarities of deep inference calculi\, the search for corres
ponding arithmetic theories takes us into the unexplored ter
ritories (from the point of view of bounded arithmetic) of i
ntuitionistic and substructural logics\, requiring an intere
sting interplay of subjects at the interface of logic and co
mputation.
DTSTART;TZID=Europe/Paris:20151209T143000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201512091
430
UID:LSVsemLSV.201512091430@lsv.ens-cachan.fr
LOCATION:Amphi A 117 (Bat. Alembert)
END:VEVENT
END:VCALENDAR