Jens Otten
   Senior Researcher
University of Oslo  

Theorem Provers
Welcome! Willkommen!

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.

Research Interests

My research interests are 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.

Professional Activities

I serve on the program and steering committees of the following international conferences and workshops.

  • Member of the steering committee of IJCAR (International Joint Conference on Automated Reasoning).
  • President of the steering committee of TABLEAUX (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods).


Please feel free to contact me if you need any further information.

Jens Otten · Institutt for informatikk · University of Oslo · 01.01.2017