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.

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

• ORCID
• DBLP
• ResearchGate
• Google Scholar
• Deutsche Nationalbibliothek
• PGP 0A98 A9ED 65D1 A1BB FB88 D69A 6D1B B85D 6DEE 684B

Masters Theses (As Co-Supervisor)

• Kranz, T. : "Induction Provers in Hets: Leveraging the Tons of Inductive Problems language and tools to talk to more Automated Theorem Provers", 16.10.2022, OvGU Magdeburg, First supervisor: Prof. Dr.-Ing. T. Mossakowski

Bachelor Theses (As Co-Supervisor)

• Repp, L. : "Extending the Automated Theorem Prover nanoCoP with Arithmetic Procedures",  09.09.2022, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz
• Münch, K. : "Entwicklung einer performanten und verlässlichen Schnittstelle für leanCoP-Ω", 04.04.2021, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz
• Behrens, A. : "Modernisierung von Legacy Beweissystemen", 30.09.2019, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz - PDF,BibTex
• Engelhard, C. : "Konzeption und Implementierung eines Interfaces zwischen SAT/SMT Solvern und automatischen Beweissystemen", 20.12.2018, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz
• Martin, J. : "Analyse und Prototypische Implementierung des SUP-INF-Algorithmus für Presburger Arithmetik", 26.05.2017, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz

• 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)

Repp, L.; Frank, M. (2024) nanoCoP-Ω: A Non-Clausal Connection Prover with Arithmetic. In: Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (Prague, Czech Republic, Sept. 18, 2023). Ed. by Jens Otten and Wolfgang Bibel. CEUR Workshop Proceedings 3613. Aachen, 2024, pp. 41–53.

Frinker, N.; Liebergeld, S.; Dr. Otto, A.; Frank, M.; Egger, M. (2023) Eine vertrauenswürdige, sichere Public Cloud - Utopie oder Realität. In: Digital sicher in eine nachhaltige Zukunft. 19. Deutscher IT-Sicherheitskongress. Bundesamt für Sicherheit in der Informationstechnik - BSI, 2023, pp. 227–240. ISBN: 978-3-922746-85-0.

Frinker, N.; Frank, M.; Liebergeld, S. (2023) “VerSeCloud. Der Weg zur vertrauenswürdigen und sicheren Cloud ”Made in Germany””. In: Behörden Spiegel. Jahrgang. 39. Nr. 4 (2023), p. 31, ISSN: 1437-8337.

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.

Artifact Evaluation Committee

• 18th International Conference on integrated Formal Methods (iFM 2023)

Competitions

• Cade ATP Systems Competition (CASC-24), System: TEMPLAR::leanCoP
• Cade ATP Systems Competition (CASC-J6), System: leanCoP-ARDE