We present a new extended resolution clause learning (ERCL) algorithm, implemented as part of a conflict-driven clause-learning (CDCL) SAT solver, wherein new variables are dynamically introduced as definitions for {\it Dual Implication Points} (DIPs) in the implication graph constructed by the solver at runtime. DIPs are generalizations of unique implication points and can be informally viewed as a pair of dominator nodes, from the decision variable at the highest decision level to the conflict node, in an implication graph. We perform extensive experimental evaluation to establish the efficacy of our ERCL method, implemented as part of the MapleLCM SAT solver and dubbed xMapleLCM, against several leading solvers including the baseline MapleLCM, as well as CDCL solvers such as Kissat 3.1.1, CryptoMiniSat 5.11, and SBVA+CaDiCaL, the winner of SAT Competition 2023. We show that xMapleLCM outperforms these solvers on Tseitin and XORified formulas. We further compare xMapleLCM with GlucoseER, a system that implements extended resolution in a different way, and provide a detailed comparative analysis of their performance.

Regular resolution is a refinement of the resolution proof system requiring that no variable be resolved on more than once along any path in the proof. It is known that there exist sequences of formulas that require exponential-size proofs in regular resolution while admitting polynomial-size proofs in resolution. Thus, with respect to the usual notion of simulation, regular resolution is separated from resolution. An alternative, and weaker, notion for comparing proof systems is that of an “effective simulation,” which allows the translation of the formula along with the proof when moving between proof systems. We prove that regular resolution is equivalent to resolution under effective simulations. As a corollary, we recover in a black-box fashion a recent result on the hardness of automating regular resolution.

We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory ‍V20 is consistent with the conjecture that ‍NEXP ‍⊈ ‍P/poly, i.e., some problem that is solvable in non-deterministic exponential time does not have polynomial size circuits. We suggest this is the best currently available evidence for the truth of the conjecture. Additionally, we establish a magnification result on the hardness of proving circuit lower bounds.

This article is motivated by seeking lower bounds on OBDD(∧, w, r) refutations, namely, OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1 - NBP ∧ refutations based on read-once nondeterministic branching programs. These generalize OBDD(∧, r) refutations. There are polynomial size 1 - NBP(∧) refutations of the pigeonhole principle, hence 1-NBP(∧) is strictly stronger than OBDD}(∧, r). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP(∧) refutations. As a corollary, OBDD}(∧, r) does not simulate tree-like resolution, answering a previously open question. The system 1-NBP(∧, ∃) uses projection inferences instead of weakening. 1-NBP(∧, ∃ k is the system restricted to projection on at most k distinct variables. We construct explicit constant degree graphs G n on n vertices and an ε > 0, such that 1-NBP(∧, ∃ ε n ) refutations of the Tseitin formula for G n require exponential size. Second, we study the proof system OBDD}(∧, w, r ℓ ), which allows ℓ different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD(∧, w, r ℓ ) refutations for ℓ = ε log n , where n is the number of variables and ε > 0 is a constant. The lower bound is based on multiparty communication complexity.

This paper studies propositional proof systems in which lines are sequents of decision trees or branching programs - deterministic and nondeterministic. The systems LDT and LNDT are propositional proof systems in which lines represent deterministic or non-deterministic decision trees. Branching programs are modeled as decision dags. Adding extension to LDT and LNDT gives systems eLDT and eLNDT in which lines represent deterministic and non-deterministic branching programs, respectively. Deterministic and non-deterministic branching programs correspond to log-space (L) and nondeterministic log-space (NL). Thus the systems eLDT and eLNDT are propositional proof systems that reason with (nonuniform) L and NL properties. The main results of the paper are simulation and non-simulation results for tree-like and dag-like proofs in the systems LDT, LNDT, eLDT, and eLNDT. These systems are also compared with Frege systems, constantdepth Frege systems and extended Frege systems

We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [44], and show that this analysis can be formalized in the bounded arithmetic system VNC1 (corresponding to the “NC1 reasoning”). As a corollary, we prove the assumption made by Jeřábek [28] that a construction of certain bipartite expander graphs can be formalized in VNC1. This in turn implies that every proof in Gentzen's sequent calculus LK of a monotone sequent can be simulated in the monotone version of LK (MLK) with only polynomial blowup in proof size, strengthening the quasipolynomial simulation result of Atserias, Galesi, and Pudlák [9].

