Publications (recent selection)
Bayer, J., Benzmüller, C., Buzzard, K., David, M., Lamport, L., Matiyasevich, Y., Paulson, L., Schleicher, D., Stock, B., & Zelmanov, E. (2024). Mathematical Proof Between Generations. Notices of the American Mathematical Society, 71(1), 79–92.
Benzmüller, C. (2024). Who finds the short proof?: Searching for Wormholes in Proof-Space. Dagstuhl Reports, 13(10), 6.
Benzmüller, C., & Andrews, P. (2024). Church’s Type Theory. Stanford Encyclopedia of Philosophy.
Benzmüller, C., Fuenmayor, D., & Lomfeld, B. (2024). Modelling Value-Oriented Legal Reasoning in LogiKEy. Logics, 2(1), 31–78.
Parent, X., & Benzmüller, C. (2024). Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset). Archive of Formal Proofs.
Solopova, V., Herman, V., Benzmüller, C., & Landgraf, T. (2024a). Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection (pp. 1–8). arXiv.
Solopova, V., Herman, V., Benzmüller, C., & Landgraf, T. (2024b). Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection. Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics: System Demonstrations, 44–51.
Steen, A., & Benzmüller, C. (2024). What are Non-classical Logics and Why Do We Need Them?: An Extended Interview with Dov Gabbay and Leon van der Torre. Künstliche Intelligenz, Online-First.
Steen, A., Sutcliffe, G., & Benzmüller, C. (2024). Solving Quantified Modal Logic Problems by Translation to Classical Logics. arXiv.
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.
Passon, O., Benzmüller, C., & Falkenburg, B. (Eds.). (2023). On G?del and the Nonexistence of Time: G?del und die Nichtexistenz der Zeit; Kurt G?del essay competition 2021: Kurt-G?del-Preis 2021 (1st ed.). Springer Spektrum Berlin.
Baroni, P., Benzmüller, C., & Wáng, Y. (Eds.). (2023). Journal of logic and computation (Vol. 33, Issues 2, Special Issue: Logic and Argumentation). Oxford University Press.
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.
Bayer, J., Gonus, A., Benzmüller, C., & Scott, D. S. (2023). Category Theory in?Isabelle/HOL as?a?Basis for?Meta-logical Investigation. Intelligent Computer Mathematics: 16th International Conference, CICM 2023, Cambridge, UK, , September 5–8, 2023 Proceedings, 69–83.
Benzmüller, C. (2023c). A Simplified Variant of G?del’s Ontological Argument. In A. Vestrucci (Ed.), Beyond Babel: Religion and Linguistic Pluralism: Vol. Sophia Studies in Cross-cultural Philosophy of Traditions and Cultures ; vol 43. (1st ed., pp. 271–286). Springer International Publishing.
Benzmüller, C. (2023a). Reasonable, Trusted AI through Symbolic Ethico-legal Control and Reflection? (Keynote Abstract). The Florida Artificial Interlligence Research Society, 2023(36).
Benzmüller, C. (2023b). Is HOL (as a metalogic) all we need for flexible normative reasoning?. Dagstuhl Reports, 13(4), 22.
Benzmüller, C., Bayer, J., Gonus, A., & Scott, D. S. (2023). Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation (pp. 1–16). arXiv.
Benzmüller, C., & Fuenmayor, D. (2023). Mathematical Proof Assistants for Teaching Logic: the LogiKEy Methodology. Book of Abstracts: International Congress Tools for Teaching Logic V, 1–3. https://doi.org/10.20378/irb-59552
Benzmüller, C., Fuenmayor, D., Steen, A., & Sutcliffe, G. (2023). Who Finds the Short Proof?. Logic Journal of the IGPL, Online First, 1–23.
Benzmüller, C., & Reiche, S. (2023). Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy. Journal of Logic and Computation, 33(6), 1243–1269.
Benzmüller, C., Solopova, V., Landgraf, T., & Popescu, O.-I. (2023). Automated Multilingual Detection of Pro-Kremlin Propaganda in Newspapers and Telegram Posts. Datenbank-Spektrum, 25(1).
Parent, X., & Benzmüller, C. (2023b). Normative Conditional Reasoning as a Fragment of HOL (pp. 1–22). arXiv.
Parent, X., & Benzmüller, C. (2023a). 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.
Rothgang, C., Rabe, F., & Benzmüller, C. (2023b). Theorem Proving in?Dependently-Typed Higher-Order Logic. Automated Deduction – CADE 29: 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings, 438–455.
Rothgang, C., Rabe, F., & Benzmüller, C. (2023a). Theorem Proving in Dependently-Typed Higher-Order Logic: Extended Preprint (Issue arXiv:2305.15382). arXiv.
Solopova, V., Benzmüller, C., & Landgraf, T. (2023). The Evolution of Pro-Kremlin Propaganda From a Machine Learning and Linguistics Perspective. Proceedings of the Second Ukrainian Natural Language Processing Workshop (UNLP 2023), 40–48.
Solopova, V., Gruszczynski, A., Rostom, E., Cremer, F., Witte, S., Zhang, C., López, F. R., Pl??l. Lea, Hofmann, F., Romeike, R., Gl?ser-Zikuda, M., Benzmüller, C., & Landgraf, T. (2023). PapagAI: Automated Feedback for Reflective Essays (pp. 1–12). arXiv.
Solopova, V., Popescu, O.-I., Benzmüller, C., & Landgraf, T. (2023). Automated multilingual detection of Pro-Kremlin propaganda in newspapers and Telegram posts. arXiv.
Solopova, V., Rostom, E., Cremer, F., Gruszczynski, A., Witte, S., Zhang, C., López, F. R., Pl??l. Lea, Romeike, R., Gl?ser-Zikuda, M., Hofmann, F., Landgraf, T., & Benzmüller, C. (2023). PapagAI: Automated Feedback for?Reflective Essays. KI 2023: Advances in Artificial Intelligence: 46th German Conference on AI, Berlin, Germany, September 26–29, 2023; Proceedings, 198–206.
Steen, A., Sutcliffe, G., Scholl, T., & Benzmüller, C. (2023). Solving Modal Logic Problems by?Translation to?Higher-Order Logic. In A. Herzig, J. Luo, & P. Pardo (Eds.), Logic and Argumentation: 5th International Conference, CLAR 2023, Hangzhou, China, September 10-12, 2023; Proceedings (Vol. 14156, pp. 25–43). Springer Nature Switzerland.
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.
Benzmüller, C. (2022b). A Simplified Variant of G?del’s Ontological Argument. Zygon, 57(4), 953–962.
Benzmüller, C. (2022a). Symbolic AI and G?del’s Ontological Argument. Zygon, 57(4).
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., 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.
Benzmüller, C., Fuenmayor, D., & Lomfeld, B. (2022). Modelling Value-oriented Legal Reasoning in LogiKEy. arXiv.
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.
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.
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.
Steen, A., Sutcliffe, G., Glei?ner, T., & Benzmüller, C. (2022). Solving QMLTP Problems by Translation to Higher-order Logic. arXiv.
Passon, O., & Benzmüller, C. (Eds.). (2021). Wider den Reduktionismus: Ausgew?hlte Beitr?ge zum Kurt G?del Preis 2019. Springer Spektrum.
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. (2021a). Value-Oriented Legal Argumentation in Isabelle/HOL. Leibniz International Proceedings in Informatics (LIPIcs), 193, 1–20.
Benzmüller, C., & Fuenmayor, D. (2021b). Cantor’s Theorem without Reductio Ad Absurdum (pp. 1–3). Research Gate.
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.
Benzmüller, C., & Reiche, S. (2021a). Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL. Archive of Formal Proofs.
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.
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.
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.
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.
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.
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.
Benzmüller, C., Fuenmayor, D., & Lomfeld, B. (2020). Modelling Value-oriented Legal Reasoning in LogiKEy (pp. 1–57). arXiv.
Benzmüller, C., & Lomfeld, B. (2020a). Reasonable Machines: a Research Manifesto (pp. 1–8). arXiv.
Benzmüller, C., & Lomfeld, B. (2020b). Reasonable Machines: a Research Manifesto. KI 2020, 12325, 251–258.
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.
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.
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.
Fuenmayor, D., & Benzmüller, C. (2020b). Normative Reasoning with Expressive Logic Combinations. ECAI 2020, 325, 2903–2904.
Fuenmayor, D., & Benzmüller, C. (2020e). Higher-order Logic as Lingua Franca -- Integrating Argumentative Discourse and Deep Logical Analysis. arXiv.
Fuenmayor, D., & Benzmüller, C. (2020c). Computer-Supported Analysis of Arguments in Climate Engineering. Lecture Notes in Computer Science, 12061, 104–115.
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.
Fuenmayor, D., & Benzmüller, C. (2020d). Higher-order Logic as Lingua Franca: Integrating Argumentative Discourse and Deep Logical Analysis (pp. 1–35). arXiv.
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.
Reiche, S., & Benzmüller, C. (2020b). Public Announcement Logic in HOL. Lecture Notes in Computer Science, 12569(12569), 222–238.
Reiche, S., & Benzmüller, C. (2020a). Public Announcement Logic in HOL (pp. 1–17). arXiv.
Steen, A., & Benzmüller, C. (2020b). The Higher-Order Prover Leo-III. Frontiers in Artificial Intelligence and Applications, 2020(325), 2937–2938.
Steen, A., & Benzmüller, C. (2020a). On Reductions of Hintikka Sets for Higher-Order Logic (pp. 1–10). arXiv.
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.
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.
Benzmüller, C. (2019a). Universal (meta-)logical reasoning: The Wise Men Puzzle (Isabelle/HOL dataset). Data in Brief, 24(June, 103823).
Benzmüller, C. (2019b). What is a proof? What should it be?. In arXiv. arXiv.org.
Benzmüller, C. (2019c). Universal (meta-)logical reasoning: Recent successes. Science of Computer Programming, 172(1), 48–62.
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.
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.
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.
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.
Fuenmayor, D., & Benzmüller, C. (2019e). Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories (pp. 1–14). arXiv.
Fuenmayor, D., & Benzmüller, C. (2019a). Computational Hermeneutics: an Integrated Approach for the Logical Analysis of Natural-Language Arguments. Logic in Asia, 187–207.
Fuenmayor, D., & Benzmüller, C. (2019d). A Computational-Hermeneutic Approach for Conceptual Explicitation (pp. 1–29). arXiv.
Fuenmayor, D., & Benzmüller, C. (2019c). A Computational-Hermeneutic Approach for Conceptual Explicitation. Studies in Applied Philosophy, Epistemology and Rational Ethics, 49, 441–469.
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.
Kirchner, D., Benzmüller, C., & Zalta, E. N. (2019b). Computer Science and Metaphysics: a Cross-Fertilization (pp. 1–39). arXiv.
Kirchner, D., Benzmüller, C., & Zalta, E. N. (2019c). Computer Science and Metaphysics: a Cross-Fertilization. Open Philosophy, 2(1), 230–251.
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.
Steen, A., & Benzmüller, C. (2019). Extensional Higher-Order Paramodulation in Leo-III (pp. 1–34). arXiv.
Tiemens, L., Scott, D. S., Benzmüller, C., & Benda, M. (2019). Computer-supported Exploration of a Categorical Axiomatization of Modeloids (pp. 1–24). arXiv.
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.
Wisniewski, M., Steen, A., Kern, K., & Benzmüller, C. (2016). Effective Normalization Techniques for HOL. Automated Reasoning — 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016, Proceedings, 362–370.