A form of feasible interpolation for constant depth Frege systems

DOI10.2178/jsl/1268917504zbMath1194.03052OpenAlexW1991886545MaRDI QIDQ3570172

Jan Krajíček

Publication date: 24 June 2010

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2178/jsl/1268917504

zbMATH Keywords

Frege systemchain interpolationcomplexity of formula

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Other degrees and reducibilities in computability and recursion theory (03D30) Complexity of proofs (03F20)

Related Items (2)

Short refutations for an equivalence‐chain principle for constant‐depth formulas ⋮ Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem

Cites Work

• Unnamed Item
• Unnamed Item
• Exponential lower bounds for the pigeonhole principle
• Non-automatizability of bounded-depth Frege proofs
• Provability of the pigeonhole principle and the existence of infinitely many primes
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• On Interpolation and Automatization for Frege Systems
• 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
• An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams

This page was built for publication: A form of feasible interpolation for constant depth Frege systems