We introduce new stable natural merge sort algorithms, called 2-merge sort and α-merge sort. We prove upper and lower bounds for several merge sort algorithms, including Timsort, Shiver's sort, α-stack sorts, and our new 2-merge and α-merge sorts. The upper and lower bounds have the forms c · n log m and c · n log n for inputs of length n comprising m runs. For Timsort, we prove a lower bound of (1.5 – o(1))n log n. For 2-merge sort, we prove optimal upper and lower bounds of approximately (1.089 ± o(1))n log m. We state similar asymptotically matching upper and lower bounds for α-merge sort, when ϕ < α < 2, where ϕ is the golden ratio. Our bounds are in terms of merge cost; this upper bounds the number of comparisons and accurately models runtime. The merge strategies can be used for any stable merge sort, not just natural merge sorts. The new 2-merge and α-merge sorts have better worst-case merge cost upper bounds and are slightly simpler to implement than the widely-used Timsort; they also perform better in experiments.

Conflict-driven clause learning (CDCL) is at the core of the success of modern SAT solvers. In terms of propositional proof complexity, CDCL has been shown as strong as general resolution. Improvements to SAT solvers can be realized either by improving existing algorithms, or by exploiting proof systems stronger than CDCL. Recent work proposed an approach for solving SAT by reduction to Horn MaxSAT. The proposed reduction coupled with MaxSAT resolution represents a new proof system, DRMaxSAT, which was shown to enable polynomial time refutations of pigeonhole formulas, in contrast with either CDCL or general resolution. This paper investigates the DRMaxSAT proof system, and shows that DRMaxSAT p-simulates general resolution, that AC0-Frege+PHP p-simulates DRMaxSAT, and that DRMaxSAT can not p-simulate AC0-Frege+PHP or the cutting planes proof system.

We study consistency search problems for Frege and extended Frege proofs—namely the NP search problems of finding syntactic errors in Frege and extended Frege proofs of contradictions. The input is a polynomial time function, or an oracle, describing a proof of a contradiction; the output is the location of a syntactic error in the proof. The consistency search problems for Frege and extended Frege systems are shown to be many-one complete for the provably total NP search problems of the second-order bounded arithmetic theories U 1 2 and V 1 2 , respectively.

Abstract We extend results of Bonet, Buss and Pitassi on Bondy’s Theorem and of Nozaki, Arai and Arai on Bollobás’ Theorem by proving that Frankl’s Theorem on the trace of sets has quasipolynomial size Frege proofs. For constant values of the parameter t , we prove that Frankl’s Theorem has polynomial size AC 0 -Frege proofs from instances of the pigeonhole principle.

Abstract We introduce the safe recursive set functions based on a Bellantoni–Cook style subclass of the primitive recursive set functions. We show that the functions computed by safe recursive set functions under a list encoding of finite strings by hereditarily finite sets are exactly the polynomial growth rate functions computed by alternating exponential time Turing machines with polynomially many alternations. We also show that the functions computed by safe recursive set functions under a more efficient binary tree encoding of finite strings by hereditarily finite sets are exactly the quasipolynomial growth rate functions computed by alternating quasipolynomial time Turing machines with polylogarithmic many alternations. We characterize the safe recursive set functions on arbitrary sets in definability-theoretic terms. In its strongest form, we show that a function on arbitrary sets is safe recursive if and only if it is uniformly definable in some polynomial level of a refinement of Jensen's J-hierarchy, relativized to the transitive closure of the function's arguments. We observe that safe recursive set functions on infinite binary strings are equivalent to functions computed by infinite-time Turing machines in time less than ωω. We also give a machine model for safe recursive set functions which is based on set-indexed parallel processors and the natural bound on running times.

