My research is focused on automating logical reasoning. More specifically, tableau- and connection-based proof search calculi for classical and non-classical logics. I have developed the leanCoP series of automated theorem provers, extremely compact yet efficient provers for classical and several non-classical logics. More recently I have developed nanoCoP, an efficient connection-based theorem prover.
I am adapting these theorem provers to use them to develop and access data in ontology-based databases.
Scientific interests: Automated theorem proving, logic, ontology-based data access
What triggers me scientifically: My objective is to integrate theorem-proving technology into industrial applications. More specifically, I like to develop and deploy the most elegant and efficient theorem provers to automate and optimize ontology-based data access.