[logic-ml] JAIST Verification Seminar on Complexity Theory by Prof. Yijia Chen (Feb 9, 13:00)

[Nao Hirokawa]

皆様

明日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.