Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over GF (2) in Hrubeš-Tzameret [15]. Specifically, we show that the multiplicativity of the determinant function and the Cayley-Hamilton theorem over the integers are provable in the bounded arithmetic theory VNC 2 ; the latter is a first-order theory corresponding to the complexity class NC 2 consisting of problems solvable by uniform families of polynomial-size circuits and O (log 2 n )-depth. This also establishes the existence of uniform polynomial-size propositional proofs operating with NC 2 -circuits of the basic determinant identities over the integers (previous propositional proofs hold only over the two-element field).

Monotone span programs are a linear-algebraic model of computation which were introduced by Karchmer and Wigderson in 1993 [1]. They are known to be equivalent to linear secret sharing schemes, and have various applications in complexity theory and cryptography. Lower bounds for monotone span programs have been difficult to obtain because they use non-monotone operations to compute monotone functions, in fact, the best known lower bounds are quasipolynomial for a function in (nonmonotone) P [2]. A fundamental open problem is to prove exponential lower bounds on monotone span program size for any explicit function. We resolve this open problem by giving exponential lower bounds on monotone span program size for a function in monotone P. This also implies the first exponential lower bounds for linear secret sharing schemes. Our result is obtained by proving exponential lower bounds using Razborov's rank method [3], a measure that is strong enough to prove lower bounds for many monotone models. As corollaries we obtain new proofs of exponential lower bounds for monotone formula size, monotone switching network size, and the first lower bounds for monotone comparator circuit size for a function in monotone P. We also obtain new polynomial degree lower bounds for Nullstellensatz refutations using an interpolation theorem of Pudlak and Sgall [4]. Finally, we obtain quasipolynomial lower bounds on the rank measure for the st-connectivity function, implying tight bounds for st-connectivity in all of the computational models mentioned above.

We prove exponential lower bounds on the size of semantic read-once 3-ary nondeterministic branching programs. Prior to our result the best that was known was for D-ary branching programs with |D| >= 2^{13}.

This paper is a contribution to our understanding of the relationship between uniform and nonuniform proof complexity. The latter studies the lengths of proofs in various propositional proof systems such as Frege and bounded-depth Frege systems, and the former studies the strength of the corresponding logical theories such as VNC1 and V0 in [Cook/Nguyen, 2010]. A superpolynomial lower bound on the length of proofs in a propositional proof system for a family of tautologies expressing a result like the pigeonhole principle implies that the result is not provable in the theory associated with the propositional proof system. We define a new class of bounded arithmetic theories n^epsilon-ioV^\infinity for epsilon < 1 and show that they correspond to complexity classes AltTime(O(1),O(n^epsilon)), uniform classes of subexponential-size bounded-depth circuits DepthSize(O(1),2^O(n^epsilon)). To accomplish this we introduce the novel idea of using types to control the amount of composition in our bounded arithmetic theories. This allows our theories to capture complexity classes that have weaker closure properties and are not closed under composition. We show that the proofs of Sigma^B_0-theorems in our theories translate to subexponential-size bounded-depth Frege proofs. We use these theories to formalize the complexity theory result that problems in uniform NC1 circuits can be computed by uniform subexponential bounded-depth circuits in [Allender/Koucky, 2010]. We prove that our theories contain a variation of the theory VNC1 for the complexity class NC1. We formalize Buss's proof in [Buss, 1993] that the (unbalanced) Boolean Formula Evaluation problem is in NC1 and use it to prove the soundness of Frege systems. As a corollary, we obtain an alternative proof of [Filmus et al, ICALP, 2011] that polynomial-size Frege proofs can be simulated by subexponential-size bounded-depth Frege proofs. Our results can be extended to theories corresponding to other nice complexity classes inside NTimeSpace(n^O(1), n^o(1)) such as NL. This is achieved by essentially formalizing the containment NTimeSpace(n^O(1), n^o(1)) \subseteq AltTime(O(1), O(n^epsilon)) for all epsilon > 0.

An approximate computation of a Boolean function by a circuit or switching network is a computation in which the function is computed correctly on the majority of the inputs (rather than on all inputs). Besides being interesting in their own right, lower bounds for approximate computation have proved useful in many sub areas of complexity theory, such as cryptography and derandomization. Lower bounds for approximate computation are also known as correlation bounds or average case hardness. In this paper, we obtain the first average case monotone depth lower bounds for a function in monotone P. We tolerate errors that are asymptotically the best possible for monotone circuits. Specifically, we prove average case exponential lower bounds on the size of monotone switching networks for the GEN function. As a corollary, we separate the monotone NC hierarchy in the case of errors -- a result which was previously only known for exact computations. Our proof extends and simplifies the Fourier analytic technique due to Potechin, and further developed by Chan and Potechin. As a corollary of our main lower bound, we prove that the communication complexity approach for monotone depth lower bounds does not naturally generalize to the average case setting.

