Abstract A proof of the (propositional) Craig interpolation theorem for cut-free sequent calculus yields that a with (or cut-formulas restricted form; in particular, only analytic cuts) k inferences has an interpolant whose circuit-size is at most . We give new based on communication complexity approach which allows similar estimate larger class proofs. derive from it several corollaries: (1) Feasible theorems following systems: (a) resolution (b) subsystem LK corresponding to bounded...

Abstract We consider the problem about length of proofs sentences saying that there is no proof contradiction in S whose < n . show relation this to some problems propositional systems.

Abstract We prove lower bounds of the form exp( n ε d ), > 0, on length proofs an explicit sequence tautologies, based Pigeonhole Principle, in proof systems using formulas depth , for any constant d. This is largest bound strongest system, which superpolynomial are known.

We investigate the proof complexity, in (extensions of) resolution and bounded arithmetic, of weak pigeonhole principle Ramsey theorem. In particular, we link complexities these two principles. Further give lower bounds t

The so-called weak form of Hilbert's Nullstellensatz says that a system algebraic equations over field, Q i ( x ¯ ) = 0 , does not have solution in the closure if and only 1 is theideal generated by polynomials . We shall prove lower bound on degrees P such ∑ This result has following application. modular counting principle states no finite set whose cardinality divisible q can be partitioned into q-element classes. For each fixed N, this expressed as propositional formula Count N e … with...

Abstract LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and ∧,∨ (both bounded arity). Then every d ≥ 0 n 2, there set depth sequents total size O ( 3+ ) which are refutable in by + 1 proof exp( (log 2 )) but such that refutation must have the at least Ω(1) ). The sets express weaker form pigeonhole principle.

We develop a method for establishing the independence of some ∑ i b ( α ) formulas from S 2 . In particular, we show that T is not ∀ -conservative over characterize -definable functions 1 as being precisely definable projections polynomial local search (PLS) problems.

Article Free Access Share on Exponential lower bounds for the pigeonhole principle Authors: Paul Beame University of Washington WashingtonView Profile , Russell Impagliazzo UC, San Diego DiegoView Jan Krajíček Mathematical Institute, Prague PragueView Toniann Pitassi Toronto TorontoView Pavel Pudlák Alan Woods Western Australia AustraliaView Authors Info & Claims STOC '92: Proceedings twenty-fourth annual ACM symposium Theory ComputingJuly 1992 Pages...

Abstract We prove the following results: (i) PV proves NP ⊆ P /poly iff coNP / O (1). (ii) If P/poly then that Polynomial Hierarchy collapses to Boolean Hierarchy, (iii) NP/O (log n ). (iv) [log ]. (v) . Motivated by these results we introduce a new concept in proof complexity: systems with advice, and make some initial observations about them.

Abstract This article is a continuation of our search for tautologies that are hard even strong propositional proof systems like EF. cf. [14, 15]. The particular we study, the τ -formulas. obtained from any /poly map g ; they express string outside range , Maps considered here pseudorandom generators. ultimate goal to deduce hardness -formulas at least EF some general, plausible computational hypothesis. In this paper introduce notions pseudo-surjective and iterable functions (related free...

Abstract We define a first-order extension LK(CP) of the cutting planes proof system CP as sequent calculus LK whose atomic formulas are CP-inequalities ∑ i · x ≥ b ( 's variables, and constants). prove an interpolation theorem for yielding corollary conditional lower bound LK(CP)-proofs. For subsystem R(CP) LK(CP), essentially resolution working with clauses formed by CP-inequalities, we monotone obtaining thus unconditional (depending on maximum size coefficients in proofs number clauses)....

We characterize functions and predicates <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="normal upper Sigma Subscript i plus 1 Superscript b"> <mml:semantics> <mml:msubsup> <mml:mi mathvariant="normal">Σ<!-- Σ --></mml:mi> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi>i</mml:mi> <mml:mo>+</mml:mo> <mml:mn>1</mml:mn> </mml:mrow> <mml:mi>b</mml:mi> </mml:msubsup> <mml:annotation encoding="application/x-tex">\Sigma _{i +...

Abstract We give combinatorial and computational characterizations of the NP search problems definable in bounded arithmetic theories .

Abstract We prove an exponential lower bound on the size of proofs in proof system operating with ordered binary decision diagrams introduced by Atserias, Kolaitis and Vardi [2]. In fact, applies to semantic derivations sets defined OBDDs. do not assume any particular format or ordering variables, hard formulas are CNF. utilize (somewhat indirectly) feasible interpolation. define a combining resolution OBDD system.

Abstract We consider tautologies formed from a pseudo-random number generator, defined in Krajíček [11] and Alekhnovich et al. [2]. explain strategy of proving their hardness for Extended Frege systems via conjecture about bounded arithmetic formulated [11]. Further we give purely finitary statement, the form condition imposed on function, equivalent to conjecture.