Technische Universität München, Fakultät für Informatik
Lehrstuhl Informatik IV

Stephan Schulz, Dr. rer.nat., Dipl. Inform.

Room:           00.09.061
Telephone:      +49 - 89 - 289 - 17880
FAX:            +49 - 89 - 289 - 17307
GPG public key: Click here
Snail:	        TU München
                Institut für Informatik
                Boltzmannstr. 3
		85748 Garching b. München
     So-so picture of Stephan Schulz

I studied computer science in Kaiserslautern and obtained my diploma from the Universität Kaiserslautern in spring 1995. My main focus of interest has been the analysis of equational proofs and proof systems, and the improvement of their performance using various means. Check out the TEAMWORK page to find out more about the DISCOUNT prover used in these projects.

I joined the Research Group Automated Reasoning in March 1995 to work on the integration of symbolic and connectionist systems in the ESPRIT BRA 9119 MIX. After the successful conclusion of MIX in 1997 I started working on a DFG-funded project on the integration of special techniques for the handling of equality into the theorem prover SETHEO to create E-SETHEO. My major contribution is the equational theorem prover E, one of the most powerful (and friendly) monolithic automated theorem provers currently available. E can be used both as a stand-alone prover and as a component in E-SETHEO. E is under active development and still forms the core platform for my research.

In early 2000, I obtained a Ph.D. in computer science from the Technische Universität München for my thesis Learning Search Control Knowledge for Equational Deduction.

I spent the fall semester 2002 teaching two classes at the University of Miami. For more see my home page there. After briefly returning to Munich, I went to visit first RISC Linz, then the Mathematical Reasoning Group at the University of Edinburgh and finally ITC/irst in Trento, all on a CALCULEMUS grant sponsored by the European Union. In 2004/2005 I spend some some time at the University of Verona before returning to Trento.

One of my more exciting jobs was a summer position as a visiting lecturer at the Mona Institute of Applied Sciences in Kingston, Jamaica, in 2005. There is a course web page for the class I taught.

I'm currently associated with TU Munich as a guest researcher.

I've been elected to a position on the FTP steering committee in November 2003. You can read my candidate statement.

Here is an example of recursion and here an example of well-founded recursion. Yes, this is hacker humor. Perhaps my private page (which is not very private anyways) is more interesting for normal people. It will also explain why this page was black and what the blue ribbon below signifies. I also have a partial bibliography of my scientific work online.
Blue Ribbon    "The problem is not that the world is full of fools. The problem is that lightning isn't being distributed right."     

-Mark Twain

Stephan Schulz,, Mon May 1 11:17:32 CEST 2006