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 The University of Bamberg () in Bamberg, Germany, specializes in the humanities, cultural studies, social sciences, economics, and applied computer science. Campus The university is partly housed in historical buildings in Bamberg's Old Town. ...

since 2022, in charge of the chair for AI Systems Engineering, and at the

FU Berlin The Free University of Berlin (, often abbreviated as FU Berlin or simply FU) is a public university, public research university in Berlin, Germany. It was founded in West Berlin in 1948 with American support during the early Cold War period a ...

since 2021.

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 in 1999 on the subject of Equality and Extensionality in Higher-Order Theorem Proving, supervised by

Michael Kohlhase Michael Kohlhase (born 13 September 1964, in Erlangen) is a German computer scientist and professor at University of Erlangen–Nuremberg, where he is head of the KWARC research group (Knowledge Adaptation and Reasoning for Content). Academic Po ...

and

Frank Pfenning Frank Pfenning is a German-American professor of computer science, adjunct professor in philosophy, and was head of the Computer Science Department at Carnegie Mellon University from 2013 to 2018. Education and career Pfenning grew up in Rüsse ...

. After spending time abroad in Birmingham and Edinburgh, he worked as a university lecturer at

Saarland University Saarland University (, ) is a public research university located in Saarbrücken, the capital of the German state of Saarland. It was founded in 1948 in Homburg in co-operation with France and is organized in six faculties that cover all major ...

from 2001 to 2008, including a research stay in Cambridge. He was then a professor at the in

Bruchsal Bruchsal (; South Franconian: ''Brusl'') is a city at the western edge of the Kraichgau, approximately 20 km northeast of Karlsruhe in the state of Baden-Württemberg, Germany. It is located on Bertha Benz Memorial Route. Bruchsal is the lar ...

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.

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 The University of Luxembourg (French language, French: ''Université du Luxembourg''; German language, German: ''Universität Luxemburg''; Luxembourgish language, Luxembourgish: ''Universitéit Lëtzebuerg'') is a Public university, public researc ...

Stanford University Leland Stanford Junior University, commonly referred to as Stanford University, is a Private university, private research university in Stanford, California, United States. It was founded in 1885 by railroad magnate Leland Stanford (the eighth ...

(USA),

University of Cambridge The University of Cambridge is a Public university, public collegiate university, collegiate research university in Cambridge, England. Founded in 1209, the University of Cambridge is the List of oldest universities in continuous operation, wo ...

(UK),

Carnegie Mellon University Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania, United States. The institution was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools. In 1912, it became the Carnegie Institu ...

(USA), BITS Pilani Dubai (UAE) and

Zhejiang University Zhejiang University (ZJU) is a public university, public research university in Hangzhou, Zhejiang, China. It is affiliated with the Ministry of Education (China), Ministry of Education. The university is part of Project 211, Project 985, and D ...

(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 The Confederation of Laboratories for Artificial Intelligence Research in Europe (CAINRE) (formally known as CLAIRE) is a European organisation, created to strengthen artificial intelligence (AI) and human-centred AI research and innovation, in E ...

(CLAIRE-AI), member of the Graduate School Berlin Mathematical Research Centre (MATH+) and the

Federation of German Scientists The Federation of German Scientists - VDW (Vereinigung Deutscher Wissenschaftler e. V.) is a German non-governmental organization. History Since its founding 1959 by Carl Friedrich von Weizsäcker, Otto Hahn, Max Born and further prominent nuclea ...

. He is best known for his work on formalising

Gödel's ontological proof Gödel's ontological proof is a formal argument by the mathematician Kurt Gödel (1906–1978) for the existence of God. The argument is in a line of development that goes back to Anselm of Canterbury (1033–1109). St. Anselm's ontological argume ...

in 2014, 2025 and verifying the theorems using

automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a majo ...

with

Isabelle Isabel is a female name of Iberian origin. Isabelle is a name that is similar, but it is of French origin. It originates as the medieval Spanish form of '' Elisabeth'' (ultimately Hebrew ''Elisheba''). Arising in the 12th century, it became popul ...

in 2016. The proof could be confirmed by researchers from TU Vienna. For the formalisation and the proof, Benzmüller gained attention by the national press and internationally across interdisciplinary researchers.

References

External links

Home pageComments on the formalisation and automation of foundational theories from the point of view of LogiKEy

( Terra X with

Harald Lesch Harald Lesch (born 28 July 1960) is a German physicist, astronomer, natural philosopher, author, television presenter, professor of physics at the Ludwig Maximilian University of Munich (LMU) and professor of natural philosophy at the Munich Un ...

) * {{DEFAULTSORT:Benzmueller, Christoph Living people German computer scientists Academic staff of the University of Bamberg Year of birth missing (living people)