Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
From MaRDI portal
Publication:4358049
DOI10.2307/2275541zbMATH Open0891.03029OpenAlexW2044632231WikidataQ106785017 ScholiaQ106785017MaRDI QIDQ4358049FDOQ4358049
Authors: Jan Krajíček 
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
Recommendations
- scientific article; zbMATH DE number 819737
- scientific article; zbMATH DE number 806751
- scientific article; zbMATH DE number 1070621
- Witnessing functions in bounded arithmetic and search problems
- scientific article; zbMATH DE number 2102736
- scientific article; zbMATH DE number 1342249
- scientific article; zbMATH DE number 7650818
- scientific article; zbMATH DE number 922617
- On the complexity of arithmetical interpretations of modal formulae
- scientific article; zbMATH DE number 2196512
bounded arithmeticcommunication complexityexponential lower boundsproof systemsweak pigeonhole principleinterpolantCraig interpolation theoremcircuit-sizefeasible monotone interpolation theorem
Classical propositional logic (03B05) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20) First-order arithmetic and fragments (03F30) Complexity of computation (including implicit computational complexity) (03D15)
Cites Work
- Title not available (Why is that?)
- On the scheme of induction for bounded arithmetic formulas
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- The monotone circuit complexity of Boolean functions
- On the complexity of cutting-plane proofs
- Proof theory
- The intractability of resolution
- Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity
- Quantified propositional calculi and fragments of bounded arithmetic
- On induction-free provability
- Every Prime Has a Succinct Certificate
- Provability of the pigeonhole principle and the existence of infinitely many primes
- Resolution proofs of generalized pigeonhole principles
- A lower bound for the complexity of Craig's interpolants in sentential logic
- The complexity of explicit definitions
- Title not available (Why is that?)
Cited In (86)
- Abstract Counterexamples for Non-disjunctive Abstractions
- Feasibly constructive proofs of succinct weak circuit lower bounds
- Title not available (Why is that?)
- NIL: learning nonlinear interpolants
- How QBF expansion makes strategy extraction hard
- Parity Games and Propositional Proofs
- Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
- First-order reasoning and efficient semi-algebraic proofs
- Resolution over linear equations modulo two
- An Independence Result for Intuitionistic Bounded Arithmetic
- Polynomial time ultrapowers and the consistency of circuit lower bounds
- On P-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics $$\mathcal{E}\mathcal{L}, \mathcal{E}\mathcal{L}^+$$
- Feasible interpolation for QBF resolution calculi
- Transition power abstractions for deep counterexample detection
- On transformations of constant depth propositional proofs
- Random resolution refutations
- Characterizing propositional proofs as noncommutative formulas
- Lower bound techniques for QBF expansion
- Reflections on Proof Complexity and Counting Principles
- Interpolation and model checking for nonlinear arithmetic
- Proof complexity of modal resolution
- Random \( \Theta (\log n) \) -CNFs are Hard for Cutting Planes
- An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
- Towards NP-P via proof complexity and search
- Resolution proof transformation for compression and interpolation
- The Complexity of Propositional Proofs
- Nondeterministic functions and the existence of optimal proof systems
- Classes of representable disjoint \textsf{NP}-pairs
- Tuples of disjoint \(\mathsf{NP}\)-sets
- Incompleteness in the finite domain
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- Resolution for Max-SAT
- Mean-payoff games and propositional proofs
- ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Interpolation systems for ground proofs in automated deduction: a survey
- Proof complexity of non-classical logics
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- On semantic cutting planes with very small coefficients
- Lower bounds for monotone real circuit depth and formula size and tree-like cutting planes
- A form of feasible interpolation for constant depth Frege systems
- A note about \(k\)-DNF resolution
- Approximation Refinement for Interpolation-Based Model Checking
- Cutting planes cannot approximate some integer programs
- A characterization of tree-like resolution size
- Partition-based logical reasoning for first-order and propositional theories
- Monotone circuit lower bounds from resolution
- Nisan-Wigderson generators in proof systems with forms of interpolation
- Constraint solving for interpolation
- A game characterisation of tree-like Q-resolution size
- A feasible interpolation for random resolution
- Some consequences of cryptographical conjectures for \(S_2^1\) and EF
- A supernodal formulation of vertex colouring with applications in course timetabling
- Understanding cutting planes for QBFs
- Proof complexity of intuitionistic implicational formulas
- On interpolation in decision procedures
- Tautologies from pseudo-random generators
- Lower bounds for modal logics
- On the automatizability of resolution and related propositional proof systems
- Separation results for the size of constant-depth propositional proofs
- Title not available (Why is that?)
- Title not available (Why is that?)
- The computational content of arithmetical proofs
- Discretely ordered modules as a first-order extension of the cutting planes proof system
- From positive and intuitionistic bounded arithmetic to monotone proof complexity
- On the computational content of intuitionistic propositional proofs
- A game characterisation of tree-like Q-resolution size
- A lower bound for intuitionistic logic
- Size, cost and capacity: a semantic technique for hard random QBFs
- Randomized feasible interpolation and monotone circuits with a local oracle
- On lengths of proofs in non-classical logics
- The cost of a cycle is a square
- Lower bound techniques for QBF proof systems
- Logical Closure Properties of Propositional Proof Systems
- Foundations of instance level updates in expressive description logics
- Collapsing modular counting in bounded arithmetic and constant depth propositional proofs
- An interpolating theorem prover
- Resolution over linear equations and multilinear proofs
- Dag-like communication and its applications
- Title not available (Why is that?)
- Cliques enumeration and tree-like resolution proofs
- Monotone simulations of non-monotone proofs.
- Pseudorandom generators hard for \(k\)-DNF resolution and polynomial calculus resolution
- How to deal with unbelievable assertions
- Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic
- Interpolation-based GR(1) assumptions refinement
This page was built for publication: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4358049)
