Logical reasoning is one of the key characteristics of
intelligent behaviour of (most) humans.
Automating logical reasoning is an important research
area in the field of artificial intelligence. The core of this
research area is called automated theorem proving.
My research interests are
within the field of automated theorem proving. More details can
be found in my publications. Most of the
theoretical results presented in these papers have been implemented.
The source code of these programs can be found in the
theorem provers section.
Please feel free to contact me.
My research interest is focused on areas in automated theorem proving
that are related to one or more of the following topics.
Connection-based theorem proving: developing proof methods
that are based on the connection calculus.
Non-classical logics: proof methods that deal with,
e.g., intuitionistic logic, modal logics or linear logic.
Non-clausal theorem proving: developing calculi that
work entirely on the original presentation of the given input.
Lean theorem proving: implementing provers that are
not only very compact but also have a strong performance.
Benchmark libraries: providing libraries for testing and
benchmarking provers for popular non-classical logics.
Program synthesis: using automated theorem provers
in the development of verifiably correct software.
Proof presentation: presenting proofs found by automated
theorem provers in a readable form.
I have served and am currently serving on the programme committees
and steering committees of the following international conferences
Programme committee member:
Member of the steering committee of
(International Joint Conference on Automated Reasoning).
President of the steering committee of
(International Conference on Automated Reasoning with Analytic
Tableaux and Related Methods).
Please contact me for more information or in case of questions.