My research areas are (i) the implementation of
automatic reasoning
and (ii) applications of automated reasoning.
In the recent past, my research was mostly focused on development of
efficient implementation
techniques for saturation-based reasoning, such as
term indexing
[1, 2, 3] ,
efficient organisation of search [4, 5] and
run-time algorithm specialisation
([6, 7]).
As an experimental part of this research, I developed (together with Prof. Andrei Voronkov)
the resolution- and paramodulation-based kernel of the theorem
prover Vampire. The system has won the "world cup for theorem
provers" CASC in
the most prestigious CNF (MIX) division for nine years (1999, 2001-2008). A
complete account of this work can be found in my PhD
thesis.
Currently, I also have a strong interest in adapting classical reasoning
techniques for the purposes of semantic technologies in general, and
Semantic Web
in particular. More specifically, I am interested in Web-scale
semantic search and query answering over large databases modulo
very expressive knowledge bases. Also, as part of my current work in North Side Inc,
I have been developing practical methods for commonsense reasoning
in natural
language processing applications.
