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


Most of my work deals with theorem proving - especially with the DISCOUNT system developed at the Efficient Algorithms Group at the University of Kaiserslautern and my own equational theorem prover E, which started as part of the E-SETHEO project sponored by the DFG under the grant Je112/9-1, but has evolved over the next 12 years.

I am particularly interested in finding out more about good proof heuristics, and I work towards the automatic acquistion of search control knowledge for deductive systems. Thus, much of my research has to do with (deductive) reasoning and with (inductive) machine learning. Another aspect of my work is the efficient implementation of reasoning mechanisms.

Publications are listed in chronological order, but the list is probably somewhat incomplete. I'm working on it.

Authored Publications

Edited Proceedings


I only make presentations availabe for major talks, and only if there is no associated paper. If you want any of my other presentations, feel free to ask (but I suggest you read the paper instead). Older presentations are prepared using pdflatex and some modified style files originally borrowed from Matt Welsh, newer ones use a Frankenstein mixture of LaTeX Beamer and Apple's Keynote.

Stephan Schulz, 25.1.2001