9 Search Results for "Cook, Stephen"

Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2020.5
From Classical Proof Theory to P versus NP: a Guide to Bounded Theories (Invited Talk)

Authors: Iddo Tzameret

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
This talk explores the question of what does logic and specifically proof theory can tell us about the fundamental hardness questions in computational complexity. We start with a brief description of the main concepts behind bounded arithmetic which is a family of weak formal theories of arithmetic that mirror in a precise manner the world of propositional proofs: if a statement of a given form is provable in a given bounded arithmetic theory then the same statement is suitably translated to a family of propositional formulas with short (polynomial-size) proofs in a corresponding propositional proof system. We will proceed to describe the motivations behind the study of bounded arithmetic theories, their corresponding propositional proof systems, and how they relate to the fundamental complexity class separations and circuit lower bounds questions in computational complexity. We provide a collage of results and recent developments showing how bounded arithmetic and propositional proof complexity form a cohesive framework in which both concrete combinatorial questions about complexity as well as meta-mathematical questions about provability of statements of complexity theory itself, are studied. Specific topics we shall mention are: (i) The bounded reverse mathematics program [Stephen Cook and Phuong Nguyen, 2010]: studying the weakest possible axiomatic assumptions that can prove important results in mathematics and computing (cf. [Iddo Tzameret and Stephen A. Cook, 2017; Pavel Hrubeš and Iddo Tzameret, 2015]), and the correspondence between circuit classes and theories. (ii) The meta-mathematics of computational complexity: what kind of reasoning power do we need in order to prove major results in complexity theory itself, and applications to complexity lower bounds (cf. [Razborov, 1995; Rahul Santhanam and Jan Pich, 2019]). (iii) Proof complexity: the systematic treatment of propositional proofs as combinatorial and algebraic objects and their algorithmic applications (cf. [Samuel Buss, 2012; Tonnian Pitassi and Iddo Tzameret, 2016; Noah Fleming et al., 2019]).
Cite as

