Prof. Dr. Christoph Benzmüller

E-Mail: christoph.benzmueller(at)uni-bamberg.de

Address: An der Weberei 5, 96047 Bamberg

Office: WE_5/05.090

Tel.: +49 (0)951/863-2942

Office hours: on request

Prof. Christoph Benzmüller is since 2022 chair for AI Systems Development at the University of Bamberg. As an associate (apl.) professor he is also affiliated with the Department of Mathematics and Computer Science at Freie Universität Berlin (where he has been the first UNA Europa guest chair) and he maintains a close research collaboration with the University of Luxembourg. In addition, he advises AI startup companies in Germany and abroad.

Benzmüller's research interests lie at the intersection of AI/computer science, philosophy, mathematics, and language. His research shows that rational arguments can now be very well mechanized and analyzed in computers by using modern, symbolic AI technology. Benzmüller and his team have developed their own automatic theorem provers (for classical and higher-level non-classical logics) and are applying them in the fields mentioned above. Benzmüller's studies of Gödel's ontological argument for the existence of God in the computer gained particular media attention. The range of applications of his work is far-reaching and concerns, among other things, the mechanisation of ethical-legal reasoning in computers, e.g., for the control of autonomous AI systems.

Benzmüller is convinced that AI, as a scientific discipline, should more strongly focus on the exploration of, and experimentation with, representing objects.* For Benzmüller, it is precisely the exploration and flexible processing of representing objects in combination with hybrid AI technology (fusion of symbolic and subsymbolic techniques) that constitues a core challenge and opportunity for the modeling of (strongly) intelligent AI systems. Explicit, declarative representations are particularly relevant for the realization of trusted and responsible AI systems, since they make normative (and other) knowledge not only transparent and explainable, but also efficiently and robustly communicable between humans and machines.

Benzmüller has conducted research as a visiting professor/scholar at numerous prestigious universities in Germany and abroad and has established a close research network. Stations in his career include: Free University of Berlin, University of Luxembourg, Stanford University (USA), International University in Germany, Cambridge University (UK), University of Birmingham (UK), University of Edinburgh (UK) and Carnegie Mellon University (USA). Benzmüller studied (1989-1995), received his PhD (1999) and habilitated (2006) at Saarland University.

Benzmüller's research activities have been funded by the DFG (Heisenberg Fellowship, Research Stipend, Research Grants, Collaborative Research Center), EPSRC/UK (Research Grant), Volkswagen Foundation (Experiment!), Studienstiftung des Deutschen Volkes (Doctoral Scholarship), ERC (Research Training Network), FNR/Luxembourg, BMBF, among others.

Prior to his academia career, Christoph Benzmüller was a successful long-distance runner at German national level.

(*The term "representing objects" goes back to the AI pioneer Wolfgang Bibel.)

Publications (recent selection)

Benzmüller, C., & Otten, J. (Eds.). (2023). CEUR Workshop Proceedings (Issues 3326, ARQNL 2022 Automated Reasoning in Quantified Non-Classical Logics 2022 : Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022) affiliated with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022)). RWTH Aachen.

Baroni, P., Benzmüller, C., & N Wáng, Y. (2023). Preface: Special Issue on Logic and Argumentation. Journal of Logic and Computation, Online First, 1–3. https://doi.org/10.1093/logcom/exac091

Parent, X., & Benzmüller, C. (2023). Automated Verification of Deontic Correspondences in Isabelle/HOL: First Results. CEUR Workshop Proceedings, 3326, Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022) affiliated with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022), 92–108.

Bayer, J., Benzmüller, C., Buzzard, K., David, M., Lamport, L., Matiyasevich, Y., Paulson, L., Schleicher, D., Stock, B., & Zelmanov, E. (2022). Mathematical Proof Between Generations (pp. 1–17). arXiv. https://doi.org/10.48550/ARXIV.2207.04779

Benzmüller, C. (2022c). Studies in Computational Metaphysics: Results of an Interdisciplinary Research Project. In H. Cukierman & F. Bertato (Eds.), Tópicos em História e Filosofia da Computação (pp. 129–160). University of Campinas (UNICAMP).

Benzmüller, C. (2022a). Symbolic AI and Gödel’s Ontological Argument. Zygon, Online First. https://doi.org/10.1111/zygo.12830

Benzmüller, C. (2022b). A Simplified Variant of Gödel’s Ontological Argument. arXiv. https://doi.org/10.48550/ARXIV.2202.06264

Benzmüller, C., Farjami, A., & Parent, X. (2022). Dyadic Deontic Logic in HOL: Faithful Embedding and Meta-Theoretical Experiments. In S. Rahman, M. Armgardt, & H. C. Nordtveit Kvernenes (Eds.), New developments in legal reasoning and logic: from ancient law to modern legal systems (pp. 353–377). Springer. https://doi.org/10.1007/978-3-030-70084-3_14

