Research interests

• applied logic, logic engineering, automating logic,
• logical formalisations and proof methods for agent-based systems,
• automated reasoning,
• model generation,
• second-order quantifier elimination,
• resolution-based proof techniques, resolution decision procedures,
• most other styles of proof systems: tableau, sequent calculus, natural deduction, inverse method, Rasiowa-Sikorski proof systems, ...
• relationships between proof systems, relative complexity of proof systems, simulating proof procedures
• implementing theorem provers and other logical tools,
• empirical evaluation,
• translating logics into first-order logic,
• decidable fragments of first-order logic, solvable clausal classes,
• modal logics, PDL-like modal logics, dynamic logic, temporal logic
• description logics, knowledge representation,
• Tarski's relational calculus and relation algebra,
• Boolean modules, Peirce algebra.