| |

:: Home:: What is EACSL:: Organization:: Membership:: CSL Conferences:: Ackermann Award:: Alonzo Church Award:: CSL Bibliography:: Constitutions:: Minutes:: Contact |
## Ackermann Award 2005: Nathan Segerlind## CitationNathan Segerlind recieves the 2005 Ackermann Award of the European Association of Computer Science Logic (EACSL) for his thesis## New Separations in Propositional Proof Complexity.Res(k) from an
almost complete mystery to being almost completely understood.
## Background of the thesisThe central question of propositional proof complexity can be formulated in a deceivingly simple way. Given a (sound and complete) proof systemP
for propositional logic and a tautology φ, what is the ``simplest''
(in most cases meaning the shortest) P-proof of φ? Partly due to
the universal nature of the notion of a propositional tautology, this is
an interdisciplinary area on the border between (and with motivations
from) mathematical logic, theory of computing, automated theorem proving,
cryptography, algebra and combinatorics among other.
Largely influenced by the automated theorem proving (Davis, Putnam (1960), Davis, Longemann, Loveland (1962), Robinson (1965)), the most widely studied proof system in the area is (propositional) Resolution. After considerable efforts by many researchers beginning with the seminal paper by Tseitin (1968), the resolution proof system is by now fairly well understood. We have rather general, industrial methods to analyze the complexity of resolution proofs (like the width-size relation by Ben-Sasson, Wigderson (1999)), as well as concrete results concerning virtually all combinatorial principles normally used as ``benchmarks'' in the whole area (Haken (1985), Urquhart (1987), Chvátal, Szemerédi (1988), Raz (2001), Razborov (2001)).
Until the work represented by Segerlind's thesis, however, everything
looked very different (meaning much more obscure) beyond Resolution. As a
typical example, take one of the most influential results in the whole
area, exponential lower bounds on the complexity of the
Just to give an idea of the state of the art in the area,
Another important subject addressed in the thesis is ## Segerlind's thesisIn his thesis Segerlind proved important and nice results about the relative power of algebraic and mixed proof systems, both positive and negative, that had been open for a while. Among other things he showed that counting gates are more powerful than counting axioms (Chapter VI), but the counting axioms can efficiently simulate any Nullstellensatz proof (Chapter V). The most striking part of the thesis, however, concerns the systemsRes(k)
for small values of k (Chapters III and IV).
The upshot of these latter results is very simple: we now understand the
systems The first is its speed. For Resolution it took decades to have reached the level of understanding that was reached here in a single step. Of course, this comparison is not quite fair since the general methodology gathered during these decades also played very essential role in Segerlind's work. But even with this disclaimer the speed with which it all happened was quite remarkable and totally unexpected.
The second surprise came in the form of proof methods. The novelty
essentially consists in a new version of switching lemmas called in the
thesis ## Biographic SketchNathan Segerlind was born on December 31, 1973 in Marlette, Michigan. In 1992-1998 he studied Computer Science and Mathematics at Carnegie Mellon University, Pittsburg. Between 1998 and 2003 he was a PhD student at the University of California at San Diego, under joint supervision by Samuel Bass and Russell Impagliazzo. He spent the next year 2003-2004 as a postdoctoral member at the Institute for Advanced Study, Princeton. Currently he is continuing his post-doc research at the University of Washington, Seattle. |