Benzmüller, C., Fuenmayor, D., Steen, A., & Sutcliffe, G. (2022b). Automation of Boolos’ Curious Inference in Isabelle/HOL. Archive of Formal Proofs.

Benzmüller, C., Fuenmayor, D., Steen, A., & Sutcliffe, G. (2022a). Who Finds the Short Proof?: an Exploration of Variants of Boolos’ Curious Inference using Higher-order Automated Theorem Provers. arXiv. https://doi.org/10.48550/ARXIV.2208.06879

Benzmüller, C., & Reiche, S. (2022). Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy. Journal of Logic and Computation, 1–28. https://doi.org/10.1093/logcom/exac029

Fuenmayor, D., & Benzmüller, C. (2022). Higher-order Logic as a Lingua Franca for Logico-Pluralist Argumentation. Logics for New-Generation AI: Second International Workshop. 10-12 June 2022, Zhuhai, 83–94.

Mucha, H., Correia de Barros, A., Benjamin, J. J., Benzmüller, C., Bischof, A., Buchmüller, S., de Carvalho, A., Dhungel, A.-K., Draude, C., Fleck, M.-J., Jarke, J., Klein, S., Kortekaas, C., Kurze, A., Linke, D., Maas, F., Marsden, N., Melo, R., Michel, S., … Berger, A. (2022). Collaborative Speculations on Future Themes for Participatory Design in Germany. I-Com, 21(2), 283–298. https://doi.org/10.1515/icom-2021-0030

Steen, A., Fuenmayor, D., Gleißner, T., Sutcliffe, G., & Benzmüller, C. (2022b). Automated Reasoning in Non-classical Logics in the TPTP World. CEUR Workshop Proceedings, CEUR-WS.Org.

Steen, A., Fuenmayor, D., Gleißner, T., Sutcliffe, G., & Benzmüller, C. (2022a). Automated Reasoning in Non-classical Logics in the TPTP World. arXiv. https://doi.org/10.48550/ARXIV.2202.09836

Steen, A., Sutcliffe, G., Gleißner, T., & Benzmüller, C. (2022). Solving QMLTP Problems by Translation to Higher-order Logic. arXiv. https://doi.org/10.48550/ARXIV.2212.09570

Passon, O., & Benzmüller, C. (Eds.). (2021). Wider den Reduktionismus: Ausgewählte Beiträge zum Kurt Gödel Preis 2019. Springer Spektrum. https://doi.org/10.1007/978-3-662-63187-4

Logic and Argumentation: 4th International Conference, CLAR 2021, Hangzhou, China, October 20–22, 2021, Proceedings. (2021). https://doi.org/10.1007/978-3-030-89391-0

Ammon, S., Beck, B., Benzmüller, C., Burchardt, A., Heidingsfelder, L. M., Kaiser, S., Lomfeld, B., Mühlhoff, R., Remmers, P., & Schraudner, M. (2021). KI als Laboratorium?: Ethik als Aufgabe!.

Benzmüller, C. (2021). Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL. Archive of Formal Proofs.

Benzmüller, C., & Fuenmayor, D. (2021). Value-Oriented Legal Argumentation in Isabelle/HOL. Leibniz International Proceedings in Informatics (LIPIcs), 193, 1–20. https://doi.org/10.4230/LIPICS.ITP.2021.7

Benzmüller, C., & Reiche, S. (2021a). Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL. Archive of Formal Proofs.

Benzmüller, C., & Reiche, S. (2021b). Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy (pp. 1–28). arXiv. https://doi.org/10.48550/ARXIV.2111.01654

Solopova, V., Popescu, O.-I., Chikobava, M., Romeike, F., Landgraf, T., & Benzmüller, C. (2021). A German Corpus of Reflective Sentences. Proceedings of the 18th International Conference on Natural Language Processing (ICON), 593–600.

Steen, A., & Benzmüller, C. (2021). Extensional Higher-Order Paramodulation in Leo-III. Journal of Automated Reasoning, 65, 775–807. https://doi.org/10.1007/s10817-021-09588-x

Benzmüller, C., & Miller, B. (Eds.). (2020). Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings. Springer International Publishing. https://doi.org/10.1007/978-3-030-53518-6

Benzmüller, C. (2020a). A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel’s Ontological Argument (pp. 1–11). arXiv. https://doi.org/10.48550/ARXIV.2001.04701

Benzmüller, C. (2020b). A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel’s Ontological Argument. Proceedings of the Seventeenth International Conference on Principles of Knowledge Representation and Reasoning, 779–789. https://doi.org/10.24963/kr.2020/80

Benzmüller, C., Farjami, A., Fuenmayor, D., Meder, P., Parent, X., Steen, A., van der Torre, L., & Zahoransky, V. (2020). LogiKEy workbench: Deontic logics, logic combinations and expressive ethical and legal reasoning (Isabelle/HOL dataset). Data in Brief, 33. https://doi.org/10.1016/j.dib.2020.106409

Benzmüller, C., & Fuenmayor, D. (2020). Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel’s Ontological Argument. Bulletin of the Section of Logic, 49(2), 127–148. https://doi.org/10.18778/0138-0680.2020.08

Benzmüller, C., Fuenmayor, D., & Lomfeld, B. (2020). Modelling Value-oriented Legal Reasoning in LogiKEy (pp. 1–57). arXiv. https://doi.org/10.48550/ARXIV.2006.12789

Benzmüller, C., & Lomfeld, B. (2020b). Reasonable Machines: a Research Manifesto. KI 2020, 12325, 251–258. https://doi.org/10.1007/978-3-030-58285-2_20

Benzmüller, C., & Lomfeld, B. (2020a). Reasonable Machines: a Research Manifesto (pp. 1–8). arXiv. https://doi.org/10.48550/ARXIV.2008.06250

Benzmüller, C., Parent, X., & Ricca, F. (2020). Introduction to the Special Issue on Logic Rules and Reasoning: Selected Papers from the 2nd International Joint Conference on Rules and Reasoning (RuleML+RR 2018). Theory and Practice of Logic Programming, 21(1), 1–3. https://doi.org/10.1017/S1471068420000113

Benzmüller, C., Parent, X., & van der Torre, L. (2020). Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. Artificial Intelligence, 287. https://doi.org/10.1016/j.artint.2020.103348

Benzmüller, C., & Scott, D. S. (2020). Automating Free Logic in HOL, with an Experimental Application in Category Theory. Journal of Automated Reasoning, 64, 53–72. https://doi.org/10.1007/s10817-018-09507-7

Fuenmayor, D., & Benzmüller, C. (2020d). Higher-order Logic as Lingua Franca: Integrating Argumentative Discourse and Deep Logical Analysis (pp. 1–35). arXiv. https://doi.org/10.48550/ARXIV.2007.01019

Fuenmayor, D., & Benzmüller, C. (2020a). A Case Study on Computational Hermeneutics: E. J. Lowe’s Modal Ontological Argument. In R. S. Silvestre, B. P. Göcke, J.-Y. Béziau, & P. Bilimoria (Eds.), Beyond Faith and Rationality: Sophia Studies in Cross-cultural Philosophy of Traditions and Cultures (Vol. 34, pp. 195–228). Springer. https://doi.org/10.1007/978-3-030-43535-6_12

Fuenmayor, D., & Benzmüller, C. (2020b). Normative Reasoning with Expressive Logic Combinations. ECAI 2020, 325, 2903–2904. https://doi.org/10.3233/FAIA200445

Fuenmayor, D., & Benzmüller, C. (2020c). Computer-Supported Analysis of Arguments in Climate Engineering. Lecture Notes in Computer Science, 12061, 104–115. https://doi.org/10.1007/978-3-030-44638-3_7

Makarenko, I., & Benzmüller, C. (2020). Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding. Lecture Notes in Computer Science, 12325, 116–131. https://doi.org/10.1007/978-3-030-58285-2_9

Reiche, S., & Benzmüller, C. (2020b). Public Announcement Logic in HOL. Lecture Notes in Computer Science, 12569(12569), 222–238. https://doi.org/10.1007/978-3-030-65840-3_14

Reiche, S., & Benzmüller, C. (2020a). Public Announcement Logic in HOL (pp. 1–17). arXiv. https://doi.org/10.48550/ARXIV.2010.00810

Steen, A., & Benzmüller, C. (2020b). The Higher-Order Prover Leo-III. Frontiers in Artificial Intelligence and Applications, 2020(325), 2937–2938. https://doi.org/10.3233/FAIA200462

Steen, A., & Benzmüller, C. (2020a). On Reductions of Hintikka Sets for Higher-Order Logic (pp. 1–10). arXiv. https://doi.org/10.48550/ARXIV.2004.07506

Tiemens, L., Scott, D. S., Benzmüller, C., & Benda, M. (2020). Computer-Supported Exploration of a Categorical Axiomatization of Modeloids. Lecture Notes in Computer Science, 12062, 302–317. https://doi.org/10.1007/978-3-030-43520-2_19

Selected Student Contributions and Workshop Papers of LuxLogAI 2018. (2019). 10.

Benzmüller, C., & Stuckenschmidt, H. (Eds.). (2019). KI 2019: Advances in Artificial Intelligence; 42nd German Conference on AI, Kassel, Germany, September 23-26, 2019, Proceedings. Springer. https://doi.org/10.1007/978-3-030-30179-8

