License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagRep.8.1.124
URN: urn:nbn:de:0030-drops-92864
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9286/
Go back to Dagstuhl Reports

Atserias, Albert ; Nordström, Jakob ; Pudlák, Pavel ; Santhanam, Rahul
Weitere Beteiligte (Hrsg. etc.): Albert Atserias and Jakob Nordström and Pavel Pudlák and Rahul Santhanam

Proof Complexity (Dagstuhl Seminar 18051)

pdf-format:
dagrep_v008_i001_p124_18051.pdf (12 MB)

Abstract

The study of proof complexity was initiated in [Cook and Reckhow 1979] as a way to attack the P vs.NP problem, and in the ensuing decades many powerful techniques have been discovered for analyzing different proof systems. Proof complexity also gives a way of studying subsystems of Peano Arithmetic where the power of mathematical reasoning is restricted, and to quantify how complex different mathematical theorems are measured in terms of the strength of the methods of reasoning required to establish their validity. Moreover, it allows to analyse the power and limitations of satisfiability algorithms (SAT solvers) used in industrial applications with formulas containing up to millions of variables.

During the last 10--15 years the area of proof complexity has seen a
revival with many exciting results, and new connections have also been revealed with other areas such as, e.g., cryptography, algebraic complexity theory, communication complexity, and combinatorial optimization. While many longstanding open problems from the 1980s and 1990s still remain unsolved, recent progress gives hope that the area may be ripe for decisive breakthroughs. This workshop, gathering researchers from different strands of the proof complexity community, gave opportunities to take stock of
where we stand and discuss the way ahead.

BibTeX - Entry

@Article{atserias_et_al:DR:2018:9286,
  author =	{Albert Atserias and Jakob Nordstr{\"o}m and Pavel Pudl{\'a}k and Rahul Santhanam},
  title =	{{Proof Complexity (Dagstuhl Seminar 18051)}},
  pages =	{124--157},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{8},
  number =	{1},
  editor =	{Albert Atserias and Jakob Nordstr{\"o}m and Pavel Pudl{\'a}k and Rahul Santhanam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9286},
  URN =		{urn:nbn:de:0030-drops-92864},
  doi =		{10.4230/DagRep.8.1.124},
  annote =	{Keywords: bounded arithmetic, computational complexity, logic, proof complexity, satisfiability algorithms}
}

Keywords: bounded arithmetic, computational complexity, logic, proof complexity, satisfiability algorithms
Collection: Dagstuhl Reports, Volume 8, Issue 1
Issue Date: 2018
Date of publication: 20.07.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI