Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic

DOI10.2307/2275541zbMath0891.03029OpenAlexW2044632231WikidataQ106785017 ScholiaQ106785017MaRDI QIDQ4358049

Publication date: 8 July 1998

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

Full work available at URL: https://doi.org/10.2307/2275541

zbMATH Keywords

exponential lower bounds bounded arithmetic proof systems communication complexity interpolant weak pigeonhole principle Craig interpolation theorem circuit-size feasible monotone interpolation theorem

Mathematics Subject Classification ID

Complexity of computation (including implicit computational complexity) (03D15) First-order arithmetic and fragments (03F30) Classical propositional logic (03B05) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20)

Related Items (79)

Monotone simulations of non-monotone proofs. ⋮ Discretely ordered modules as a first-order extension of the cutting planes proof system ⋮ Random \( \Theta (\log n) \) -CNFs are Hard for Cutting Planes ⋮ On the automatizability of resolution and related propositional proof systems ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Interpolation and model checking for nonlinear arithmetic ⋮ Proof complexity of modal resolution ⋮ The cost of a cycle is a square ⋮ Lower bounds for monotone real circuit depth and formula size and tree-like cutting planes ⋮ Nondeterministic functions and the existence of optimal proof systems ⋮ Feasible Interpolation for QBF Resolution Calculi ⋮ Nisan-Wigderson generators in proof systems with forms of interpolation ⋮ Unnamed Item ⋮ A note about \(k\)-DNF resolution ⋮ Proof complexity of intuitionistic implicational formulas ⋮ Randomized feasible interpolation and monotone circuits with a local oracle ⋮ Dag-like communication and its applications ⋮ A lower bound for intuitionistic logic ⋮ Constraint solving for interpolation ⋮ Characterizing Propositional Proofs as Noncommutative Formulas ⋮ Some consequences of cryptographical conjectures for \(S_2^1\) and EF ⋮ Lower Bound Techniques for QBF Proof Systems ⋮ Collapsing modular counting in bounded arithmetic and constant depth propositional proofs ⋮ Classes of representable disjoint \textsf{NP}-pairs ⋮ A supernodal formulation of vertex colouring with applications in course timetabling ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Logical Closure Properties of Propositional Proof Systems ⋮ Parity Games and Propositional Proofs ⋮ Towards NP-P via proof complexity and search ⋮ A game characterisation of tree-like Q-resolution size ⋮ Foundations of instance level updates in expressive description logics ⋮ Cliques enumeration and tree-like resolution proofs ⋮ Cutting planes cannot approximate some integer programs ⋮ A characterization of tree-like resolution size ⋮ Tuples of disjoint \(\mathsf{NP}\)-sets ⋮ An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams ⋮ Resolution proof transformation for compression and interpolation ⋮ Partition-based logical reasoning for first-order and propositional theories ⋮ ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES ⋮ Interpolation-Based GR(1) Assumptions Refinement ⋮ INCOMPLETENESS IN THE FINITE DOMAIN ⋮ Tautologies from Pseudo-Random Generators ⋮ On Interpolation in Decision Procedures ⋮ Lower bound techniques for QBF expansion ⋮ Resolution over linear equations and multilinear proofs ⋮ On semantic cutting planes with very small coefficients ⋮ A form of feasible interpolation for constant depth Frege systems ⋮ How to deal with unbelievable assertions ⋮ Pseudorandom generators hard for \(k\)-DNF resolution and polynomial calculus resolution ⋮ The computational content of arithmetical proofs ⋮ Lower bounds for modal logics ⋮ Feasibly constructive proofs of succinct weak circuit lower bounds ⋮ On the computational content of intuitionistic propositional proofs ⋮ Mean-payoff games and propositional proofs ⋮ Understanding cutting planes for QBFs ⋮ The Complexity of Propositional Proofs ⋮ A Game Characterisation of Tree-like Q-resolution Size ⋮ Approximation Refinement for Interpolation-Based Model Checking ⋮ Polynomial time ultrapowers and the consistency of circuit lower bounds ⋮ Proof Complexity of Non-classical Logics ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ On Interpolation and Symbol Elimination in Theory Extensions ⋮ Unnamed Item ⋮ NIL: learning nonlinear interpolants ⋮ On transformations of constant depth propositional proofs ⋮ Random resolution refutations ⋮ Resolution for Max-SAT ⋮ Abstract Counterexamples for Non-disjunctive Abstractions ⋮ Unnamed Item ⋮ Separation results for the size of constant-depth propositional proofs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Resolution over linear equations modulo two ⋮ An interpolating theorem prover ⋮ How QBF expansion makes strategy extraction hard ⋮ A feasible interpolation for random resolution ⋮ Reflections on Proof Complexity and Counting Principles

Cites Work

This page was built for publication: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic