Most of the research done in our group is concerned with automated deduction, that is, with the problem of how to automate the process of drawing logical inferences. In this context, we are mainly interested in subclasses of first-order predicate logic for which the interesting inference problems are still decidable. On one hand, we are investigating the combination of special deduction methods, and their integration into general deduction procedures. On the other hand, we are designing logic-based knowledge representation languages with decidable inference problems.