Benzmüller, C. (2019b). What is a proof? What should it be?. In arXiv. arXiv.org. https://doi.org/10.48550/arXiv.1904.06332

Benzmüller, C. (2019a). Universal (meta-)logical reasoning: The Wise Men Puzzle (Isabelle/HOL dataset). Data in Brief, 24(June, 103823). https://doi.org/10.1016/j.dib.2019.103823

Benzmüller, C. (2019c). Universal (meta-)logical reasoning: Recent successes. Science of Computer Programming, 172(1), 48–62. https://doi.org/10.1016/j.scico.2018.10.008

Benzmüller, C., & Andrews, P. (2019). Church’s Type Theory. The Stanford Encyclopedia of Philosophy.

Benzmüller, C., Farjami, A., Meder, P., & Parent, X. (2019). I/O Logic in HOL. Journal of Applied Logics -- IfCoLoG Journal of Logics and Their Applications, 6(5), 715–733.

Benzmüller, C., Farjami, A., & Parent, X. (2019). Aqvist’s Dyadic Deontic Logic E in HOL. Journal of Applied Logics -- IfCoLoG Journal of Logics and Their Applications, 6(5), 733–755.

Benzmüller, C., & Fuenmayor, D. (2019). Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel’s Ontological Argument. arXiv. https://doi.org/10.48550/ARXIV.1910.08955

Benzmüller, C., Parent, X., & Ricca, F. (2019). Report on the Second International Joint Conference on Rules and Reasoning. AI Magazine, 40(2), 73–74. https://doi.org/10.1609/aimag.v40i2.2888

Benzmüller, C., Parent, X., & van der Torre, L. (2019). Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support (pp. 1–50). arXiv. https://doi.org/10.48550/ARXIV.1903.10187

Benzmüller, C., & Sutcliffe, G. (2019). Explicit Normative Reasoning and Machine Ethics. Arcade 2019 Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, 5.

Fuenmayor Pelaez, D., & Benzmüller, C. (2019). Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations. Lecture Notes in Computer Science, 112–128. https://doi.org/10.1007/978-3-030-29007-8_7

Fuenmayor, D., & Benzmüller, C. (2019e). Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories (pp. 1–14). arXiv. https://doi.org/10.48550/ARXIV.1903.09818

Fuenmayor, D., & Benzmüller, C. (2019d). A Computational-Hermeneutic Approach for Conceptual Explicitation (pp. 1–29). arXiv. https://doi.org/10.48550/ARXIV.1906.06582

Fuenmayor, D., & Benzmüller, C. (2019c). A Computational-Hermeneutic Approach for Conceptual Explicitation. Studies in Applied Philosophy, Epistemology and Rational Ethics, 49, 441–469. https://doi.org/10.1007/978-3-030-32722-4_25

Fuenmayor, D., & Benzmüller, C. (2019a). Computational Hermeneutics: an Integrated Approach for the Logical Analysis of Natural-Language Arguments. Logic in Asia, 187–207. https://doi.org/10.1007/978-981-13-7791-4_9

Fuenmayor, D., & Benzmüller, C. (2019b). Harnessing Higher-Order (Meta-) Logic to Represent and Reason with Complex Ethical Theories. Lecture Notes in Computer Science, 11670, 418–432. https://doi.org/10.1007/978-3-030-29908-8_34

Kirchner, D., Benzmüller, C., & Zalta, E. N. (2019a). Mechanizing prinzipia Logico-Metaphysica in functional type-theory. The Review of Symbolic Logic, 13(1), 206–218. https://doi.org/10.1017/S1755020319000297

Kirchner, D., Benzmüller, C., & Zalta, E. N. (2019c). Computer Science and Metaphysics: a Cross-Fertilization. Open Philosophy, 2(1), 230–251. https://doi.org/10.1515/opphil-2019-0015

Kirchner, D., Benzmüller, C., & Zalta, E. N. (2019b). Computer Science and Metaphysics: a Cross-Fertilization (pp. 1–39). arXiv. https://doi.org/10.48550/ARXIV.1905.00787

Steen, A., & Benzmüller, C. (2019). Extensional Higher-Order Paramodulation in Leo-III (pp. 1–34). arXiv. https://doi.org/10.48550/ARXIV.1907.11501

Tiemens, L., Scott, D. S., Benzmüller, C., & Benda, M. (2019). Computer-supported Exploration of a Categorical Axiomatization of Modeloids (pp. 1–24). arXiv. https://doi.org/10.48550/ARXIV.1910.12863

Zahoransky, V. (2019). Modelling the US Constitution to establish constitutional dictatorship. CEUR Workshop Proceedings, 2632, 1–13.

Fuenmayor, D., & Benzmüller, C. (2017). Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic. Lecture Notes in Artificial Intelligence, 10505, 114–127. https://doi.org/10.1007/978-3-319-67190-1_9