Logic-Based Knowledge
Representation. In particular, expressing knowledge processing
operations in semantically founded and integrable ways by variants of
second-order quantifier elimination. Automated Theorem Proving in
First-Order Logic, along with generalizations such as Craig
interpolation and second-order quantifier elimination. Practical
applications of knowledge-based techniques.