In 1989 Kushilevitz initiated the study of iinformation-theoretic privacy within the context of communication complexity. Unfortunately, it has been shown that most interesting functions are not privately computable. The unattainability of perfect privacy for many functions motivated the study of approximate privacy. Feigenbaum et al. define notions of worst-case as well as average-case approximate privacy, and present several interesting upper bounds, and some open problems for further study. In this paper, we obtain asymptotically tight bounds on the tradeoffs between both the worst-case and average-case approximate privacy of protocols and their communication cost for Vickrey-auctions. Further, we relate the notion of average-case approximate privacy to other measures based on information cost of protocols. This enables us to prove exponential lower bounds on the subjective approximate privacy of protocols for computing the Intersection function, independent of its communication cost. This proves a conjecture of Feigenbaum et al.

The Jordan curve theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded arithmetic that correspond to small complexity classes. The theory V 0 (2) (corresponding to AC 0 (2)) proves that any set of edges that form disjoint cycles divides the grid into at least two regions. The theory V 0 (corresponding to AC 0 ) proves that any sequence of edges that form a simple closed curve divides the grid into exactly two regions. As a consequence, the Hex tautologies and the st-connectivity tautologies have polynomial size AC 0 (2)- Frege -proofs, which improves results of Buss which only apply to the stronger proof system TC 0 - Frege .

Using Jerábek's framework for probabilistic reasoning, we formalize the correctness of two fundamental RNC^2 algorithms for bipartite perfect matching within the theory VPV for polytime reasoning. The first algorithm is for testing if a bipartite graph has a perfect matching, and is based on the Schwartz-Zippel Lemma for polynomial identity testing applied to the Edmonds polynomial of the graph. The second algorithm, due to Mulmuley, Vazirani and Vazirani, is for finding a perfect matching, where the key ingredient of this algorithm is the Isolating Lemma.

We propose a new framework for discussing computational complexity of problems involving uncountably many objects, such as real numbers, sets and functions, that can be represented only through approximation. The key idea is to use a certain class of string functions, which we call regular functions, as names representing these objects. These are more expressive than infinite sequences, which served as names in prior work that formulated complexity in more restricted settings. An important advantage of using regular functions is that we can define their size in the way inspired by higher-type complexity theory. This enables us to talk about computation on regular functions whose time or space is bounded polynomially in the input size, giving rise to more general analogues of the classes P, NP, and PSPACE. We also define NP- and PSPACE-completeness under suitable many-one reductions.

We study the branching program complexity of the {\em tree evaluation problem}, introduced in \cite{BrCoMcSaWe09} as a candidate for separating \nl\ from\logcfl. The input to the problem is a rooted, balanced $d$-ary tree of height$h$, whose internal nodes are labelled with $d$-ary functions on$[k]=\{1,\ldots,k\}$, and whose leaves are labelled with elements of $[k]$.Each node obtains a value in $[k]$ equal to its $d$-ary function applied to the values of its $d$ children. The output is the value of the root. Deterministic $k$-way branching programs as related to black pebbling algorithms have been studied in \cite{BrCoMcSaWe09}. Here we introduce the notion of {\em fractional pebbling} of graphs to study non-deterministicbranching program size. We prove that this yields non-deterministic branching programs with $\Theta(k^{h/2+1})$ states solving the Boolean problem ``determine whether the root has value 1'' for binary trees - this isasymptotically better than the branching program size corresponding toblack-white pebbling. We prove upper and lower bounds on the fractionalpebbling number of $d$-ary trees, as well as a general result relating thefractional pebbling number of a graph to the black-white pebbling number. We introduce a simple semantic restriction called {\em thrifty} on $k$-way branching programs solving tree evaluation problems and show that the branchingprogram size bound of $\Theta(k^h)$ is tight (up to a constant factor) for all $h\ge 2$ for deterministic thrifty programs. We show that thenon-deterministic branching programs that correspond to fractional pebbling are thrifty as well, and that the bound of $\Theta(k^{h/2+1})$ is tight for non-deterministic thrifty programs for $h=2,3,4$. We hypothesise that thrifty branching programs are optimal among $k$-way branching programs solving the tree evaluation problem - proving this for deterministic programs would separate \lspace\ from \logcfl\, and proving it for non-deterministic programs would separate \nl\ from \logcfl.

The Jordan Curve Theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded arithmetic that correspond to small complexity classes. The theory V0(corresponding to AC0(2)) proves that any set of edges that form disjoint cycles divides the grid into at least two regions. The theory V0(corresponding to AC0) proves that any sequence of edges that form a simple closed curve divides the grid into exactly two regions. As a consequence, the Hex tautologies and the st-Connectivity tautologies have polynomial size AC0(2)-Frege-proofs, which improves results of Buss which only apply to the stronger proof system TC0-Frege.

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

