I am a researcher focussing on theoretical computer science, knowledge representation, description logics and ontologies. My main areas of interest are temporal and probabilistic extensions of description logics, non-standard reasoning tasks such as forgetting and abduction, and explainability of description logic reasoning. I am currently involved in the DFG collaborative research center CPEC on perspicous software systems, and was formerly working within HAEC on situation recognition with probabilistic and temporal description logic reasoning.

I did my PhD at the University of Manchester, where I developed practical methods for uniform interpolation and forgetting in expressive description logics. As part of my research, I developed the tool LETHE, which can be used to compute uniform interpolants of ontologies, as well as to compute logical differences between ontology versions. After I finished my PhD, I worked as a researcher at the University of Oxford, before I then moved to Dresden.

You can find my publications at Google Scholar and DBLP.

Tools

CAPI - Connection-minimal Abduction using Prime Implicates

Performs TBox abduction for EL ontologies, which can be used to repair and explain missing entailments.

UPDATE 2022-12-13: new version 0.2 with additional post-processing.

Website

EVEE - Evincing Expressive DL Entailments

Although logic-based ontology languages offer the inherent possibility of explaining the process of deriving implicit knowledge, explaining complex Description Logic (DL) entailments to users is still a challenging task. So far, the ontology editor Protégé supports only (black-box) justifications and (glass-box) proofs for lightweight OWL 2 EL ontologies via the proof facilities of the reasoner Elk. Evee is a library for computing proofs that includes proof generation algorithms for DLs up to ALCH. It includes a recently developed technique for computing black-box elimination proofs as well as a glass-box technique based on the resolution calculus of Lethe, a tool for computing uniform interpolants. Additionally, it provides methods to optimize proofs that are generated via other methods according to various measures of proof quality. The Evee library is used by two frontends: a collection of Protégé plugins of the same name and the standalone tool Evonne, which supports more varied ways of displaying and interacting with proofs.

Github-Page

ELK Certifier

Certify ELK classification results so that they can be verified with the LFSC proof-checker.

Website
Paper

LETHE-Abduction

An extension of LETHE for performing signature-based abduction for ALC knowledge bases. To be used as library for Java.

Website
Paper

LETHE

Uniform interpolation and forgetting for expressive description logics. (Supports SH knowledge bases, and with restrictions SHQ TBoxes.) Comes with a graphical front-end, but can also be used from the command line or as java library.

Website
Paper

lat-scala-dl-tools

Collection of classes and objects to make work with OWL under Scala and Java more convenient.

Github-Page

forgetting-based-proof-generation

Generating step-wise explanations or proofs of concept inclusions using a forgetting tool such as LETHE or FAME.

Source code
Paper (XLoKR'20)
Paper (LPAR'20)
XLoKR talk (Youtube)

News