This paper studies the relationship between resolution and conflict driven clause learning (CDCL) without restarts, and refutes some conjectured possible separations. We prove that the guarded, xor-ified pebbling tautology clauses, which Urquhart proved are hard for regular resolution, as well as the guarded graph tautology clauses of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. For the latter set of clauses, we extend this to prove that a CDCL search without restarts can refute these clauses in polynomial time, provided it makes the right choices for decision literals and clause learning. This holds even if the CDCL search is required to greedily process conflicts arising from unit propagation. This refutes the conjecture that the guarded graph tautology clauses or the guarded xor-ified pebbling tautology clauses can be used to separate CDCL without restarts from general resolution. Together with subsequent results by Buss and Kolodziejczyk, this means we lack any good conjectures about how to establish the exact logical strength of conflict-driven clause learning without restarts.

Abstract We study the long-standing open problem of giving $\forall {\rm{\Sigma }}_1^b$ separations for fragments of bounded arithmetic in the relativized setting. Rather than considering the usual fragments defined by the amount of induction they allow, we study Jeřábek’s theories for approximate counting and their subtheories. We show that the $\forall {\rm{\Sigma }}_1^b$ Herbrandized ordering principle is unprovable in a fragment of bounded arithmetic that includes the injective weak pigeonhole principle for polynomial time functions, and also in a fragment that includes the surjective weak pigeonhole principle for FPNPfunctions. We further give new propositional translations, in terms of random resolution refutations, for the consequences of $T_2^1$ augmented with the surjective weak pigeonhole principle for polynomial time functions.

This article concerns the second-order systems U 1 2 and V 1 2 of bounded arithmetic, which have proof-theoretic strengths corresponding to polynomial-space and exponential-time computation. We formulate improved witnessing theorems for these two theories by using S 1 2 as a base theory for proving the correctness of the polynomial-space or exponential-time witnessing functions. We develop the theory of nondeterministic polynomial-space computation, including Savitch's theorem, in U 1 2 . Kołodziejczyk et al. [2011] have introduced local improvement properties to characterize the provably total NP functions of these second-order theories. We show that the strengths of their local improvement principles over U 1 2 and V 1 2 depend primarily on the topology of the underlying graph, not the number of rounds in the local improvement games. The theory U 1 2 proves the local improvement principle for linear graphs even without restricting to logarithmically many rounds. The local improvement principle for grid graphs with only logarithmically-many rounds is complete for the provably total NP search problems of V 1 2 . Related results are obtained for local improvement principles with one improvement round and for local improvement over rectangular grids.

Abstract We introduce martingales defined by probabilistic strategies, in which randomness is used to decide whether to bet. We show that different criteria for the success of computable probabilistic strategies can be used to characterize ML-randomness, computable randomness, and partial computable randomness. Our characterization of ML-randomness partially addresses a critique of Schnorr by formulating ML randomness in terms of a computable process rather than a computably enumerable function.

This paper characterizes alternation trading based proofs that the satisfiability problem is not in the time and space bounded class DTISP(nc, nϵ), for various values c <; 2 and ϵ <; 1. We characterize exactly what can be proved for ϵ ∈ o(1) with currently known methods, and prove the conjecture of Williams that the best known lower bound exponent c = 2 cos(π/7) is optimal for alternation trading proofs. For general time-space tradeoff lower bounds on satisfiability, we give a theoretical and computational analysis of the alternation trading proofs for 0 <; ϵ <; 1, again proving time lower bounds for various values of ϵ which are optimal for the alternation trading proof paradigm.

Abstract We present sharpened lower bounds on the size of cut free proofs for first-order logic. Prior lower bounds for eliminating cuts from a proof established superexponential lower bounds as a stack of exponentials, with the height of the stack proportional to the maximum depthdof the formulas in the original proof. Our results remove the constant of proportionality, giving an exponential stack of height equal tod−O(1). The proof method is based on more efficiently expressing the Gentzen–Solovay cut formulas as low depth formulas.

Abstract We give the first systematic study of strong isomorphism reductions, a notion of reduction more appropriate than polynomial time reduction when, for example, comparing the computational complexity of the isomorphim problem for different classes of structures. We show that the partial ordering of its degrees is quite rich. We analyze its relationship to a further type of reduction between classes of structures based on purely comparing for everynthe number of nonisomorphic structures of cardinality at mostnin both classes. Furthermore, in a more general setting we address the question of the existence of a maximal element in the partial ordering of the degrees.

We introduce new features for the broad phase algorithm sweep and prune that increase scalability for large virtual reality environments and allow for efficient AABB (axis-aligned bounding boxes) insertion and removal to support dynamic object creation and destruction. We introduce a novel segmented interval list structure that allows AABB insertion and removal without requiring a full sort of the axes. This algorithm is well-suited to large environments in which many objects are not moving at once. We analyze and test implementations of sweep and prune that include subdivision, batch insertion and removal, and segmented interval lists. Our tests show these techniques provide higher performance than previous sweep and prune methods, and perform better than octrees in temporally coherent environments.

Resolution refinements called w-resolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both WRTL and WRTI when there is no regularity condition. For regular proofs, an exponential separation between regular dag-like resolution and both regular WRTL and regular WRTI is given. It is proved that DLL proof search algorithms that use clause learning based on unit propagation can be polynomially simulated by regular WRTI. More generally, non-greedy DLL algorithms with learning by unit propagation are equivalent to regular WRTI. A general form of clause learning, called DLL-Learn, is defined that is equivalent to regular WRTL. A variable extension method is used to give simulations of resolution by regular WRTI, using a simplified form of proof trace extensions. DLL-Learn and non-greedy DLL algorithms with learning by unit propagation can use variable extensions to simulate general resolution without doing restarts. Finally, an exponential lower bound for WRTL where the lemmas are restricted to short clauses is shown.

We prove a new switching lemma that works for restrictions that set only a small fraction of the variables and is applicable to formulas in disjunctive normal form (DNFs) with small terms. We use this to prove lower bounds for the Res(k) propositional proof system, an extension of resolution which works with k-DNFs instead of clauses. We also obtain an exponential separation between depth d circuits of bottom fan-in k and depth d circuits of bottom fan-in k + 1. Our results for Res(k) are as follows:The 2n to n weak pigeonhole principle requires exponential size to refute in Res(k) for $k \leq \sqrt{\log n / \log \log n } $. For each constant k, there exists a constant w > k so that random w-CNFs require exponential size to refute in Res(k). For each constant k, there are sets of clauses which have polynomial size Res(k + 1) refutations but which require exponential size Res(k) refutations.

We prove a new switching lemma that works for restrictions that set only a small fraction of the variables and is applicable to DNFs with small conjunctions. We use this to prove lower bounds for the Res(k) propositional proof system, an extension of resolution which works with k-DNFs instead of clauses. We also obtain an exponential separation between depth d circuits of bottom fan-in k and depth d circuits of bottom fan-in k+1. Our results for Res(k) are: 1. The 2n to n weak pigeonhole principle requires exponential size to refute in Res(k), for k /spl les/ /spl radic/(log n/ log log n). 2. For each constant k, there exists a constant w > k so that random w-CNFs require exponential size to refute in Res(k). 3. For each constant k, there are sets of clauses which have polynomial size Res(k+1) refutations, but which require exponential size Res(k) refutations.

We define notions of resource-bounded continuity and sequentiality for type-two functionals with total inputs, and prove that in the resource-bounded model there are continuous functionals which cannot be efficiently simulated by sequential functionals. We also show that for some naturally defined classes of continuous functionals an efficient simulation is possible.

Abstract We prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within a factor of . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution. Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.

This article introduces a method for computing weighted averages on spheres based on least squares minimization that respects spherical distance. We prove existence and uniqueness properties of the weighted averages, and give fast iterative algorithms with linear and quadratic convergence rates. Our methods are appropriate to problems involving averages of spherical data in meteorological, geophysical, and astronomical applications. One simple application is a method for smooth averaging of quaternions, which generalizes Shoemake's spherical linear interpolation.The weighted averages methods allow a novel method of defining Bézier and spline curves on spheres, which provides direct generalization of Bézier and B-spline curves to spherical spline curves. We present a fast algorithm for spline interpolation on spheres. Our spherical splines allow the use of arbitrary knot positions; potential applications of spherical splines include smooth quaternion curves for applications in graphics, animation, robotics, and motion planning.

We define notions of resource-bounded continuity and sequentiality for type-two functionals with total inputs, and prove that in the resource-bounded model there are continuous functionals which cannot be efficiently simulated by sequential functionals. We also show that for some naturally defined classes of continuous functionals, an efficient simulation is possible.

Two important algebraic proof systems are the Nullstellensatz system and the polynomial calculus (also called the Grobner system). The Nullstellensatz system is a propositional proof system based on Hilbert's Nullstellensatz, and the polynomial calculus (PC) is a proof system which allows derivations of polynomials, over some field. The complexity of a proof in these systems is measured in terms of the degree of the polynomials used in the proof. The mod p counting principle can be formulated as a set MOD/sub p//sup n/ of constant-degree polynomials expressing the negation of the counting principle. The Tseitin mod p principles, TS/sub n/(p), are translations of the MOD/sub p//sup n/ into the Fourier basis. The present paper gives linear lower bounds on the degree of polynomial calculus refutations of MOD/sub p//sup n/ over p fields of characteristic q /spl ne/ p and over rings Z/sub q/ with q,p relatively prime. These are the first linear lower bounds for the polynomial calculus. As it is well-known to be easy to give constant degree polynomial calculus (and even Nullstellensatz) refutations of the MOD/sub p//sup n/ polynomials over F/sub p/, our results imply that the MOD/sub p//sup n/ polynomials have a linear gap between proof complexity for the polynomial calculus over F/sub p/ and over F/sub q/. We also obtain a linear gap for the polynomial calculus over rings Z/sub p/ and Z/sub q/ where p, q do not have identical prime factors.

This paper gives nearly optimal lower bounds on the minimum degree of polynomial calculus refutations of Tseitin's graph tautologies and the mod p counting principles, p >_ 2. The lower bounds apply to the polynomial calculus over fields or rings.These are the first linear lower bounds for polynomial calculus; moreover, they distinguish linearly between proofs over fields of characteristic p and T, y # r, and more generally distinguish linearly the rings Z, and Z, where 4 and P do not have the identical prime factors.

Let G be a complete, weighted, undirected, bipartite graph with n red nodes, n " blue nodes, and symmetric cost function c(x,y). A maximum matching for G consists of $\min\{n,n^\prime\}$ edges from distinct red nodes to distinct blue nodes. Our objective is to find a minimum-cost maximum matching, i.e., one for which the sum of the edge costs has minimal value. This is the weighted bipartite matching problem or, as it is sometimes called, the assignment problem. We report a new and very fast algorithm for an abstract special case of this problem. Our first requirement is that the nodes of the graph are given as a "quasi-convex tour." This means that they are provided circularly ordered as x 1 ,...,x N , where N = n + n " , and that for any $x_i, x_j, x_k, x_\ell$, not necessarily adjacent but in tour order, with x i , x j of one color and $x_k,x_\ell$ of the opposite color, the following inequality holds: \[ c(x_i,x_\ell) + c(x_j,x_k) \le c(x_i,x_k) + c(x_j,x_\ell). \] If $n = n^\prime$, our algorithm then finds a minimum-cost matching in $O(N \log N)$ time. Given an additional condition of ``weak analyticity," the time complexity is reduced to $O(N)$. In both cases only linear space is required. In the special case where the circular ordering is a line-like ordering, these results apply even if $n \ne n^\prime$. Our algorithm is conceptually elegant, straightforward to implement, and free of large hidden constants. As such we expect that it may be of practical value in several problem areas. Many natural graphs satisfy the quasi-convexity condition. These include graphs which lie on a line or circle with the canonical tour ordering, and costs given by any concave-down function of arclength --- or graphs whose nodes lie on an arbitrary convex planar figure with costs provided by Euclidean distance. The weak-analyticity condition applies to points lying on a circle with costs given by Euclidean distance, and we thus obtain the first linear-time algorithm for the minimum-cost matching problem in this setting (and also where costs are given by the $L_1$ or $L_\infty$ metrics). Given two symbol strings over the same alphabet, we may imagine one to be red and the other blue and use our algorithms to compute string distances. In this formulation, the strings are embedded in the real line and multiple independent assignment problems are solved, one for each distinct alphabet symbol. While these examples are somewhat geometrical, it is important to remember that our conditions are purely abstract; hence, our algorithms may find application to problems in which no direct connection to geometry is evident.

This paper gives nearly optimal, logarithmic upper and lower bounds on the minimum degree of Nullstellensatz refutations (i.e., polynomials) of the propositional induction principle.

The serial transitive closure problem is the problem, given a directed graph G and a list of edges, called closure edges, which are in the transitive closure of the graph, to generate all the closure edges from edges in G. A nearly linear upper bound is given on the number of steps in optimal solutions to the serial transitive closure problem for the case of graphs that are trees. “Nearly linear” means $O(n \cdot \alpha (n))$, where $\alpha $ is the inverse Ackermann function. This upper bound is optimal to within a constant factor.

Abstract This paper discusses lower bounds for proof length, especially as measured by number of steps (inferences). We give the first publicly known proof of Gödel's claim that there is superrecursive (in fact, unbounded) proof speedup of (i + l)st-order arithmetic over ith-order arithmetic, where arithmetic is formalized in Hilbert-style calculi with + and • as function symbols or with the language of PRA. The same results are established for any weakly schematic formalization of higher-order logic: this allows all tautologies as axioms and allows all generalizations of axioms as axioms. Our first proof of Gödel's claim is based on self-referential sentences: we give a second proof that avoids the use of self-reference based loosely on a method of Statman.

Abstract We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems , and nested deduction Frege systems , which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines (or formulas) in the proof. A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by “nearly linear” is meant the ratio of proof lengths is O (α( n )) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O ( n . α( n )). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O ( n log n ) lines and of height O (log n ). As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O ( n log n ).

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.

Proof systems for propositional logic called simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule, are introduced. Upper bounds are given on the lengths of proofs in these systems compared to lengths in Frege proof systems. As an application, a near-linear simulation of the propositional Gentzen sequent calculus by Frege proofs is presented. It is shown that a general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege systems where by 'nearly linear' is meant that the ratio of proof lengths is O( alpha (n)), where alpha is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, and hence a Frege proof system can simulate the propositional sequent calculus with proof lengths bounded by O(n alpha (n)). As a technical tool, the serial transitive closure problem is introduced. Given a directed graph and a list of closure edges in the transitive closure of the graph, the problem is to derive all the closure edges. A nearly linear bound is given on the number of steps in such a derivation when the graph is treelike.>

The authors show a sharp dichotomy between systems of identical automata with symmetric global control whose behavior is easy to predict and those whose behavior is hard to predict. The division pertains to whether the global control rule is invariant with respect to permutations of the states of the automaton. It is also shown that testing whether the global control rule has this invariance property is an undecidable problem. It is argued that there is a natural analog between complexity in the present model and chaos in dynamical systems.>

The Boolean formula value problem is in alternating log time and, more generally, parenthesis context-free languages are in alternating log time. The evaluation of reverse Polish notation Boolean formulas is also in alternating log time. These results are optimal since the Boolean formula value problem is complete for alternating log time under deterministic log time reductions. Consequently, it is also complete for alternating log time under AC reductions.

Abstract Cook and Reckhow defined a propositional formulation of the pigeonhole principle. This paper shows that there are Frege proofs of this propositional pigeonhole principle of polynomial size. This together with a result of Haken gives another proof of Urquhart's theorem that Frege systems have an exponential speedup over resolution. We also discuss connections to provability in theories of bounded arithmetic.

Article Free Access Share on The polynomial hierarchy and fragments of bounded arithmetic Author: S R Buss Department of Mathematics, Princeton University Department of Mathematics, Princeton UniversityView Profile Authors Info & Claims STOC '85: Proceedings of the seventeenth annual ACM symposium on Theory of computingDecember 1985 Pages 285–290https://doi.org/10.1145/22145.22177Online:01 December 1985Publication History 4citation219DownloadsMetricsTotal Citations4Total Downloads219Last 12 Months6Last 6 weeks1 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