Researcher (wissenschaftlicher Mitarbeiter), Dr. rer. nat.,
Programming Systems Lab,
Saarland University.
My research interests include completeness, decidability and automation of reasoning for modal, temporal and description logics. I am particularly interested in the design and implementation of efficient decision procedures for expressive modal logics, as well as in applying decision procedures to problems in ontological reasoning, hardware and software verification. My past studies include some work on the semantic expressiveness and deductive completeness of higher-order logic and its fragments.
Together with my students, I developed Spartacus and InKreSAT, two efficient theorem provers for modal logic.