We present a general method for introducing finitely axiomatizable "minimal" two-sorted theories for various subclasses of P (problems solvable in polynomial time). The two sorts are natural numbers and finite sets of natural numbers. The latter are essentially the finite binary strings, which provide a natural domain for defining the functions and sets in small complexity classes. We concentrate on the complexity class TC^0, whose problems are defined by uniform polynomial-size families of bounded-depth Boolean circuits with majority gates. We present an elegant theory VTC^0 in which the provably-total functions are those associated with TC^0, and then prove that VTC^0 is "isomorphic" to a different-looking single-sorted theory introduced by Johannsen and Pollet. The most technical part of the isomorphism proof is defining binary number multiplication in terms a bit-counting function, and showing how to formalize the proofs of its algebraic properties.

Thereplacement(orcollectionorchoice) axiom scheme BB(Γ) asserts bounded quantifier exchange as follows: ∀i< |a| ∃x<aϕ(i,x) → ∃w∀i< |a|ϕ(i,[w]i), for ϕ in the class Γ of formulas. The theoryS12proves the scheme BB(Σb1), and thus inS12every Σb1formula is equivalent to a strict Σb1formula (in which all non-sharply-bounded quantifiers are in front). Here we prove (sometimes subject to an assumption) that certain theories weaker thanS12do not prove either BB(Σb1) or BB(Σb0). We show (unconditionally) thatV0does not prove BB(Σb0), where V0(essentially IΣ1,b0) is the two-sorted theory associated with the complexity class AC0. We show that PV does not prove BB(Σb0), assuming that integer factoring is not possible in probabilistic polynomial time. Johannsen and Pollett introduced the theoryC02associated with the complexity class TC0, and later introduced an apparently weaker theory Δb1− CR for the same class. We use our methods to show that Δb1− CR is indeed weaker thanC02, assuming that RSA is secure against probabilistic polynomial time attack.Our main tool is the KPT witnessing theorem.

We introduce a second-order theory V-Krom of bounded arithmetic for nondeterministic log space. This system is based on Gradel's characterization of NL by second-order Krom formulae with only universal first-order quantifiers, which in turn is motivated by the result that the decision problem for 2-CNF satisfiability is complete for coNL (and hence for NL). This theory has the style of the authors' theory Vi-Horn [APAL 124 (2003)] for polynomial time. Both theories use Zambella's elegant second-order syntax, and are axiomatized by a set 2-BASIC of simple formulae, together with a comprehension scheme for either second-order Horn formulae (in the case of V/sub 1/-Horn), or second-order Krom (2CNF) formulae (in the case of V-Krom). Our main result for V-Krom is a formalization of the Immerman-Szelepcsenyi theorem that NL is closed under complementation. This formalization is necessary to show that the NL functions are /spl Sigma//sub 1//sup B/-definable in V-Krom. The only other theory for NL in the literature relies on the Immerman-Szelepcsenyi's result rather than proving it.

The replacement (or collection or choice,) axiom scheme BB(/spl Gamma/) asserts bounded quantifier exchange as follows: /spl forall/I < |a| /spl exist/x < ao(i, x) /spl rarr/ /spl exist/w /spl forall/i < |a| o (i, [w]/sub i/) where o is in the class /spl Gamma/ of formulas. The theory S/sub 2//sup 1/ proves the scheme BB(/spl Sigma//sub 1//sup b/), and thus in S/sub 2//sup 1/ every /spl Sigma//sub 1//sup b/ formula is equivalent to a strict /spl Sigma//sub 1//sup b/ formula (in which all non-sharply-bounded quantifiers are in front). Here we prove (sometimes subject to an assumption) that certain theories weaker than S/sub 2//sup 1/ do not prove either BB(/spl Sigma//sub 1//sup b/) or BB(/spl Sigma//sub 0//sup b/). We show (unconditionally) that V/sup 0/ does not prove BB(/spl Sigma//sub 1//sup B/), where V/sup 0/ (essentially I/spl Sigma//sub 0//sup 1,b/) is the two-sorted theory associated with the complexity class AC/sup 0/. We show that PV does not prove BB(/spl Sigma//sub 0//sup b/), assuming that integer factoring is not possible in probabilistic polynomial time. Johannsen and Pollet introduced the theory C/sub 2//sup 0/ associated with the complexity class TC/sup 0/, and later introduced an apparently weaker theory /spl Delta//sub 1//sup b/ - CR for the same class. We use our methods to show that /spl Delta//sub 1//sup b/ - CR is indeed weaker than C/sub 2//sup 0/, assuming that RSA is secure against probabilistic polynomial time attack. Our main tool is the KPT witnessing theorem.

