On Interpolation and Automatization for Frege Systems
From MaRDI portal
Publication:4507332
DOI10.1137/S0097539798353230zbMath0959.03044WikidataQ60512241 ScholiaQ60512241MaRDI QIDQ4507332
Maria Luisa Bonet, Toniann Pitassi, Ran Raz
Publication date: 18 October 2000
Published in: SIAM Journal on Computing (Search for Journal in Brave)
interpolationlower boundspropositional proof systemsDiffie-Hellmanthreshold circuitsFrege proof systems
Classical propositional logic (03B05) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20)
Related Items (31)
On the automatizability of resolution and related propositional proof systems ⋮ On the complexity of resolution with bounded conjunctions ⋮ The proof complexity of linear algebra ⋮ Nondeterministic functions and the existence of optimal proof systems ⋮ Feasible Interpolation for QBF Resolution Calculi ⋮ A Basic Parameterized Complexity Primer ⋮ On the complexity of finding shortest variable disjunction branch-and-bound proofs ⋮ Conjunctive query evaluation by search-tree revisited ⋮ INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH ⋮ Characterizing Propositional Proofs as Noncommutative Formulas ⋮ Classes of representable disjoint \textsf{NP}-pairs ⋮ Extended clause learning ⋮ Towards NP-P via proof complexity and search ⋮ On reducibility and symmetry of disjoint NP pairs. ⋮ Satisfiability, branch-width and Tseitin tautologies ⋮ Unnamed Item ⋮ Proof complexity of propositional default logic ⋮ On the automatizability of polynomial calculus ⋮ Automatizability and Simple Stochastic Games ⋮ Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds ⋮ A form of feasible interpolation for constant depth Frege systems ⋮ Pseudorandom generators hard for \(k\)-DNF resolution and polynomial calculus resolution ⋮ Mean-payoff games and propositional proofs ⋮ Polynomial-size Frege and resolution proofs of \(st\)-connectivity and Hex tautologies ⋮ Unnamed Item ⋮ The Complexity of Propositional Proofs ⋮ Quantum deduction rules ⋮ Short propositional refutations for dense random 3CNF formulas ⋮ Proof Complexity of Non-classical Logics ⋮ Boundary Points and Resolution ⋮ Short Proofs Are Hard to Find
This page was built for publication: On Interpolation and Automatization for Frege Systems
