Курс будет посвящён оценкам длины доказательств в первую очередь для утверждений логики высказываний, хотя будут рассмотрены и другие языки. Существование системы, в которой есть доказательство полиномиальной длины для каждой тавтологии, эквивалентно (неправдоподобному) утверждению NP = co-NP. Однако на констатации этого факта вопросы не заканчиваются: даже если такой системы нет, есть ли оптимальная система с самыми короткими доказательствами? Для каких систем мы можем доказать экспоненциальные нижние оценки на длину доказательств? Как длины доказательств связаны со сложностью вычислительных задач? Подобным вопросам и будет посвящён этот курс.

Литература

• Обзоры
  • A. Urquhart. The complexity of propositional proofs.
  • P. Pudlak. On the complexity of propositional calculus.
  • E. A. Hirsch, Optimal acceptors and optimal proof systems. Proc. TAMC-2010. LNCS 6108, 2010.
• Статьи
  • A. Atserias, M. L. Bonet. On the Automatizability of Resolution and Related Propositional Proof Systems, Information and Computation, 189(2), pages 182-201, 2004.
  • P. Pudlák, Lower bounds for resolution and cutting planes proofs and monotone computations, J. of Symb. Logic 62(3), 1997, pp.981-998.
  • A. Goerdt, Cutting Plane versus Frege proof systems, Proc. CSL'90, LNCS 533, 1990.
  • E. Ben-Sasson, A. Wigderson, Short Proofs are Narrow - Resolution made Simple. Journal of the ACM 48(2), 2001.