We introduce a finitely axiomatizable second-order theory, which is VTC/sup 0/ associated with the class FO-uniform TC/sup 0/. It consists of the base theory V/sup 0/ for AC/sup 0/ reasoning together with the axiom NUMONES, which states the existence of a "counting array" Y for any string X: the ith row of Y contains only the number of 1 bits up to (excluding) bit i of X. We introduce the notion of "strong /spl Delta//sub 1//sup B/-definability" for relations in a theory, and use a recursive characterization of the TC/sup 0/ relations (rather than functions) to show that the TC/sup 0/ relations are strongly /spl Delta//sub 1//sup B/-definable. It follows that the TC/sup 0/ functions are /spl Sigma//sub 1//sup B/-definable in VTC/sup 0/. We prove a general witnessing theorem for second-order theories and conclude that the/spl Sigma//sub 1//sup B/ theorems of VTC/sup 0/ are witnessed by TC/sup 0/ functions. We prove that VTC/sup 0/ is RSUV isomorphic to the first order theory /spl Delta//sub 1//sup b/-CR of Johannsen and Pollett (the "minimal theory for TC/sup 0/"), /spl Delta//sub 1//sup b/-CR includes the /spl Delta//sub 1//sup b/ comprehension rule, and J and P ask whether there is an upper bound to the nesting depth required for this rule. We answer "yes", because VTC/sup 0/ , and therefore /spl Delta//sub 1//sup b/-CR, are finitely axiomatizable. Finally, we show that /spl Sigma//sub 1//sup B/ theorems of VTC/sup 0/ translate to families of tautologies which have polynomial-size constant-depth TC/sup 0/-Frege proofs. We also show that PHP is a /spl Sigma//sub 0//sup B/ theorem of VTC/sup 0/. These together imply that the family of propositional tautologies associated with PHP has polynomial-size constant-depth TC/sup 0/-Frege proofs.

