Proof com plexity is the study of the complexity of theorem proving procedures. The central question in proof complexity is: given a theorem F (e.g. a propositi onal tautology) and a proof system P (i.e., a form alism usually comprised of axioms and rules), what is the size of the smallest proof of F in the sys tem P? Moreover, how difficult is it to construct a small proof? Many ingenious techniques have been developed to try to answer these questions, which bare tight relations to intricate theoretical ope n problems from computational complexity (such as the celebrated P vs. NP problem), mathematical log ic (e.g. separating theories of Bounded Arithmetic ) as well as to practical problems in SAT/QBF solv ing.
\nThe workshop will be part of FLoC a nd will be affiliated with the conference SAT'22.< /p>\n
We welcome 1-2-page abstrac ts presenting (finished, ongoing, or if clearly st ated even recently published) work on proof comple xity. Particular topics of interest are * Proof Co mplexity * Bounded Arithmetic * Relations to SAT/Q BF solving * Relations to Computational Complexity . The abstracts will appear in electronic pre-proc eedings that will be distributed at the meeting.\n
Abstracts (at most 2 pages, in LNCS style ) are to be submitted electronically in PDF via Ea syChair. Accepted communications must be presented at the workshop by one of the authors.
\n