皆様
明日2月9日(木)に JAIST で行われます Yijia Chen 教授の計算量理論に関する 講演をご案内致します。どうぞお気軽にお越しください。
http://www.ldl.jaist.ac.jp/svrcenter/event.html#20120209
廣川 直（北陸先端科学技術大学院大学）
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Seminars of Research Center for Software Verification, JAIST - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Date: 9th Feb (Thu) 13:00-15:00
Place: JAIST IS school collaboration room 7 (5F)
Speaker: Prof.Yijia Chen (Shanghai Jiao Tong University)
Title: A Logic for PTIME and a Parameterized Halting Problem
Abstract: Whether there is a logic for polynomial time (PTIME) is the central problem in finite model theory. When formalizing this problem, Gurevich (1988), together with Blass, actually proposed a logic LFP_inv, which is a version of least fixed-point logic plus some additional invariance condition. Although they don't believe that LFP_inv captures PTIME, no proof was given. Later, in a work of Nash, Remmel, and Vianu (2005), it was shown that whether LFP_inv captures PTIME is equivalent to the parameterized complexity of a halting problem:
input: A nondeterministic Turing machine M and a natural number n in unary. parameter: |M|, i.e., the size of M question: does M accept the empty input in at most n steps?
Our recent work (2010-11) reveals that it is even equivalent to an open problem in proof complexity, i.e., whether there is a polynomial optimal proof system for the set TAUT of tautologies of propositional logic.
In this talk, I will discuss all these equivalences and their extensions to some other complexity classes beside PTIME. It turns out that Levin's optimal inverters (1973) play a central role in the proofs.
This is joint work with Joerg Flum.