ICS 2010

Welcome to ICS2010
Innovations in Computer Science  ICS 2010, Tsinghua University, Beijing, China, January 57, 2010. Proceedings, 370382,
9787302217527
Tsinghua University Press
We introduce a more general notion of efficient simulation between proof systems, which we call effectivelyp simulation. We argue that this notion is more natural from a complexitytheoretic point of view, and by revisiting standard concepts in this light we obtain some surprising new results. First, we give several examples where effectivelyp simulations are possible between different propositional proof systems, but where psimulations are impossible (sometimes under complexity assumptions). Secondly, we prove that the rather weak proof system G0 for quantified propositional logic (QBF) can effectivelyp simulate any proof system for QBF. Thus our definition sheds new light on the comparative power of proof systems. We also give some evidence that with respect to Frege and Extended Frege systems, an effectivelyp simulation may not be possible. Lastly, we prove new relationships between effectivelyp simulations, automatizability, and the P versus NP question. Preview:

Copyright 20092010, Institute for Computer Science, Tsinghua University, All Rights Reserved.