Advancement of automated deduction, in particular first-order logic theorem proving. Design of calculi (in particular the Model Evolution calculus), implementations (in particular the E-Darwin system) and their application for software verification, knowledge representation, and business rules analysis; exploiting connections into related areas such as logic programming, description logics and nonmonotonic reasoning.