The P versus NP problem is to determine whether every language accepted by some nondeterministic Turing machine in polynomial time is also accepted by some de-terministic Turing machine in polynomial time. Unquestionably this problem has caught the interest of the mathematical community. For example, it is the first of seven million-dollar “Millennium Prize Problems ” listed by the Clay Mathematics Institute [www.claymath.org]. The Riemann Hypothesis and Poincare ́ Conjec-ture, both mathematical classics, are farther down the list. On the other hand, Fields Medalist Steve Smale lists P versus NP as problem number three, after Riemann and Poincaré, in “Mathematical Problems for the Next Century ” [Smale 1998]. But P versus NP is also a problem of central interest in computer science. It was posed thirty years ago [Cook 1971; Levin 1973] as a problem concerned with the fundamental limits of feasible computation. Although this question is front and center in complexity theory, NP-completeness proofs have become pervasive in many other areas of computer science, including artificial intelligence, databases, programming languages, and computer networks (see Garey and Johnson [1979]

Blocks World (BW) has been one of the most popular model domains in AI history. However, there has not been serious work on axiomatizing the state constraints of BW and giving justification for its soundness and completeness. In this paper, we model a state of BW by a finite collection of finite chains, and call the theory of all these structures BW theory. We present seven simple axioms and prove that their consequences are precisely BW theory, using Ehrenfeucht-Fraïssé games. We give a simple decision procedure for the theory which can be implemented in exponential space, and prove that every decision procedure (even if nondeterministic) for the theory must take at least exponential time. We also give a characterization of all nonstandard models for the theory. Finally, we present an expansion of BW theory and show that it admits elimination of quantifiers. As a result, we are able to characterize all definable predicates in BW theory, and give simple examples of undefinable predicates.

We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley-Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities.

We introduce a second-order system V/sub 1/-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Gradel's (1992) second-order Horn characterization of P. Our system has comprehension over P predicates (defined by Gradel's second-order Horn formulas), and only finitely, many function symbols. Other systems of polynomial-time reasoning either allow induction on NP predicates (such as Buss's (1986) S/sub 2//sup 1/ or the second-order V/sub 1//sup 1/), and hence are more powerful than our system (assuming the polynomial hierarchy does not collapse), or use Cobham's theorem to introduce function symbols for all polynomial-time functions (such as Cook's PV and Zambella's P-def). We prove that our system is equivalent to QPV and Zambella's (1996) P-def. Using our techniques, we also show that V/sub 1/-Horn is finitely, axiomatizable, and, as a corollary, that the class of /spl forall//spl Sigma//sub 1//sup b/ consequences of S/sub 2//sup 1/ is finitely axiomatizable as well, thus answering an open question.

K. Mehlhorn introduced a class of polynomial-time-computable operators in order to study poly-time reducibilities between functions. This class is defined using a generalization of A. Cobham's definition of feasibility for type-1 functions to type-2 functionals. Cobham's feasible functions are equivalent to the familiar poly-time functions. We generalize this equivalence to type-2 functionals. This requires a definition of the notion “poly time in the length of type-1 inputs.” The proof of this equivalence is not a simple generalization of the proof for type-1 functions; it depends on the fact that Mehlhorn’s class is closed under a strong form of simultaneous limited recursion on notation and requires an analysis of the structure of oracle queries in time-bounded computations.

Papadimitriou introduced several classes of NP search problems based on combinatorial principles which guarantee the existence of solutions to the problems.Many interesting search problems not known to be solvable in polynomial time are contained in these classes, and a number of them are complete problems.We consider the question of the relative complexity of these search problem classes.We prove several separations which show that in a generic relativized world, the search classes are distinct and there is a standard search problem in each of them that is not computationally equivalent to any decision problem.(Naturally, absolute separations would imply that P 6 = NP.)Our separation proofs have interesting combinatorial content and go to the heart of the combinatorial principles on which the classes are based.We derive one result via new lower bounds on the degrees of polynomials asserted to exist by Hilbert's Nullstellensatz over nite elds.

We give a recursion-theoretic characterization of FP which describes polynomial time computation independently of any externally imposed resource bounds. In particular, this syntactic characterization avoids the explicit size bounds on recursion (and the initial function 2|x|.|y|) of Cobham.

A new approach to Buss’s ${\textbf{NC}}^1 $ algorithm [Proc. 19th ACM Symposium on Theory of Computing, Association for Computing Machinery, New York, 1987, pp. 123–131] for evaluation of Boolean formulas is presented. This problem is shown to be complete for ${\textbf{NC}}^1 $ over ${\textbf{AC}}^0 $ reductions. This approach is then used to solve the more general problem of evaluating arithmetic formulas by using arithmetic circuits.

A. Cobham (1964) presented a machine-independent characterization of computational feasibility, via inductive definition. R. Constable (1973) was apparently the first to consider the notion of feasibility for type 2 functionals. K. Mehlhorn's (1976) study of feasible reducibilities proceeds from Constable's work. Here, a class of polytime operators is defined, using a generalization of Cobham's definition. The authors provide an affirmative answer to the question of whether there is a natural machine based definition of Mehlhorn's class.>

The authors define a simple typed while-programming language that generalizes the sort of simple language used in computability texts to define the familiar numerical computable functions and corresponds roughly to the mu -recursion of R.O. Gandy (1967). This language does not fully capture the notion of higher type computability. The authors define run times for their programs and prove that the feasible functionals of S. Cook and A. Urquhart (1988) are precisely those functionals computable by typed while-programs with run times feasibly length-bounded. The authors introduce the notion of a bounded typed loop program and prove that a finite type functional is feasible if it is computable by a bounded typed loop program.>

Article Free Access Share on Functional interpretations of feasibly constructive arithmetic Authors: S. Cook Department of Computer Science, University of Toronto, Toronto, Canada Department of Computer Science, University of Toronto, Toronto, CanadaView Profile , A. Urquhart Department of Philosophy, University of Toronto, Toronto, Canada Department of Philosophy, University of Toronto, Toronto, CanadaView Profile Authors Info & Claims STOC '89: Proceedings of the twenty-first annual ACM symposium on Theory of computingFebruary 1989 Pages 107–112https://doi.org/10.1145/73007.73017Online:01 February 1989Publication History 18citation150DownloadsMetricsTotal Citations18Total Downloads150Last 12 Months4Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Following the recent independent proofs of Immerman [SIAM J. Comput., 17 (1988), pp. 935–938] and Szelepcsenyi [Bull. European Assoc. Theoret. Comput. Sci., 33 (1987), pp. 96–100] that nondeterministic space-bounded complexity classes are closed under complementation, two further applications of the inductive counting technique are developed. First, an errorless probabilistic algorithm for the undirected graph s-t connectivity problem that runs in $O(\log n)$ space and polynomial expected time is given. Then it is shown that the class LOGCFL is closed under complementation. The latter is a special case of a general result that shows closure under complementation of classes defined by semi-unbounded fan-in circuits (or, equivalently, nondeterministic auxiliary pushdown automata or tree-size bounded alternating Turing machines). As one consequence, it is shown that small numbers of “role switches” in two-person pebbling can be eliminated.

Previous article Full AccessErratum: Two Applications of Indctive Counting for Complementation ProblemsAllan Borodin, Stephen A. Cook, Patrick W. Dymond, Walter L. Ruzzo, and Martin TompaAllan Borodin, Stephen A. Cook, Patrick W. Dymond, Walter L. Ruzzo, and Martin Tompahttps://doi.org/10.1137/0218084PDFBibTexSections ToolsAdd to favoritesExport CitationTrack CitationsEmail SectionsAbout"Erratum: Two Applications of Indctive Counting for Complementation Problems." SIAM Journal on Computing, 18(6), p. 1283[1] Allan Borodin, , Stephen A. Cook, , Patrick W. Dymond, , Walter L. Ruzzo and , Martin Tompa, Two applications of inductive counting for complementation problems, SIAM J. Comput., 18 (1989), 559–578 10.1137/0218038 90k:68049a 0678.68031 LinkISIGoogle Scholar[2] John Gill, Computational complexity of probabilistic Turing machines, SIAM J. Comput., 6 (1977), 675–695 10.1137/0206049 57:4616 0366.02024 LinkISIGoogle Scholar[3] Hermann Jung, On probabilistic time and spaceAutomata, languages and programming (Nafplion, 1985), Lecture Notes in Comput. Sci., Vol. 194, Springer, Berlin, 1985, 310–317 87b:68039 0599.68043 CrossrefGoogle Scholar Previous article FiguresRelatedReferencesCited byDetails Dual VP Classes23 September 2016 | computational complexity, Vol. 26, No. 3 Cross Ref Input Reversals and Iterated Pushdown Automata: A New Characterization of Khabbaz Geometric Hierarchy of Languages Cross Ref Computational Complexity Cross Ref Trading Space for Time in Undirected s-t ConnectivityAndrei Z. Broder, Anna R. Karlin, Prabhakar Raghavan, and Eli Upfal31 July 2006 | SIAM Journal on Computing, Vol. 23, No. 2AbstractPDF (1266 KB)My favorite ten complexity theorems of the past decade1 June 2005 Cross Ref Lower bounds on the length of universal traversal sequencesJournal of Computer and System Sciences, Vol. 45, No. 2 Cross Ref A very hard log space counting class Cross Ref Volume 18, Issue 6| 1989SIAM Journal on Computing History Submitted:03 August 1989Accepted:30 August 1989Published online:13 July 2006 InformationCopyright © 1989 Society for Industrial and Applied MathematicsPDF Download Article & Publication DataArticle DOI:10.1137/0218084Article page range:pp. 1283-1283ISSN (print):0097-5397ISSN (online):1095-7111Publisher:Society for Industrial and Applied Mathematics

We classify Abelian permutation group problems with respect to their parallel complexity. For such groups specified by generating permutations we show that testing membership, computing order and testing isomorphism are $NC^1 $-equivalent to (and therefore have essentially the same parallel complexity as) determining solvability of a system of linear equations modulo a product of small prime powers; we show that intersecting two such groups is $NC^1 $-equivalent to computing setwise stabilizers; we show that each of these problems is $NC^1 $-reducible to the problem of computing a generator-relator presentation. Then we prove that the aforementioned problems belong to $NC^3 $, thus identifying several natural set recognition problems in $NC$ which may lie outside $NC^2 $. Finally we prove that $NC^4 $ contains the problem of computing the cyclic decomposition of an Abelian permutation group. Background results include an $NC^1 $ solution to the problem of computing the product of n integers modulo a $\lceil {\log n} \rceil $-bit integer, and an $NC^1 $ reduction from the problem of computing a path between two nodes in a graph to that of determining accessibility of one node from another.

We present optimal depth Boolean circuits (depth $O(\log n)$) for integer division, powering, and multiple products. We also show that these three problems are of equivalent uniform depth and space complexity. In addition, we describe an algorithm for testing divisibility that is optimal for both depth and space.

One of the frequently used models for a synchronous parallel computer is that of a parallel random access machine, where each processor can read from and write into a common random access memory. Different processors may read the same memory location at the same time, but simultaneous writing is disallowed. We show that even if we allow nonuniform algorithms, an arbitrary number of processors, and arbitrary instruction sets, $\Omega (\log n)$ is a lower bound on the time required to compute various simple functions, including sorting n keys and finding the logical “or” of n bits. We also prove a surprising time upper bound of $.72\log _2 n$ steps for these functions, which beats the obvious algorithms requiring $\log _2 n$ steps.If simultaneous writes are allowed, there are simple algorithms to compute these functions in a constant number of steps.

This paper describes a family of depth-universal circuits. For any n, c, d there is a universal circuit $U(n,c,d)$ that can simulate any circuit $\alpha $ having n inputs, of size c and depth d, and U has depth $O(d)$ and size $O(c^3 d/\log c)$. The construction is used to give an alternative proof of a theorem of Ruzzo showing the invariance under different uniformity conditions of complexity classes defined by uniform circuit families.

We present optimal depth Boolean circuits (depth O(log n)) for integer division, powering, and multiple products. We also show that these three problems are of equivalent uniform depth and space complexity. In addition, we describe an algorithm for testing divisibility that is optimal for both depth and space.

We show that the permutation group membership problem can be solved in depth (logn)3 on a Monte Carlo Boolean circuit of polynomial size in the restricted case in which the group is abelian. We also show that this restricted problem is NC1-hard for NSPACE(logn).

Let S(n) be a nice space bound such that log2 n S(n) n. Then every DCFL is recognized by a multitape Turing machine simultaneously in time O(n2/S(n)) and space O(S(n)), and this time bound is optimal. If the machine is allowed a random access input, then the time bound can be improved so that the time-space product is O(n1 + ).

We prove that a parallel RAM with no write conflicts allowed requires Ω(log n) steps to compute the Boolean or of n bits stored in the first n global memory cells. We first argue that this result is subtler than it appears, and in fact the “obvious” lower bound of log2n steps can be beaten.

In a general sequential model of computation, no restrictions are placed on the way in which the computation may proceed, except that parallel operations are not allowed. We show that in such an unrestricted environment ${\text{TIME}} \cdot {\text{SPACE}} = \Omega (N^2 /\log N)$ in order to sort N integers, each in the range $[1,N^2 ]$.

Previous article Next article Full AccessCorrigendum: Soundness and Completeness of an Axiom System for Program VerificationStephen A. CookStephen A. Cookhttps://doi.org/10.1137/0210045PDFBibTexSections ToolsAdd to favoritesExport CitationTrack CitationsEmail SectionsAbout"Corrigendum: Soundness and Completeness of an Axiom System for Program Verification." SIAM Journal on Computing, 10(3), p. 612 Previous article Next article FiguresRelatedReferencesCited byDetails Completeness and Complexity of Reasoning about Call-by-Value in Hoare LogicACM Transactions on Programming Languages and Systems, Vol. 43, No. 4 Cross Ref A decision procedure and complete axiomatization for projection temporal logicTheoretical Computer Science, Vol. 819 Cross Ref On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics22 April 2020 Cross Ref Fifty years of Hoare's logicFormal Aspects of Computing, Vol. 31, No. 6 Cross Ref Ogre and Pythia: an invariance proof method for weak consistency modelsACM SIGPLAN Notices, Vol. 52, No. 1 Cross Ref Ogre and Pythia: an invariance proof method for weak consistency models1 January 2017 Cross Ref Program Verification: To Err is Human13 March 2016 Cross Ref Automated compositional proofs for real-time systemsTheoretical Computer Science, Vol. 376, No. 3 Cross Ref Hoare's logic for programming languages with two data typesTheoretical Computer Science, Vol. 28, No. 1-2 Cross Ref Expressiveness and the completeness of Hoare's logicJournal of Computer and System Sciences, Vol. 25, No. 3 Cross Ref Volume 10, Issue 3| 1981SIAM Journal on Computing History Published online:13 July 2006 InformationCopyright © 1981 Society for Industrial and Applied MathematicsPDF Download Article & Publication DataArticle DOI:10.1137/0210045Article page range:pp. 612-612ISSN (print):0097-5397ISSN (online):1095-7111Publisher:Society for Industrial and Applied Mathematics

In a general sequential model of computation, no restrictions are placed on the way in which the computation may proceed, except parallel operations are not allowed. We show that in such an unrestricted environment TIME•SPACE=Ω(N2/log N) in order to sort N elements, each in the range [1,N2].

A restricted model of a Turing machine called a JAG (Jumping Automaton for Graphs) is introduced for solving the maze threadability problem (determining whether there is a path joining two distinguished nodes in an input graph). A JAG accesses its input graph by moving pebbles from a limited supply along the edges of the graph under a finite state control, and detecting when two pebbles coincide. It can also cause one pebble to jump to another. We prove that for every N there is a JAG which can determine threadability of an arbitrary N node input graph in storage $O((\log N)^2 )$, where the storage of a JAG with Ppebbles and N states is defined to be $P\log N + \log Q$. Further, we prove that any JAG which determines threadability requires storage $\Omega ((\log N)^2 /\log \log N)$. Finally, we prove that even when the inputs are restricted to undirected graphs (with no bound on the number of nodes), no single JAG can determine threadability.

We propose to prove the theorem in the title. Let PLOSS be the class of sets recognizable on a deterministic Turing machine simultaneously in polynomial time and log squared space. Using the notation of Bruss and Meyer [1], PLOSS = υk TISP(nk,k log2n).

We are interested in studying the length of the shortest proof of a propositional tautology in various proof systems as a function of the length of the tautology. The smallest upper bound known for this function is exponential, no matter what the proof system. A question we would like to answer (but have not been able to) is whether this function has a polynomial bound for some proof system. (This question is motivated below.) Our results here are relative results. In §§2 and 3 we indicate that all standard Hilbert type systems (or Frege systems, as we call them) and natural deduction systems are equivalent, up to application of a polynomial, as far as minimum proof length goes. In §4 we introduce extended Frege systems, which allow introduction of abbreviations for formulas. Since these abbreviations can be iterated, they eliminate the need for a possible exponential growth in formula length in a proof, as is illustrated by an example (the pigeonhole principle). In fact, Theorem 4.6 (which is a variation of a theorem of Statman) states that with a penalty of at most a linear increase in the number of lines of a proof in an extended Frege system, no line in the proof need be more than a constant times the length of the formula proved.

A simple ALGOL-like language is defined which includes conditional, while, and procedure call statements as well as blocks. A formal interpretive semantics and a Hoare style axiom system are given for the language. The axiom system is proved to be sound, and in a certain sense complete, relative to the interpretive semantics. The main new results are the completeness theorem, and a careful treatment of the procedure call rules for procedures with global variables in their declarations.

The number of addition-subtraction operations required to compute univariate pol nomials is investigated. The existence of rational coefficient polynomials of degree n requiring $ \sim (\sqrt n ) \pm $ operations is established using an argument based on algebraic independence. A more analytic argument is used to relate $ \pm $ complexity to the number of distinct real zeros possessed by a given real coefficient polynomial.

In this paper we wish to consider the problem of proving assertions about programs that construct and alter arbitrarily complex data structures. In recent years several papers have been written on the subject of proving assertions about such programs; however, the class of data structures considered has generally been a proper sub-class of the class of all data structures, such as the classes of linear lists or trees. [Burstall 1972] discusses the problem of what he calls Distinct Non-repeating Lists and Distinct Non-repeating Trees. [Kowaltowski 1973] extends Burstall's approach. His approach is likewise basically tree-oriented but is applicable to more general data structures. [Laventhal 1974] restricts his attention to 'simple singly-linked lists', noting the problem of providing 'a complete framework for correctness proofs' if one attempts to handle very general data structures. [Morris 1972] discusses the question of designing a programming language for general data structures in order to facilitate verification of programs written in such a language. [Standish 1973] provides a set of axioms for the class of data structures in which, for instance, two data structures are equal iff they are component-wise equal.

The motivation for this work comes from two general sources. The first source is the basic open question in complexity theory of whether P equals NP (see [1] and [2]). Our approach is to try to show they are not equal, by trying to show that the set of tautologies is not in NP (of course its complement is in NP). This is equivalent to showing that no proof system (in the general sense defined in [3]) for the tautologies is “super” in the sense that there is a short proof for every tautology. Extended resolution is an example of a powerful proof system for tautologies that can simulate most standard proof systems (see [3]). The Main Theorem (5.5) in this paper describes the power of extended resolution in a way that may provide a handle for showing it is not super.

In this paper we wish to consider the problem of proving assertions about programs that construct and alter data structures. Our method will be to define a suitable assertion language L for data structures, to define a simple programming language L' for constructing and altering data structures, to give axioms and rules of inference (in the style of [Hoare 1969]) which specify the effect of program segments on data structures (described by formulas in L) and finally to prove that these axioms are correct (relative to a formal definition of the semantics of L') and, in a reasonable sense, complete. Thus our intention is to provide a complete theoretical framework for describing arbitrary data structures and proving assertions about programs that manipulate them.

