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\'atal, Szemer\'edi (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 {\em pigeon-hole principle} in the {\em constant-depth Frege proof system} (Beame, Impagliazzo, Kraj\'i\v cek, Pitassi, Pudl\'ak, Woods (1992)) based on one of the most powerful tools in the area, {\em switching lemmas for random restrictions}. We do not know how to apply this method to many tautologies where it should have been applicable, and even when successful (like e.g. Beame, Riis (1998)), the switching lemmas and other techniques, already extremely complicated, have to be re-done almost from the scratch. The situation is very similar for the intermediate proof system $Res(k)$ that operates like Resolution but allows in clauses conjunctions of size $\leq k$ rather than just literals. This system is of great potential interest for automated proving (perhaps, of better interest than constant-depth Frege) since it is structured almost as well as Resolution but surprisingly can do more interesting things than the latter (Maciel, Pitassi, Woods (2000)).
Just to give an idea of the state of the art in the area, {\em random 3-CNF} is one of the most popular benchmark models both in theoretical and practical communities. They had been shown to be hard for Resolution by Chv\'atal and Szemer\'edi in 1988, but the same question was widely open for {\em any} reasonable extension of Resolution, including $Res(2)$.
Another important subject addressed in the thesis is {\em algebraic proof systems} (like Nullstellensatz and Polynomial Calculus) and hybrid systems combining logical and algebraic reasoning (constant-depth Frege with counting axioms or modular gates). By the time of Segerlind's work, purely algebraic proof systems and relations between them were in general understood much better than purely logical systems, but several important questions remained open.
The upshot of these latter results is very simple: we now understand the systems $Res(k)$ almost as well as Resolution itself. In his thesis Segerlind analyzed the complexity of the weak pigeon-hole principle and random $w$-CNFs (both are standard ``tests for maturity'') in these proof systems, and he also gave separation results between the systems $Res(k)$ and $Res(w)$ for some $w>k$. His techniques were already used in different situations by Razborov and Alekhnovich. So, it really looks like what he has found is a general, powerful and flexible method rather than ad hoc argument. All in all, Segerlind's work changed the situation with these prominent systems from a few scattered and weak results to a few important problems left open. And two features of this development look particularly striking.
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 {\em switching with small restrictions}. And, in order to appreciate this, one should be fully aware to {\em which} extent this tool is basic in both computational complexity and proof complexity. Many researchers have been looking at these lemmas since the seminal work by H\aa stad (1986). They have been scrutinized and analyzed from every possible perspective and in all fine and technical details. The fact that Segerlind was able to say a substantially new word in an area so often re-visited by strongest researchers is also quite remarkable.