Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
From MaRDI portal
Publication:4358049
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
Cites work
- scientific article; zbMATH DE number 610968 (Why is no real title available?)
- scientific article; zbMATH DE number 4121954 (Why is no real title available?)
- A lower bound for the complexity of Craig's interpolants in sentential logic
- Every Prime Has a Succinct Certificate
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- On induction-free provability
- On the complexity of cutting-plane proofs
- On the scheme of induction for bounded arithmetic formulas
- Proof theory
- Provability of the pigeonhole principle and the existence of infinitely many primes
- Quantified propositional calculi and fragments of bounded arithmetic
- Resolution proofs of generalized pigeonhole principles
- Tautologies with a unique Craig interpolant, uniform vs. nonuniform complexity
- The complexity of explicit definitions
- The intractability of resolution
- The monotone circuit complexity of Boolean functions
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
Cited in
(86)- Interpolation-based GR(1) assumptions refinement
- Lower bound techniques for QBF expansion
- Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic
- Characterizing propositional proofs as noncommutative formulas
- 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
- Towards NP-P via proof complexity and search
- Resolution proof transformation for compression and interpolation
- Nondeterministic functions and the existence of optimal proof systems
- An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
- Classes of representable disjoint \textsf{NP}-pairs
- The Complexity of Propositional Proofs
- Tuples of disjoint \(\mathsf{NP}\)-sets
- Incompleteness in the finite domain
- Abstract Counterexamples for Non-disjunctive Abstractions
- Feasibly constructive proofs of succinct weak circuit lower bounds
- Resolution for Max-SAT
- Mean-payoff games and propositional proofs
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Interpolation systems for ground proofs in automated deduction: a survey
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- ON OBDD-BASED ALGORITHMS AND PROOF SYSTEMS THAT DYNAMICALLY CHANGE THE ORDER OF VARIABLES
- On semantic cutting planes with very small coefficients
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- Proof complexity of non-classical logics
- Lower bounds for monotone real circuit depth and formula size and tree-like cutting planes
- scientific article; zbMATH DE number 7350778 (Why is no real title available?)
- NIL: learning nonlinear interpolants
- A form of feasible interpolation for constant depth Frege systems
- A note about k-DNF resolution
- Cutting planes cannot approximate some integer programs
- Approximation Refinement for Interpolation-Based Model Checking
- How QBF expansion makes strategy extraction hard
- Constraint solving for interpolation
- A characterization of tree-like resolution size
- Partition-based logical reasoning for first-order and propositional theories
- Nisan-Wigderson generators in proof systems with forms of interpolation
- A game characterisation of tree-like Q-resolution size
- Parity Games and Propositional Proofs
- Monotone circuit lower bounds from resolution
- A feasible interpolation for random resolution
- Resolution over linear equations modulo two
- Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
- First-order reasoning and efficient semi-algebraic proofs
- A supernodal formulation of vertex colouring with applications in course timetabling
- Some consequences of cryptographical conjectures for \(S_2^1\) and EF
- Understanding cutting planes for QBFs
- An Independence Result for Intuitionistic Bounded Arithmetic
- Proof complexity of intuitionistic implicational formulas
- On interpolation in decision procedures
- Tautologies from pseudo-random generators
- On the automatizability of resolution and related propositional proof systems
- Separation results for the size of constant-depth propositional proofs
- Lower bounds for modal logics
- The computational content of arithmetical proofs
- scientific article; zbMATH DE number 7228403 (Why is no real title available?)
- scientific article; zbMATH DE number 7250156 (Why is no real title available?)
- Discretely ordered modules as a first-order extension of the cutting planes proof system
- Polynomial time ultrapowers and the consistency of circuit lower bounds
- From positive and intuitionistic bounded arithmetic to monotone proof complexity
- A game characterisation of tree-like Q-resolution size
- A lower bound for intuitionistic logic
- On the computational content of intuitionistic propositional proofs
- Feasible interpolation for QBF resolution calculi
- On lengths of proofs in non-classical logics
- 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}^+$$
- Size, cost and capacity: a semantic technique for hard random QBFs
- Randomized feasible interpolation and monotone circuits with a local oracle
- Foundations of instance level updates in expressive description logics
- The cost of a cycle is a square
- Lower bound techniques for QBF proof systems
- Logical Closure Properties of Propositional Proof Systems
- 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
- On transformations of constant depth propositional proofs
- Random resolution refutations
- Transition power abstractions for deep counterexample detection
- Cliques enumeration and tree-like resolution proofs
- Monotone simulations of non-monotone proofs.
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- Pseudorandom generators hard for \(k\)-DNF resolution and polynomial calculus resolution
- How to deal with unbelievable assertions
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)
