On the correspondence between arithmetic theories and propositional proof systems – a survey

DOI10.1002/malq.200710069zbMath1168.03042OpenAlexW2008138636WikidataQ59903620 ScholiaQ59903620MaRDI QIDQ3619867

Olaf Beyersdorff

Publication date: 9 April 2009

Published in: Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL: http://eprints.whiterose.ac.uk/74440/4/bound_ar_journal.pdf

zbMATH Keywords

surveybounded arithmeticpropositional proof systemsextended Frege systems

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20)

Related Items (6)

Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ Proof complexity of modal resolution ⋮ Nondeterministic functions and the existence of optimal proof systems ⋮ Towards Uniform Certification in QBF ⋮ Understanding cutting planes for QBFs ⋮ Proof Complexity of Non-classical Logics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exponential lower bounds for the pigeonhole principle
• Classes of representable disjoint \textsf{NP}-pairs
• The intractability of resolution
• Bounded arithmetic and the polynomial hierarchy
• Lower bounds for the polynomial calculus
• The complexity of the pigeonhole principle
• Some consequences of cryptographical conjectures for \(S_2^1\) and EF
• Optimal proof systems imply complete sets for promise classes
• On an optimal propositional proof system and the structure of easy subsets of TAUT.
• Dual weak pigeonhole principle, Boolean complexity, and derandomization
• Relating the bounded arithmetic and polynomial time hierarchies
• Pseudorandom generators hard for \(k\)-DNF resolution and polynomial calculus resolution
• The Prospects for Mathematical Logic in the Twenty-First Century
• Tautologies from Pseudo-Random Generators
• On the weak pigeonhole principle
• The deduction rule and linear and near-linear proof simulations
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• Quantified propositional calculi and fragments of bounded arithmetic
• Logical Closure Properties of Propositional Proof Systems
• Polynomial size proofs of the propositional pigeonhole principle
• Rudimentary Predicates and Relative Computation
• The relative efficiency of propositional proof systems
• Forcing on bounded arithmetic II
• Witnessing functions in bounded arithmetic and search problems
• Pseudorandom Generators in Propositional Proof Complexity
• Forcing in Proof Theory
• An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
• Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic
• The Complexity of Propositional Proofs
• Lower Bounds on Hilbert's Nullstellensatz and Propositional Proofs
• NP search problems in low fragments of bounded arithmetic
• Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds
• Consequences of the provability of NP ⊆ P/poly
• The Deduction Theorem for Strong Propositional Proof Systems
• Notes on polynomially bounded arithmetic
• Natural proofs

This page was built for publication: On the correspondence between arithmetic theories and propositional proof systems – a survey