It is well known from the work of Motzkin [55], Belaga [58] and Pan [66], that “most” nth degree polynomials p ε R[x] require about n/2 ×, ÷ ops and n ± ops and that these bounds can always be achieved within the framework of preconditioned evaluation (1). More precisely, if p can be computed using less than [equation] ×, ÷ or less than n ± ops, then the coefficients of p are algebraically dependent.

One of the most important open questions in the field of computational complexity is the question of whether there is a polynomial time decision procedure for the classical propositional calculus.

A striking example of practical tradeoffs between storage space and execution time is provided by the IBM 1401 Fortran compiler.

@ (i.e., recognizable in deterministic polynomial time) can be recognized in deterministic storage (log n)2. The methods used in the attempts were based on that of [1], in which it is shown that every context free language can be accepted in storage (log n)2 Our thesis in the present paper is that these attempts must fail. We define a specific set SP of strings which is clearly in

The purpose of this paper is to prove the following result:

In this paper we introduce a formal model for random access computers and argue that the model is a good one to use in the theory of computational complexity. Results are proved which compare run times for recognizing sets using this model (which has a fixed program) with a stored program model and with Turing machines. The main result, theorem 3, shows the existence of a time complexity hierarchy which is finer than that of any standard abstract computer model. An Algol-like programming language is introduced which facilitates proofs of the theorems.

