Logical foundations of proof complexity
From MaRDI portal
bounded arithmeticbounded reverse mathematicscomplexity classesproof complexityreflection principlewitnessing theorem
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Complexity of proofs (03F20) First-order arithmetic and fragments (03F30) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)
Recommendations
Cited in
(83)- Understanding cutting planes for QBFs
- Real closures of models of weak arithmetic
- Lower bound techniques for QBF expansion
- Feasibly constructive proofs of succinct weak circuit lower bounds
- The treewidth of proofs
- Building strategies into QBF proofs
- Expander construction in \(\mathrm{VNC}^1\)
- From QBFs to \textsf{MALL} and back via focussing
- On the efficiency of solving Boolean polynomial systems with the characteristic set method
- Partially definable forcing and bounded arithmetic
- A formal framework for stringology
- Induction rules in bounded arithmetic
- Open induction in a bounded arithmetic for \(\mathrm{TC}^{0}\)
- Applicative theories for logarithmic complexity classes
- A game characterisation of tree-like Q-resolution size
- On the complexity of the reflected logic of proofs
- Elementary analytic functions in \(\mathsf{VT}\mathsf{C}^0\)
- A game characterisation of tree-like Q-resolution size
- Total maps of Turing categories
- Reverse complexity
- Build your own clarithmetic. I: Setup and completeness
- Superpolynomial lower bounds for the \((1+1)\) EA on some easy combinatorial problems
- Recent topics on bounded arithmetic and complexity theory
- scientific article; zbMATH DE number 7228403 (Why is no real title available?)
- A form of feasible interpolation for constant depth Frege systems
- On the correspondence between arithmetic theories and propositional proof systems – a survey
- scientific article; zbMATH DE number 4053608 (Why is no real title available?)
- Corrigendum to: ``Uniform constant-depth threshold circuits for division and iterated multiplication
- Characteristic set algorithms for equation solving in finite fields
- scientific article; zbMATH DE number 1070621 (Why is no real title available?)
- A note on SAT algorithms and proof complexity
- Characterizing propositional proofs as noncommutative formulas
- Strict finitism, feasibility, and the sorites
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- Proof Complexity
- From positive and intuitionistic bounded arithmetic to monotone proof complexity
- Achieving new upper bounds for the hypergraph duality problem through logic
- Expander construction in \(\mathsf{VNC}^1\)
- Axiomatizing proof tree concepts in bounded arithmetic
- Circuit lower bounds in bounded arithmetics
- A simulation of natural deduction and Gentzen sequent calculus
- scientific article; zbMATH DE number 819737 (Why is no real title available?)
- scientific article; zbMATH DE number 937363 (Why is no real title available?)
- Polylogarithmic cuts in models of \(\mathbf{V}^{0}\)
- Rethinking defeasible reasoning: a scalable approach
- Size, cost and capacity: a semantic technique for hard random QBFs
- A recursion-theoretic characterisation of the positive polynomial-time functions
- Building strategies into QBF proofs
- On the finite axiomatizability of \(\forall\hat{\Sigma}^{\mathrm{b}}_1 (\hat{\mathsf{R}}^1_2)\)
- scientific article; zbMATH DE number 7278086 (Why is no real title available?)
- scientific article; zbMATH DE number 7155168 (Why is no real title available?)
- Conservative fragments of \({{S}^{1}_{2}}\) and \({{R}^{1}_{2}}\)
- scientific article; zbMATH DE number 2196512 (Why is no real title available?)
- Uniform Proof Complexity
- Constraint Satisfaction Problems with Global Modular Constraints: Algorithms and Hardness via Polynomial Representations
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- Proof Complexity of Non-classical Logics
- Primitive recursive reverse mathematics
- Models of VTC0$\mathsf {VTC^0}$ as exponential integer parts
- Observations on complete sets between linear time and polynomial time
- On theories of bounded arithmetic for \(\mathrm{NC}^1\)
- The provably total NP search problems of weak second order bounded arithmetic
- The strength of extensionality. II: Weak weak set theories without infinity
- Classes of hard formulas for QBF resolution
- Unprovability of strong complexity lower bounds in bounded arithmetic
- Indistinguishability obfuscation, range avoidance, and bounded arithmetic
- Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
- First-order reasoning and efficient semi-algebraic proofs
- Quantum automating TC^0-Frege is LWE-hard
- From proof complexity to circuit complexity via interactive protocols
- Bounded Henkin quantifiers and the exponential time hierarchy
- Quantum automating \(\mathrm{TC}^0\)-Frege is LWE-hard
- Root finding with threshold circuits
- Proof complexity of positive branching programs
- On some \(\boldsymbol{\Sigma}^B_0\)-formulae generalizing counting principles over \(V^0\)
- Independence results for variants of sharply bounded induction
- Feasibility of primality in bounded arithmetic
- Polynomial calculus for quantified Boolean logic: lower bounds through circuits and degree
- Prime factorization in models of \(\mathrm{PV}_1\)
- Prover-adversary games for systems over (non-deterministic) branching programs
- Does subset sum admit short proofs?
- Short propositional refutations for dense random 3CNF formulas
This page was built for publication: Logical foundations of proof complexity
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5306365)