Portrait Mario Frank

Dipl.-Inf. Mario Frank


University of Potsdam
Department of Computer Science
Campus Golm
Building 70, Room 1.05
An der Bahn 2
14476 Potsdam, Germany

Curriculum Vitae

Mario Frank studied Computer Science at the Potsdam University from the year 2007 and finished his Diploma thesis in 2013. During his studies, he collaborated with the Corpus Linguistics Chair of the Humboldt University, the Potsdam University and the Ruhr-Universität Bochum. During these collaborations, he focused on the processing and transformation of corpora. In the latter years of his studies, he specialised on the automated processing of big formula sets, especially their reduction, with application of linguistic concepts for automated text summarisation and unification based graph search. As a result of his specialisation, he attended the CADE ATP Systems Competition twice in cooperation with Dr. Jens Otten.

After finishing his studies, he began his PhD Studies under supervision of Prof. Dr. Christoph Kreitz, head of the Theoretical Computer Science Chair, in the area of automated and interactive theorem proving. In 2014/2015, he applied the Junior Teaching Professionals Program of the Potsdam Graduate School and gained his first experience as lecturer and co-lecturer.

He worked as technical assistant for the projects "Reisen.UP" and "Beschaffung.UP" at the CIO division from 2014 to 2016. During this time, he supported the projects with his knowledge of complexity theory, logics, software and requirements engineering. He worked as research assistant at the Theoretical Computer Science Chair from 2016 until 30.06.2021. Since 01.07.2021, he works on the consortial project VERSECLOUD as research assistant at the Theoretical Computer Science Chair.

Research Interests

  • Interactive and automated theorem proving
  • Software synthesis (frameworks)
  • Proof visualiastion
  • Usability in interactive theorem proving

Supervised Student Theses

As Co-Supervisor

  • Münch, K. : "Entwicklung einer performanten und verlässlichen Schnittstelle für leanCoP-Ω", Bachelor Thesis, 04.04.2021
  • Behrens, A. : "Modernisierung von Legacy Beweissystemen", Bachelor Thesis, 30.09.2019 - PDF,BibTex
  • Engelhard, C. : "Konzeption und Implementierung eines Interfaces zwischen SAT/SMT Solvern und automatischen Beweissystemen", Bachelor Thesis, 20.12.2018
  • Martin, J. : "Analyse und Prototypische Implementierung des SUP-INF-Algorithmus für Presburger Arithmetik", Bachelor Thesis, 26.05.2017


  • Summer term 2020: Theoretical Computer Science II - Efficient Algorithms (Co-Lecturer)
  • Summer term 2019: Theoretical Computer Science II - Efficient Algorithms (Co-Lecturer)
  • Winter term 2017/2018: Theoretical Computer Science I - Modelling: Automatons and formal languages (Co-Lecturer)
  • Winter term 2016/2017: Theoretical Computer Science I - Modelling: Automatons and formal languages (Co-Lecturer)
  • Summer term 2015: ATP Construction Project (Lecturer, under supervision of Prof. Dr. Kreitz )
  • Winter term 2014/2015: Seminar Theoretische Informatik - Methoden des automatischen Theorembeweisens (Lecturer, under supervision of Prof. Dr. Kreitz )
  • Summer term 2014: Seminar Theoretische Informatik - Funktionale Programmierung mit Haskell (Co-Lecturer)

Als tutor:

  • Theoretical Computer Science I (Winter term 2012/2013) und Theoretical Computer Science II (Summer term 2012)
  • Distributed Systems (Summer term 2012)
  • Programming (Summer term 2011)
  • Rechner- und Netzbetrieb (Winter term 2010/2011 and 2011/2012)


Kreitz, C.; Frank, M (2020). Automatische Inferenz. In: Handbuch der Künstlichen Intelligenz. Ed. by Günther Görz, Ute Schmid, and Tanya Braun. Berlin, Boston: De Gruyter, Dec. 16, 2020. Chap. 5, pp. 143–188. ISBN: 978-3-11-065984-9.

Frank, M (2020). The Coq Proof Script Visualiser (coq-psv). 11th Coq Workshop, colocated with IJCAR ’20. July 2020. Published as ePrint on arXiv.

Schellhorn, S.; Frank, M; Kreitz, C. (2019). Brückenkurse für mathematische und informatiknahe Studiengänge. In: Alles auf Anfang!. Ed. by Wilfried Schubarth, Sylvi Mauermeister, Friederike Schulze-Reichelt and Andreas Seidel. Potsdamer Beiträge zur Hochschulforschung, Heft 4 (2019). pp. 257-271. ISBN: 978-3-86956-452-4.

Frank, M.; Kreitz, C. (2018). A Theorem Prover for Scientific and Educational Purposes. EPTCS Vol. 267 (pp. 59-69).

Frank, M (2013/2014). TEMPLAR - Efficient Determination of Relevant Axioms in Big Formula Sets for Theorem Proving. Diploma Thesis, published 2014 online at the Institutional Repositoryof the University of Potsdam

Frank, M (2012/2014). ARDE - Technical Report. Studentische Arbeit, published 2014 online at the Institutional Repository of the University of Potsdam

Frank, M. (2012). Relevanzbasiertes Preprocessing für automatische Theorembeweiser. In J. Schmidt, T. Riechert & S. Auer (ed.), SKIL 2012 - Dritte Studentenkonferenz Informatik Leipzig , Vol. 34 (pp. 87-98) . LIV . ISBN: 978-3-941608-21-4.

Further publications can be found under my ORCID profile.