Proofs of Soundness and Proof Search (Invited Talk)

Author Albert Atserias



PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.2.pdf
  • Filesize: 163 kB
  • 1 pages

Document Identifiers

Author Details

Albert Atserias
  • Universitat Politècnica de Catalunya, Barcelona, Spain

Cite AsGet BibTex

Albert Atserias. Proofs of Soundness and Proof Search (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.2

Abstract

Let P be a sound proof system for propositional logic. For each CNF formula F, let SAT(F) be a CNF formula whose satisfying assignments are in 1-to-1 correspondence with those of F (e.g., F itself). For each integer s, let REF(F,s) be a CNF formula whose satisfying assignments are in 1-to-1 correspondence with the P-refutations of F of length s. Since P is sound, it is obvious that the conjunction formula SAT(F) & REF(F,s) is unsatisfiable for any choice of F and s. It has been long known that, for many natural proof systems P and for the most natural formalizations of the formulas SAT and REF, the unsatisfiability of SAT(F) & REF(F,s) can be established by a short refutation. In addition, for many P, these short refutations live in the proof system P itself. This is the case for all Frege proof systems. In contrast it was known since the early 2000’s that Resolution proofs of Resolution’s soundness statements must have superpolynomial length. In this talk I will explain how the soundness formulas for a proof system P relate to the computational complexity of the proof search problem for P. In particular, I will explain how such formulas are used in the recent proof that the problem of approximating the minimum proof-length for Resolution is NP-hard (Atserias-Müller 2019). Besides playing a key role in this hardness of approximation result, the renewed interest in the soundness formulas led to a complete answer to the question whether Resolution has subexponential-length proofs of its own soundness statements (Garlík 2019).

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Proof complexity
  • automatability
  • Resolution
  • proof search
  • consistency statements
  • lower bounds
  • reflection principle
  • satisfiability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads