Lower bounds for natural proof systems
Published 1 September 1977
Dexter Kozen
Citations439
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A lower space bound of n/log(n) is shown for the proof system for the PTIME complete theory and a lower length bound of 2cn/log('n'): length of polynomial space for the PSPACE complete theory.
Abstract
Two decidable logical theories are presented, one complete for deterministic polynomial time, one complete for polynomial space. Both have natural proof systems. A lower space bound of n/log(n) is shown for the proof system for the PTIME complete theory and a lower length bound of 2cn/log(n) is shown for the proof system for the PSPACE complete theory.
Keywords
Computer Science
The Design and Analysis of Computer Algorithms
9,456 Citations1974Alfred V. Aho, John E. Hopcroft
This text introduces the basic data structures and programming techniques often used in efficient algorithms, and covers use of lists, push-down stacks, queues, trees, and graphs.
Journal of Computer and System SciencesRelationships between nondeterministic and deterministic tape complexities
1,362 Citations1970Walter J. Savitch
The amount of storage needed to simulate a nondeterministic tape bounded Turingmachine on a deterministic Turing machine is investigated and a specific set is produced, namely the set of all codings of threadable mazes, such that, if there is any set which distinguishes nondeter microscopic complexity classes from deterministic tape complexity classes, then this is one such set.
ACM SIGACT NewsThe circuit value problem is log space complete for <i>P</i>
305 Citations1975Richard E. Ladner
The set P is the set of problems computable in polynomial_ time and the circuit value problem is CV, which is well known that a T(n) time bounded Turing machine can be simulate on n bits by a combinational circuit with 0(T-(n) gates.
Complexity of finitely presented algebras
158 Citations1977Dexter Kozen
The schema satisfiability problem and schema validity problem are shown to be ≤m m log-complete for NP and co-NP, respectively, and the problem of isomorphism of finitely presented algebras is shown to to be polynomial time many-one equivalent to the issue of graph isomorphicism.
Exponential space complete problems for Petri nets and commutative semigroups (Preliminary Report)
120 Citations1976E. Cardoza, Richard Lipton +1 more
The uniform word problem for commutative semigroups (UWCS) is the problem of determining from any given finite set of defining relations and any pair of words, whether the words describe the same element in the commUTative semigroup defined by the relations.
Space bounds for a game on graphs
51 Citations1976Wolfgang J. Paul, Robert E. Tarjan +1 more
It is shown that for each graph with n vertices and maximum in-degree d, there is a pebbling strategy which requires at most c(d) n/log n pebbles, and this bound is tight to within a constant factor.
eCommons (Cornell University)The complexity of resolution procedures for theorem proving in the propositional calculus.
11 Citations1975Zvi Galil
A comparative study on the complexity of various procedures for proving that a set of clauses is contradictory is described, finding exponential lower bounds for the run-time of most of the procedures and implications to the comlexity of integer programming routines.