Christoph Benzmüller

Christoph Benzmüller
Nationality	German
Alma mater	Saarland University
Known for	Formal reasoning Theorem proving
Scientific career
Institutions	University of Bamberg FU Berlin
Thesis	Equality and Extensionality in Higher-Order Theorem Proving[1]  (1999)
Doctoral advisor	Jörg H. Siekmann [de] Michael Kohlhase Frank Pfenning

Christoph Benzmüller is a German computer scientist whose research interests include formalisation of rational arguments by using symbolic artificial intelligence. He has been professor at the University of Bamberg since 2022, in charge of the chair for AI Systems Engineering, and at the FU Berlin since 2021.[2]

Education and career

Benzmüller studied computer science at Saarland University from 1989. He completed his studies in 1995 with a diploma. He then completed his doctorate under Jörg H. Siekmann [de] in 1999 on the subject of Equality and Extensionality in Higher-Order Theorem Proving, supervised by Michael Kohlhase and Frank Pfenning.[1] After spending time abroad in Birmingham and Edinburgh, he worked as a university lecturer at Saarland University from 2001 to 2008, including a research stay in Cambridge. He was then a professor at the International University in Germany [de] in Bruchsal until 2009. Benzmüller gained his habilitation at Saarland University in 2008 and at the FU Berlin in 2012. After research stays in Stanford and Luxembourg, he has been an apl. professor at the FU Berlin since 2021. In February 2022, he accepted an appointment at the University of Bamberg.[3]

Recognition

Benzmüller conducts research at the intersection of artificial intelligence, philosophy, mathematics and language processing. On the one hand, he is interested in formal reasoning and universal logic with applications in philosophy/metaphysics and mathematics, and on the other hand in the development of hybrid AI technologies for the ethical and legal control of AI systems. In the context of research stays and visiting professorships, he has established collaborations with numerous international institutions, including University of Luxembourg, Stanford University (USA), University of Cambridge (UK), Carnegie Mellon University (USA), BITS Pilani Dubai (UAE) and Zhejiang University (China). He serves on various international committees, advises AI start-ups, is the national contact person for the Confederation of Laboratories for Artificial Intelligence Research in Europe (CLAIRE-AI), member of the Graduate School Berlin Mathematical Research Centre (MATH+) and the Federation of German Scientists.[3]

He is best known for his work on formalising Gödel's ontological proof in 2014[4][5] and verifying the theorems using automated theorem proving with Isabelle in 2016.[6][7][8] The proof could be confirmed by researchers from TU Vienna.[5][9] For the formalisation and the proof, Benzmüller gained attention by the national press[10][11][12] and internationally across interdisciplinary researchers.[13]

References

1. Equality and Extensionality in Higher-Order Theorem Proving, Saarland University Library, 29 June 2022, retrieved 2024-10-15
2. FU Berlin, retrieved 2024-12-25
3. CV (PDF), retrieved 2024-10-15
4. Christoph Benzmüller and Bruno Woltzenlogel-Paleo (2014). "Automating Gödel's Ontological Proof of God's Existence with Higher-Order Automated Theorem Provers" (PDF). Proc. European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications. Vol. 263. IOS Press. pp. 93–98. Archived (PDF) from the original on 2014-07-14.
5. "FormalTheology/GoedelGod". GitHub. 28 June 2021.
6. Christoph Benzmüller and Bruno Woltzenlogel-Paleo (Jul 2016). "The Inconsistency in Gödel's Ontological Argument: — A Success Story for AI in Metaphysics" (PDF). In Subbarao Kambhampati (ed.). Proc. 25th International Joint Conference on Artificial Intelligence. AAAI Press. pp. 936–942. Archived (PDF) from the original on 2016-11-13.
7. Christoph Benzmüller and David Fuenmayor (May 2017). "Types, Tableaus and Gödel's God in Isabelle/HOL". Archive of Formal Proofs. ISSN 2150-914X.
8. Types, Tableaus and Gödel's God in Isabelle/HOL, retrieved 2024-12-25
9. FU Berlin, 2013-10-17, retrieved 2024-12-25
10. G(x) = Gott (in German), retrieved 2024-12-25
11. FU-Lehrpreis für Christoph Benzmüller: Der Gottesbeweiser (in German), retrieved 2024-12-25
12. KI-Forscher: Reale Existenz Gottes nicht absolut sicher, aber... (in German), retrieved 2024-12-25
13. Experiments in Computational Metaphysics: Gödel’s Proof of God’s Existence (in German), retrieved 2024-12-25

External links

• Home page
• Comments on the formalisation and automation of foundational theories from the point of view of LogiKEy
• Does God exist? (Terra X with Harald Lesch)
• Christoph Benzmüller publications indexed by Google Scholar