Iddo Tzameret. From Classical Proof Theory to P versus NP: a Guide to Bounded Theories (Invited Talk). In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{tzameret:LIPIcs.CSL.2020.5,
  author =	{Tzameret, Iddo},
  title =	{{From Classical Proof Theory to P versus NP: a Guide to Bounded Theories}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{5:1--5:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.5},
  URN =		{urn:nbn:de:0030-drops-116482},
  doi =		{10.4230/LIPIcs.CSL.2020.5},
  annote =	{Keywords: Bounded arithmetic, complexity class separations, circuit complexity, proof complexity, weak theories of arithmetic, feasible mathematics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.18
A Recursion-Theoretic Characterisation of the Positive Polynomial-Time Functions

Authors: Anupam Das and Isabel Oitavem

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We extend work of Lautemann, Schwentick and Stewart [Clemens Lautemann et al., 1996] on characterisations of the "positive" polynomial-time predicates (posP, also called mP by Grigni and Sipser [Grigni and Sipser, 1992]) to function classes. Our main result is the obtention of a function algebra for the positive polynomial-time functions (posFP) by imposing a simple uniformity constraint on the bounded recursion operator in Cobham's characterisation of FP. We show that a similar constraint on a function algebra based on safe recursion, in the style of Bellantoni and Cook [Stephen Bellantoni and Stephen A. Cook, 1992], yields an "implicit" characterisation of posFP, mentioning neither explicit bounds nor explicit monotonicity constraints.
Cite as

Anupam Das and Isabel Oitavem. A Recursion-Theoretic Characterisation of the Positive Polynomial-Time Functions. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.CSL.2018.18,
  author =	{Das, Anupam and Oitavem, Isabel},
  title =	{{A Recursion-Theoretic Characterisation of the Positive Polynomial-Time Functions}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.18},
  URN =		{urn:nbn:de:0030-drops-96851},
  doi =		{10.4230/LIPIcs.CSL.2018.18},
  annote =	{Keywords: Monotone complexity, Positive complexity, Function classes, Function algebras, Recursion-theoretic characterisations, Implicit complexity, Logic}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.36
Lower Bounds for Nondeterministic Semantic Read-Once Branching Programs

Authors: Stephen Cook, Jeff Edmonds, Venkatesh Medabalimi, and Toniann Pitassi

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
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}.
Cite as

Stephen Cook, Jeff Edmonds, Venkatesh Medabalimi, and Toniann Pitassi. Lower Bounds for Nondeterministic Semantic Read-Once Branching Programs. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 36:1-36:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{cook_et_al:LIPIcs.ICALP.2016.36,
  author =	{Cook, Stephen and Edmonds, Jeff and Medabalimi, Venkatesh and Pitassi, Toniann},
  title =	{{Lower Bounds for Nondeterministic Semantic Read-Once Branching Programs}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{36:1--36:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.36},
  URN =		{urn:nbn:de:0030-drops-63166},
  doi =		{10.4230/LIPIcs.ICALP.2016.36},
  annote =	{Keywords: Branching Programs, Semantic, Non-deterministic, Lower Bounds}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.296
Theories for Subexponential-size Bounded-depth Frege Proofs

Authors: Kaveh Ghasemloo and Stephen A. Cook

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
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.
Cite as

Kaveh Ghasemloo and Stephen A. Cook. Theories for Subexponential-size Bounded-depth Frege Proofs. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 296-315, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{ghasemloo_et_al:LIPIcs.CSL.2013.296,
  author =	{Ghasemloo, Kaveh and Cook, Stephen A.},
  title =	{{Theories for Subexponential-size Bounded-depth Frege Proofs}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{296--315},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.296},
  URN =		{urn:nbn:de:0030-drops-42044},
  doi =		{10.4230/LIPIcs.CSL.2013.296},
  annote =	{Keywords: Computational Complexity Theory, Proof Complexity, Bounded Arithmetic, NC1-Frege, AC0- Frege}
}
Document
DOI: 10.4230/LIPIcs.STACS.2013.622
Pebbling, Entropy and Branching Program Size Lower Bounds

Authors: Balagopal Komarath and Jayalal M. N. Sarma

Published in: LIPIcs, Volume 20, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)

Abstract
We contribute to the program of proving lower bounds on the size of branching programs solving the Tree Evaluation Problem introduced in (Stephen A. Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, and Rahul Santhanam, 2012). Proving an exponential lower bound for the size of the non-deterministic thrifty branching programs would separate NL from P under the thrifty hypothesis. In this context, we consider a restriction of non-deterministic thrifty branching programs called bitwise-independence. We show that any bitwise-independent non-deterministic thrifty branching program solving BT_2(h,k) must have at least 1/2 k^{h/2} states. Prior to this work, lower bounds were known for general branching programs only for fixed heights h=2,3,4 (Stephen A. Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, and Rahul Santhanam, 2012). Our lower bounds are also tight (up to a factor of k), since the known (Stephen A. Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, and Rahul Santhanam, 2012) non-deterministic thrifty branching programs for this problem of size O(k^{h/2+1}) are bitwise-independent. We prove our results by associating a fractional pebbling strategy with any bitwise-independent non-deterministic thrifty branching program solving the Tree Evaluation Problem. Such a connection was not known previously even for fixed heights. Our main technique is the entropy method introduced by Jukna and Zak (S. Jukna and S. Žák, 2003) originally in the context of proving lower bounds for read-once branching programs. We also show that the previous lower bounds known (Stephen A. Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, and Rahul Santhanam, 2012) for deterministic branching programs for Tree Evaluation Problem can be obtained using this approach. Using this method, we also show tight lower bounds for any k-way deterministic branching program solving Tree Evaluation Problem when the instances are restricted to have the same group operation in all internal nodes.
Cite as

Balagopal Komarath and Jayalal M. N. Sarma. Pebbling, Entropy and Branching Program Size Lower Bounds. In 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 20, pp. 622-633, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{komarath_et_al:LIPIcs.STACS.2013.622,
  author =	{Komarath, Balagopal and Sarma, Jayalal M. N.},
  title =	{{Pebbling, Entropy and Branching Program Size Lower Bounds}},
  booktitle =	{30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)},
  pages =	{622--633},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-50-7},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{20},
  editor =	{Portier, Natacha and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2013.622},
  URN =		{urn:nbn:de:0030-drops-39709},
  doi =		{10.4230/LIPIcs.STACS.2013.622},
  annote =	{Keywords: Pebbling, Entropy Method, Branching Programs, Size Lower Bounds.}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2012.9
Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (Invited Talk)

Authors: Stephen A. Cook

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
This is a survey talk explaining the connection between the three items mentioned in the title.
Cite as

Stephen A. Cook. Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (Invited Talk). In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 9-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{cook:LIPIcs.CSL.2012.9,
  author =	{Cook, Stephen A.},
  title =	{{Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{9--11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.9},
  URN =		{urn:nbn:de:0030-drops-36594},
  doi =		{10.4230/LIPIcs.CSL.2012.9},
  annote =	{Keywords: Complexity Classes, Weak Formal Theories, Propositional Proof Systems}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2012.12
Satisfiability: where Theory meets Practice (Invited Talk)

Authors: Inês Lynce

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Propositional Satisfiability (SAT) is a keystone in the history of computer science. SAT was the first problem shown to be NP-complete in 1971 by Stephen Cook. Having passed more than 40 years from then, SAT is now a lively research field where theory and practice have a natural intermixing. In this talk, we overview the use of SAT in practical domains, where SAT is thought in a broad sense, i.e. including SAT extensions such as Maximum Satisfiability (MaxSAT), Pseudo-Boolean Optimization (PBO) and Quantified Boolean Formulas (QBF).
Cite as

Inês Lynce. Satisfiability: where Theory meets Practice (Invited Talk). In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 12-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{lynce:LIPIcs.CSL.2012.12,
  author =	{Lynce, In\^{e}s},
  title =	{{Satisfiability: where Theory meets Practice}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{12--13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.12},
  URN =		{urn:nbn:de:0030-drops-36600},
  doi =		{10.4230/LIPIcs.CSL.2012.12},
  annote =	{Keywords: Propositional Satisfiability, SAT solvers, Applications}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.381
A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem

Authors: Dai Tri Man Lê, Stephen A. Cook, and Yuli Ye

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem. He proved that several other problems are complete for CC, including the stable marriage problem, and finding the lexicographical first maximal matching in a bipartite graph. We suggest alternative definitions of CC based on different reducibilities and introduce a two-sorted theory VCC* based on one of them. We sharpen and simplify Subramanian's completeness proofs for the above two problems and formalize them in VCC*.
Cite as

Dai Tri Man Lê, Stephen A. Cook, and Yuli Ye. A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 381-395, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{le_et_al:LIPIcs.CSL.2011.381,
  author =	{L\^{e}, Dai Tri Man and Cook, Stephen A. and Ye, Yuli},
  title =	{{A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{381--395},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.381},
  URN =		{urn:nbn:de:0030-drops-32440},
  doi =		{10.4230/LIPIcs.CSL.2011.381},
  annote =	{Keywords: bounded arithmetic, complexity theory, comparator circuits}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2311
Fractional Pebbling and Thrifty Branching Programs

Authors: Mark Braverman, Stephen Cook, Pierre McKenzie, Rahul Santhanam, and Dustin Wehr

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

Abstract
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.
Cite as

Mark Braverman, Stephen Cook, Pierre McKenzie, Rahul Santhanam, and Dustin Wehr. Fractional Pebbling and Thrifty Branching Programs. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 109-120, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{braverman_et_al:LIPIcs.FSTTCS.2009.2311,
  author =	{Braverman, Mark and Cook, Stephen and McKenzie, Pierre and Santhanam, Rahul and Wehr, Dustin},
  title =	{{Fractional Pebbling and Thrifty Branching Programs}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{109--120},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2311},
  URN =		{urn:nbn:de:0030-drops-23111},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2311},
  annote =	{Keywords: Branching programs, space complexity, tree evaluation, pebbling}
}
  • Refine by Author
  • 3 Cook, Stephen A.
  • 2 Cook, Stephen
  • 1 Braverman, Mark
  • 1 Das, Anupam
  • 1 Edmonds, Jeff
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Algebraic complexity theory
  • 1 Theory of computation → Circuit complexity
  • 1 Theory of computation → Complexity theory and logic
  • 1 Theory of computation → Proof complexity
  • 1 Theory of computation → Proof theory
  • Show More...

  • Refine by Keyword
  • 2 Branching Programs
  • 1 AC0- Frege
  • 1 Applications
  • 1 Bounded Arithmetic
  • 1 Bounded arithmetic
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 2 2012
  • 2 2013
  • 1 2009
  • 1 2011
  • 1 2016
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact