Die meisten Forschungsarbeiten in unserer Gruppe beschäftigen sich mit der automatisierten Deduktion, d.h. mit dem Problem, wie man die Erzeugung logischer Schlussfolgerungen automatisieren kann. In diesem Zusammenhang interessieren wir uns vor allem für Unterklassen der Prädikatenlogik erster Ordnung, für die die interessanten Inferenzprobleme noch entscheidbar sind. Auf der einen Seite untersuchen wir die Kombination spezieller Deduktionsmethoden und deren Integration in allgemeine Deduktionsverfahren. Auf der anderen Seite entwerfen wir logikbasierte Wissensrepräsentationssprachen mit entscheidbaren Inferenzproblemen.