It is shown that any recognition problem solved by a polynomial time-bounded nondeterministic Turing machine can be “reduced” to the problem of determining whether a given propositional formula is a tautology. Here “reduced” means, roughly speaking, that the first problem can be solved deterministically in polynomial time provided an oracle is available for solving the second. From this notion of reducible, polynomial degrees of difficulty are defined, and it is shown that the problem of determining tautologyhood has the same polynomial degree as the problem of determining whether the first of two given graphs is isomorphic to a subgraph of the second. Other examples are discussed. A method of measuring the complexity of proof procedures for the predicate calculus is introduced and discussed.

A class of machines called auxiliary pushdown machines is introduced.Several types of pushdown automata, including stack automata, are characterized in terms of these machines.The computing power of each class of machines in question is characterized in terms of time-bounded Turing machines, and corollaries are derived which answer some open questions in the field.

Our main result, theorem 2, gives a bound on the storage required for a Turing machine to simulate certain time-bounded pushdown machines. The theorem is a generalization of the result appearing in [3] stating that any context-free language can be recognized by a deterministic Turing machine within storage (log n)2. We introduce a combinatorial object, called a path system, develop its theory briefly, and use the theory to prove both the result on pushdown machines and the result on context free languages, as well as a third result. The third result is the Theorem of Savitch [5] stating that a non-deterministic L(n) - storage bounded Turing machine can be simulated by a deterministic (L(n))2 - storage bounded Turing machine.

A class of machines called auxiliary pushdown machines is introduced. Several types of pushdown automata, including stack automata, are characterized in terms of these machines. The computing power of each class of machines in question is characterized in terms of time bounded Turing machines, and corollaries are derived which answer some open questions in the field.

A one-normal system is a Post production system on a finite alphabet { s 1 , s 2 , · · ·, s σ } with productions s i P → PE ij , where i ranges over a subset of {1, 2, · · ·, σ} and, for fixed i , j takes on the values 1, 2, · · ·, n i . The following derivability problem is shown to be solvable for each such system: Given two words P and Q , decide whether Q can be derived from P by successive applications of the production rules. The result was proved by Hao Wang for the monogenic case (i.e., when each n i = 1).