Job Offers for Academic Positions at Freie Universität Berlin

Department of Mathematics and Informatics
Institute of Computer Science

Research assistent
limited to 3 years
Entgeltgruppe 13 TV-L FU

Job description:

Project "Effective Higher-Order Automated Theorem Proving LEO-III" funded by the German Research Foundation (DFG); Significant progress has recently been achieved in higher-order automated theorem proving. This includes the improvement of existing provers and the development of new provers and model finders. Moreover, many new application domains have been explored and a high number of experiments have been carried out. These experiments show that higher-order theorem proving systems can solve relevant problems in many application domains that cannot be solved effectively in less expressive logics. This progress has been fostered by the new international TPTP THF infrastructure. The goals of the LEO-III project in research and technology are versatile, but strongly interrelated. One common pattern in several of our research tasks is the idea to exploit, transfer, and adapt selected theoretical and technological achievements in first-order automated theorem proving for the higher-order context. This way we want to improve overall automation and make it readily available to a range of scientists from other fields, including AI, mathematics, and philosophy.

The cooperative architecture of previous LEO provers has supported the mediation between expressive modeling languages and restricted, but computationally more tractable logics for proof automation. This mediation is an inherent principle of the LEO approach and will be further explored in the LEO-III project.

The list of objectives includes:

  • Novel calculi and new design for LEO-III: the new system will be based on paramodulation/superposition
  • term-orderings, labeling techniques, and free-variable representations will be adapted and further developed for these purposes; flexible, concurrent collaboration with specialist reasoners for first-order logic and novel collaborations with specialist reasoners for other computationally interesting fragments of higher-order logic
  • Provision of proof objects and support for the integration of LEO-III with proof assistants or other AI systems
  • application and evaluation of LEO-III; dissemination of LEO-III and contribution to the build-up resp. extension of an international infrastructure.

The range of objectives is from technological challenges to foundational, theoretical issues. The research methods include theory, modeling, implementation, and evaluation.

The candidate is expected to support the principal investigator in the implementation of the Project and to carry out major parts of the proposed research.


  • MSc in Computer Science, Mathematics, or Theoretical Philosophy


We are seeking a candidate with a strong background in automated theorem proving, ideally in higher order logics. Familarity with LEO-II and/or Isabelle or Coq will be favorable.

Applications quoting the reference code 721101-wiMi shall be addressed not later than to 29th of September

Freie Universität Berlin
Fachbereich Mathematik und Informatik
Institut für Informatik
Herrn Dr. Christoph Benzmüller
Arnimallee 7
14195 Berlin (Dahlem)

The newly established interdisciplinary

Collaborative Research Center 1114 "Scaling Cascades in Complex Systems - Across-Scale Modeling and Simulation Paradigms"

offers the following open project positions for

2 PhD Students
(part time 75% / 65%)
The fixed term contract is limited to 30.06.2018
with salary according to E13 TV-L FU

In the following project:

a) Project B01: 1 PhD student position
part time 75%
Reference: SFB 1114-B01-a

Fault networks and scaling properties of deformation accumulation
Institute for Mathematics
Contact: Prof. Dr. Ralf Kornhuber,

Job description:

  • Numerical analysis of rate- and state-dependent friction models
  • Development, analysis, and implementation of multi-scale models for fault networks


  • Diploma / M.Sc. in Mathematics

Desired qualifications:

  • Substantial knowledge in the analysis and numerical analysis of partial differential equations
  • in particular from continuum mechanics
  • adaptive finite elements
  • multigrid methods
  • programming in C or C++

b) Project B05: 1 PhD student position
65% part-time
Reference: SFB1114-B05-b

Origin of the scaling cascades in protein dynamics
Institute of Theoretical Physics
Contact: Prof. Dr. Petra Imhof,

Job description:

  • First principles molecular dynamics simulations of peptides and analysis of their conformation dynamics
  • Computation of linear and 2D-Infrared spectra and analysis of vibrational couplings


  • Diploma / M.Sc. in Physics, Chemistry or a closely related field

Desired qualifications:

  • Proven experience in molecular simulations, ideally with first-principles methods
  • very good knowledge of electronic structure theory, especially Density Functional Theory
  • Solid background in statistical mechanics
  • good programming skills
  • preferably with Java or C++
  • good communication skills and ability to work in a cross-disciplinary research environment

Applications are to be submitted no later than September 28, 2014, electronically only, via the project website

Published by the President's Office of Freie Universität Berlin
Edited by Div. II A 2 - Personnel Management

Last Update: Sep 22, 2014