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., & 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. https://doi.org/10.1093/logcom/exac091
Benzmüller, C. (2023). Reasonable, Trusted AI through Symbolic Ethico-legal Control and Reflection? (Keynote Abstract). The Florida Artificial Interlligence Research Society, 2023(36). https://doi.org/10.32473/flairs.36
Benzmüller, C., Fuenmayor, D., Steen, A., & Sutcliffe, G. (2023). Who Finds the Short Proof?. Logic Journal of the IGPL, Online First, 1–23. https://doi.org/10.1093/jigpal/jzac082
Benzmüller, C., Solopova, V., Popescu, O.-I., & Landgraf, T. (2023). Automated Multilingual Detection of Pro-Kremlin Propaganda in Newspapers and Telegram Posts. Datenbank-Spektrum, 25(1). https://doi.org/10.1007/s13222-023-00437-2
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.
Rothgang, C., Rabe, F., & Benzmüller, C. (2023). Theorem Proving in Dependently-Typed Higher-Order Logic: Extended Preprint (Issue arXiv:2305.15382). arXiv. https://doi.org/10.48550/ARXIV.2305.15382
Solopova, V., Popescu, O.-I., Benzmüller, C., & Landgraf, T. (2023). Automated multilingual detection of Pro-Kremlin propaganda in newspapers and Telegram posts. arXiv. https://doi.org/10.48550/ARXIV.2301.10604
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. (2022b). A Simplified Variant of Gödel’s Ontological Argument. Zygon, 57(4), 953–962. https://doi.org/10.1111/zygo.12830
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. (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. 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. (2020a). Reasonable Machines: a Research Manifesto (pp. 1–8). arXiv. https://doi.org/10.48550/ARXIV.2008.06250
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., 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. (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
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. (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
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
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. (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. (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
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. (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
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. (2019b). Computer Science and Metaphysics: a Cross-Fertilization (pp. 1–39). arXiv. https://doi.org/10.48550/ARXIV.1905.00787
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
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