Quantified propositional calculi and fragments of bounded arithmetic

DOI10.1002/malq.19900360106zbMath0696.03031OpenAlexW2161149481WikidataQ106785088 ScholiaQ106785088MaRDI QIDQ3472099

Jan Krajíček, Pavel Pudlák

Publication date: 1990

Published in: Zeitschrift für Mathematische Logik und Grundlagen der Mathematik (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/malq.19900360106

zbMATH Keywords

finite axiomatizabilityGentzen systemPropositional proof systemsBounded Arithmetic

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30)

Related Items

Dual weak pigeonhole principle, Boolean complexity, and derandomization ⋮ On an optimal quantified propositional proof system nal proof system and a complete language for NP ∩ co-NP for NP ∩ co-NP ⋮ On induction-free provability ⋮ Circuit principles and weak pigeonhole variants ⋮ Quantified propositional calculus and a second-order theory for NC\(^{\text \textbf{1}}\) ⋮ Implicit proofs ⋮ Preservation theorems and restricted consistency statements in bounded arithmetic ⋮ Some consequences of cryptographical conjectures for \(S_2^1\) and EF ⋮ Classes of representable disjoint \textsf{NP}-pairs ⋮ Logical Closure Properties of Propositional Proof Systems ⋮ On the finite axiomatizability of ⋮ Towards Uniform Certification in QBF ⋮ Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem ⋮ Tuples of disjoint \(\mathsf{NP}\)-sets ⋮ Lifting lower bounds for tree-like proofs ⋮ Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic ⋮ Bounded arithmetic and the polynomial hierarchy ⋮ Tautologies from Pseudo-Random Generators ⋮ Towards a unified complexity theory of total functions ⋮ POLYNOMIAL LOCAL SEARCH IN THE POLYNOMIAL HIERARCHY AND WITNESSING IN FRAGMENTS OF BOUNDED ARITHMETIC ⋮ Examining Fragments of the Quantified Propositional Calculus ⋮ On the correspondence between arithmetic theories and propositional proof systems – a survey ⋮ Induction rules in bounded arithmetic ⋮ On transformations of constant depth propositional proofs ⋮ Simulating non-prenex cuts in quantified propositional calculus ⋮ Separation results for the size of constant-depth propositional proofs ⋮ Fragments of bounded arithmetic and the lengths of proofs ⋮ Expansion-based QBF solving versus Q-resolution ⋮ Witnessing functions in bounded arithmetic and search problems