Date: Dec. 2nd (Fri) 10:30-11:45
Place: ELC Seminar room (Tokyo Tech. CIC Tamachi)
Speaker: Professor Hubie Chen (Universidad del Pais Vasco)

Title: Proof Complexity Modulo the Polynomial Hierarchy:
       Understanding Alternation as a Source of Hardness
Abstract:
If one looks at typical proof systems for QBF, such as Q-resolution,
a dilemma is encountered: lower bounds for Q-resolution are implied
immediately by lower bounds for resolution, yet this says nothing
about Q-resolution's ability to cope with quantifier alternation---
and moreover clashes severely with the contemporary QBF view of SAT
as "easy".

In this talk, we will discuss this dilemma and present a possible
way to escape it.  In particular, we present and study a framework
in which one can present alternation-based lower bounds on proof 
length in proof systems for quantified Boolean formulas. A key notion 
in this framework is that of proof system ensemble, which is 
(essentially) a sequence of proof systems where, for each, proof 
checking can be performed in the polynomial hierarchy. We introduce a 
proof system ensemble called relaxing QU-res which is based on the 
established proof system QU-resolution. Our main technical results 
include an exponential separation of the tree-like and general 
versions of relaxing QU-res, and an exponential lower bound for 
relaxing QU-res; these are analogs of classical results in 
propositional proof complexity.

This talk will focus on a conceptual discussion of the work's 
motivation, the framework and the main definitions.

(host: Osamu Watanabe, watanabe@is.titech.ac.jp)