We present a novel third-order theory W(1)(1) of bounded arithmetic suitable for reasoning about PSPACE functions. This theory has the advantages of avoiding the smash function symbol and is otherwise much simpler tha...
详细信息
ISBN:
(纸本)3540230246
We present a novel third-order theory W(1)(1) of bounded arithmetic suitable for reasoning about PSPACE functions. This theory has the advantages of avoiding the smash function symbol and is otherwise much simpler than previous PSPACE theories. As an example we outline a proof in W(1)(1) that from any configuration in the game of Hex, at least one player has a winning strategy. We then exhibit a translation of theorems of W(1)(1) into families of propositional tautologies with polynomial-size proofs in BPLK (a recent propositionalproof system for PSPACE and an alternative to G). This translation is clearer and more natural in several respects than the analogous ones for previous PSPACE theories.
This paper shows that any sequence psi(n) of tautologies which expresses the validity of a fixed combinatorial principle either is "easy", i.e. has polynomial size tree-resolution proofs, or is "difficu...
详细信息
This paper shows that any sequence psi(n) of tautologies which expresses the validity of a fixed combinatorial principle either is "easy", i.e. has polynomial size tree-resolution proofs, or is "difficult", i.e. requires exponential size tree-resolution proofs. It is shown that the class of tautologies which are hard (for tree resolution) is identical to the class of tautologies which are based on combinatorial principles which are violated for infinite sets. Further it is shown that the gap phenomenon is valid for tautologies based on infinite mathematical theories (i.e. not just based on a single proposition). A corollary to this classification is that it is undecidable whether a sequence psi(n) has polynomial size tree-resolution proofs or requires exponential size tree-resolution proofs. It also follows that the degree of the polynomial in the polynomial size (in case it exists) is non-recursive, but semi-decidable.
Consider the following system of polynomial equations over a finite prime field Fp. Fix a parameter N≥1 (identified with {0, 1,..., N - 1}). The variables of the system -PHPN are xij, where i∈N and j∈N\{0}. The sys...
详细信息
Consider the following system of polynomial equations over a finite prime field Fp. Fix a parameter N≥1 (identified with {0, 1,..., N - 1}). The variables of the system -PHPN are xij, where i∈N and j∈N\{0}. The system consists of the polynomials (1)Qij := xij^2 - xij, for all i,j, (2)Qi1,i2,j := xi1xi2j, for all i1≠i2,j, (3)Qi,j1,j2 :=xij1xij2, for all i,j1≠j2,(4)Qi := 1- Σjxij, for all i, and the equations stating that all these polynomials are zero. We identify a polynomial system {Fi}i, with the system of equations {Fi = 0}*** system is unsolvable for all N: by the first equation each xij is either 0 or 1, and by the remaining equations the set {(i, j)| xij = 1} is a graph of an injective mapping from N into N\{0}, violating the pigeonhole principle (hence the name -PHPN).
We introduce a notion of a real game (a generalisation of the Karchmer-Wigderson game (cf. [3]) and of real communication complexity, and relate this complexity to the size of monotone real formulas and circuits. We g...
详细信息
We introduce a notion of a real game (a generalisation of the Karchmer-Wigderson game (cf. [3]) and of real communication complexity, and relate this complexity to the size of monotone real formulas and circuits. We give an exponential lower bound for tree-like monotone protocols (defined in [4, Definition 2.2]) of small real communication complexity solving the monotone communication complexity problem associated with the bipartite perfect matching problem. This work is motivated by a research in interpolation theorems for propositional logic (by a problem posed in [5, Section 8], in particular). Our main objective is to extend the communication complexity approach of [4, 5] to a wider class of proof systems. In this direction we obtain an effective interpolation in a form of a protocol of small real communication complexity. Together with the above mentioned lower bound for tree-like protocols this yields as a corollary a lower bound on the number of steps for particular semantic derivations of Hall's theorem (these include tree-like cutting planes proofs for which an exponential lower bound was demonstrated in [2]).
暂无评论