Lehrstuhl für KI-Systementwicklung

AI Systems Engineering (AISE)

Die Forschungsaktivitäten des AISE Lehrstuhls liegen in der Schnittstelle von Künstlicher Intelligenz, Philosophie, Mathematik, Informatik und natürlicher Sprache. Aktuelle Forschung des Teams konzentriert sich auf Mechanisierung von formaler Argumentation und Erklärungen im Computer, um vertrauenswürdige KI-Systeme zu entwickeln. Ein besonderes Interesse gilt der Verwendung von klassischer Logik höherer Ordnung (HOL) als universelle Meta-Logik, um verschiedene nicht-klassische Logiken zu automatisieren und sie in aktuellen Anwendungen zu nutzen, darunter Maschinenethik und Maschinenrecht, Metaphysik (z. B. Gödels ontologisches Argument), mathematische Grundlagen (z.B. Kategorientheorie) und rationale Argumentation. Die Forschungsaktivitäten des AISE Teams sind aber weitreichender, und befassen sich z.B. auch mit der Integration von automatisiertem Argumentieren, maschinellem Lernen und agentenbasierten Architekturen. Die Kernkompetenzen von Prof. Dr. Benzmüller liegen im Bereich der klassischen Logik höherer Stufe (HOL), zu deren Semantik und Beweistheorie er beigetragen hat. Zusammen mit Kollegen und Studenten hat er auch die Leo-Theorembeweiser für HOL entwickelt.

AISE Wissenschaftskommunikation

Benzmüller's Auftritt in der TerraX Folge "Die großen Fragen: Gibt es Gott?" erreichte ein Millionenpublikum. Auch beim Science Slam der Uni Bamberg am 27. Oktober präsentierte Benzmüller zentrale Hypothesen der AISE-Forschunglandschaft einem breiteren Publikum. Zusammen mit dem Bamberger Rapper ,,Bambägga'' gewann Benzmüller diesen Science Slam. Zuvor hatte Benzmüller auch schon andere Slams, z.B. vor dem roten Rathaus in Berlin und im bekannten Berliner Club SO36 sehr erfolgreich bestritten.

Aktuelle Publikationen des AISE Lehrstuhls (Auswahl seit 2022)

Benzmüller, Christoph/Heule, Marijn J.H./Schmidt, Renate A. (Hg.) (2024a): Automated Reasoning: 12th International Joint Conference: IJCAR 2024; Nancy, France, July 3–6, 2024; Proceedings. Cham: Springer Nature Switzerland.

Benzmüller, Christoph/Heule, Marijn J.H./Schmidt, Renate A. (Hg.) (2024b): Automated Reasoning: 12th International Joint Conference: IJCAR 2024; Nancy, France, July 3–6, 2024; Proceedings. Cham: Springer Nature Switzerland.

Steen, Alexander/Benzmüller, Christoph (Hg.) (2024a): Künstliche Intelligenz: KI; Forschung, Entwicklung, Erfahrungen. Berlin: Springer.

Bayer, Jonas et al. (2024): Mathematical Proof Between Generations. In: Notices of the American Mathematical Society 71, S. 79–92.

Benzmüller, Christoph (2024a): Who finds the short proof?: Searching for Wormholes in Proof-Space. In: Dagstuhl Reports 13, S. 6.

Benzmüller, Christoph (2024b): Logikbasierte Wissensverarbeitung. In: Furbach, Ulrich et al. (Hg.): Künstliche Intelligenz für Lehrkräfte: Eine fachliche Einführung mit didaktischen Hinweisen. Wiesbaden: Springer Vieweg. S. 139–162.

Benzmüller, Christoph/Andrews, Peter (2024): Church’s Type Theory. In: Stanford encyclopedia of philosophy.

Benzmüller, Christoph/Fuenmayor, David (2024): The LogiKEy Methodology: Applications in AI Ethics and Prospects in Logic Teaching. In: Formal Methods and Science in Philosophy V, International Conference, Book of AbstractS. Zagreb. S. 9–10.

Benzmüller, Christoph/Fuenmayor, David/Lomfeld, Bertram (2024): Modelling Value-Oriented Legal Reasoning in LogiKEy. In: Logics 2, S. 31–78.

Benzmüller, Christoph et al. (2024): Who Finds the Short Proof?. In: Logic journal of the IGPL 32, S. 442–464.

Furbach, Ulrich/Benzmüller, Christoph (2024): Schließen aus Wissen. In: Furbach, Ulrich et al. (Hg.): Künstliche Intelligenz für Lehrkräfte: Eine fachliche Einführung mit didaktischen Hinweisen. Wiesbaden: Springer Vieweg. S. 39–50.

Höper, Lukas/Schulte, Carsten/Benzmüller, Christoph (2024): Verantwortung. In: Furbach, Ulrich et al. (Hg.): Künstliche Intelligenz für Lehrkräfte: Eine fachliche Einführung mit didaktischen Hinweisen. Wiesbaden: Springer Vieweg. S. 219–242.

Kirchner, Daniel (2024): Computer-Verified Foundations of Metaphysics. In: Künstliche Intelligenz 38, S. 95–98.

Mühlenbeck, Cordelia/Benzmüller, Christoph (2024): On the Maximum of Positive Properties and Modal Collapse in Gödel’s Ontological Argument Compared to its Variants. In: Formal Methods and Science in Philosophy V, International Conference, Book of Abstracts. Zagreb. S. 31–32.

Parent, Xavier/Benzmüller, Christoph (2024a): Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset). In: Archive of Formal Proofs.

Parent, Xavier/Benzmüller, Christoph (2024b): Conditional normative reasoning as a fragment of HOL. In: Journal of Applied Non-Classical Logics, S. 1–32.

Solopova, Veronika et al. (2024a): Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection. In: Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics: System Demonstrations. St. Julians, Malta: Association for Computational Linguistics. S. 44–51.

Solopova, Veronika et al. (2024b): Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection. arXiv. S. 1–8.

Solopova, Veronika et al. (2024c): AI-powered automatic feedback on reflective writing. In: Annual Conference of the European Teacher Education Network (ETEN) “Teacher Education – Connecting Glocal”. Bamberg: Otto-Friedrich-Universität. S. 1–13.

Steen, Alexander/Benzmüller, Christoph (2024b): What are Non-classical Logics and Why Do We Need Them?: An Extended Interview with Dov Gabbay and Leon van der Torre. In: Künstliche Intelligenz.

Steen, Alexander/Benzmüller, Christoph (2024c): Challenges for Non-Classical Reasoning in Contemporary AI Applications. In: Künstliche Intelligenz.

Steen, Alexander/Benzmüller, Christoph (2024d): Non-Classical Reasoning for Contemporary AI Applications. In: Künstliche Intelligenz 38.

Steen, Alexander/Fuenmayor, David (2024): A formalization of abstract argumentation in higher-order logic. In: Journal of Logic and Computation 34, S. 229–260.

Steen, Alexander/Sutcliffe, Geoff/Benzmüller, Christoph (2024): Solving Quantified Modal Logic Problems by Translation to Classical Logics. arXiv.

Vestrucci, Andrea (2024): Prefazione. In: Oltre la giustizia. La difesa di una prospettiva pluralistica della vita buona. Rom: Castelvecchi. S. 5–16.

Vestrucci, Andrea/Lattanzi, Nicola (2024): Digital Sapiens: Decidere con l’intelligenza artificiale. Rom: Castelvecchi.

Baroni, Pietro/Benzmüller, Christoph/Wáng, Yì (Hg.) (2023): Journal of logic and computation. Eynsham, Oxford: Oxford University Press.

Vestrucci, Andrea (Hg.) (2023a): Beyond Babel: Religion and Linguistic Pluralism. Cham: Springer International Publishing. (= Sophia Studies in Cross-cultural Philosophy of Traditions and Cultures 43).

Benzmüller, Christoph/Otten, Jens (Hg.) (2023): CEUR Workshop Proceedings. Aachen: RWTH Aachen.

Passon, Oliver/Benzmüller, Christoph/Falkenburg, Brigitte (Hg.) (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. 1. Aufl. Heidelberg: Springer Spektrum Berlin.

Baroni, Pietro/Benzmüller, Christoph/N Wáng, Yì (2023): Preface: Special Issue on Logic and Argumentation. In: Journal of logic and computation 33, S. 189–191.

Bayer, Jonas et al. (2023): Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. In: Intelligent Computer Mathematics: 16th International Conference, CICM 2023, Cambridge, UK, , September 5–8, 2023 Proceedings. Cham: Springer Nature Switzerland. S. 69–83. (= Lecture Notes in Artificial Intelligence 14101).

Benzmüller, Christoph (2023a): Is HOL (as a metalogic) all we need for flexible normative reasoning?. In: Dagstuhl Reports. Wadern: Schloss Dagstuhl. S. 22.

Benzmüller, Christoph (2023b): Reasonable, Trusted AI through Symbolic Ethico-legal Control and Reflection? (Keynote Abstract). In: Proceedings of FLAIRS-36, May 14-17, 2023, Clearwater Beach, FL. Florida: LibraryPress@UF. (= The Florida Artificial Interlligence Research Society #PLACEHOLDER_PARENT_METADATA_VALUE#).

Benzmüller, Christoph (2023c): A Simplified Variant of Gödel’s Ontological Argument. In: Vestrucci, Andrea (Hg.): Beyond Babel: Religion and Linguistic Pluralism. 1. Aufl. Cham: Springer International Publishing. S. 271–286.

Benzmüller, Christoph et al. (2023a): Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. arXiv. S. 1–16.

Benzmüller, Christoph/Fuenmayor, David (2023): Mathematical Proof Assistants for Teaching Logic: the LogiKEy Methodology. In: Book of Abstracts: International Congress Tools for Teaching Logic V. Madrid. S. 1–3.

Benzmüller, Christoph/Reiche, Sebastian (2023): Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy. In: Journal of Logic and Computation 33, S. 1243–1269.

Benzmüller, Christoph et al. (2023b): Automated Multilingual Detection of Pro-Kremlin Propaganda in Newspapers and Telegram Posts. In: Datenbank-Spektrum 25.

Fuenmayor, David (2023): Semantical investigations on non-classical logics with recovery operators: negation. In: Logic Journal of the IGPL, S. 1–42.

Kirchner, Daniel et al. (2023): Formally Verified EVM Block-Optimizations. In: Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III. Cham: Springer Nature Switzerland. S. 176–189. (= Lecture Notes in Computer Science 13966).

Parent, Xavier/Benzmüller, Christoph (2023a): Automated Verification of Deontic Correspondences in Isabelle/HOL: First Results. In: CEUR Workshop Proceedings. Aachen, Germany: RWTH Aachen. S. 92–108.

Parent, Xavier/Benzmüller, Christoph (2023b): Normative Conditional Reasoning as a Fragment of HOL. Online: arXiv. S. 1–22.

Rothgang, Colin/Rabe, Florian/Benzmüller, Christoph (2023a): Theorem Proving in Dependently-Typed Higher-Order Logic: Extended Preprint. arXiv.

Rothgang, Colin/Rabe, Florian/Benzmüller, Christoph (2023b): Theorem Proving in Dependently-Typed Higher-Order Logic. In: Automated Deduction – CADE 29: 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings. Cham: Springer Nature Switzerland. S. 438–455. (= Lecture Notes in Computer Science 14132).

Solopova, Veronika/Benzmüller, Christoph/Landgraf, Tim (2023): The Evolution of Pro-Kremlin Propaganda From a Machine Learning and Linguistics Perspective. In: Proceedings of the Second Ukrainian Natural Language Processing Workshop (UNLP 2023). Dubrovnik. S. 40–48.

Solopova, Veronika et al. (2023a): PapagAI: Automated Feedback for Reflective Essays. arXiv. S. 1–12.

Solopova, Veronika et al. (2023b): Automated multilingual detection of Pro-Kremlin propaganda in newspapers and Telegram posts. arXiv.

Solopova, Veronika et al. (2023c): PapagAI: Automated Feedback for Reflective Essays. In: KI 2023: Advances in Artificial Intelligence: 46th German Conference on AI, Berlin, Germany, September 26–29, 2023; Proceedings. Cham: Springer. S. 198–206.

Steen, Alexander et al. (2023): Solving Modal Logic Problems by Translation to Higher-Order Logic. In: Herzig, Andreas/Luo, Jieting/Pardo, Pere (Hg.): Logic and Argumentation: 5th International Conference, CLAR 2023, Hangzhou, China, September 10-12, 2023; Proceedings. Cham: Springer Nature Switzerland. S. 25–43.

Vestrucci, Andrea (2023b): A Journey Beyond Babel. In: Vestrucci, Andrea (Hg.): Beyond Babel: Religion and Linguistic Pluralism. Cham: Springer International Publishing. S. 1–12.

Bayer, Jonas et al. (2022): Mathematical Proof Between Generations. arXiv. S. 1–17.

Benzmüller, Christoph (2022a): Studies in Computational Metaphysics: Results of an Interdisciplinary Research Project. In: Cukierman, Henrique/Bertato, Fabio (Hg.): Tópicos em História e Filosofia da Computação. Campinas, Brasilien: University of Campinas (UNICAMP). S. 129–160.

Benzmüller, Christoph (2022b): A Simplified Variant of Gödel’s Ontological Argument. In: Zygon 57, S. 953–962.

Benzmüller, Christoph (2022c): Symbolic AI and Gödel’s Ontological Argument. In: Zygon 57.

Benzmüller, Christoph/Farjami, Ali/Parent, Xavier (2022): Dyadic Deontic Logic in HOL: Faithful Embedding and Meta-Theoretical Experiments. In: Rahman, Shahid/Armgardt, Matthias/Nordtveit Kvernenes, Hans Christian (Hg.): New developments in legal reasoning and logic: from ancient law to modern legal systems. Cham: Springer. S. 353–377.

Benzmüller, Christoph et al. (2022a): Automation of Boolos’ Curious Inference in Isabelle/HOL. In: Archive of Formal Proofs.

Benzmüller, Christoph et al. (2022b): Who Finds the Short Proof?: an Exploration of Variants of Boolos’ Curious Inference using Higher-order Automated Theorem Provers. arXiv.

Fehige, Yiftach/Vestrucci, Andrea (2022): On Thought Experiments, Theology, and Mathematical Platonism. In: Axiomathes 32, S. 1–12.

Fuenmayor, David (2022): Semantical Investigations on Non-classical Logics with Recovery Operators: Negation. arXiv. S. 1–44.

Fuenmayor, David/Benzmüller, Christoph (2022): Higher-order Logic as a Lingua Franca for Logico-Pluralist Argumentation. In: Logics for New-Generation AI: Second International Workshop. 10-12 June 2022, Zhuhai. London: College Publications. S. 83–94.

Fuenmayor, David/Serrano Suárez, Fabián Fernando (2022): Formalising Basic Topology for Computational Logic in Simple Type Theory. In: Intelligent Computer Mathematics: 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022, Proceedings. Cham: Springer. S. 56–74. (= Lecture Notes in Computer Science 13467).

Kirchner, Daniel (2022a): Computer-Verified Foundations of Metaphysics and an Ontology of Natural Numbers in Isabelle/HOL. Berlin: Refubium - Repositorium der Freien Universität Berlin.

Kirchner, Daniel (2022b): Abstract Object Theory. In: Archive of Formal Proofs, S. 392.

Mucha, Henrik et al. (2022): Collaborative Speculations on Future Themes for Participatory Design in Germany. In: i-com 21, S. 283–298.

Steen, Alexander/Fuenmayor, David (2022): Bridging Between LegalRuleML and TPTP for Automated Normative Reasoning. In: Lecture Notes in Computer Science. Berlin: Springer International Publishing. S. 244–260.

Steen, Alexander et al. (2022a): Automated Reasoning in Non-classical Logics in the TPTP World. In: Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11 - 12, 2022. CEUR Workshop Proceedings.

Steen, Alexander et al. (2022b): Automated Reasoning in Non-classical Logics in the TPTP World. arXiv.

Steen, Alexander et al. (2022c): Solving QMLTP Problems by Translation to Higher-order Logic. arXiv.

Vestrucci, Andrea (2022a): Deontic-doxastic belief revision and linear system model. In: Frontiers in Psychology 13, S. 1–5.

Vestrucci, Andrea (2022b): Introduction: Five steps toward a religion-AI dialogue. In: Zygon 57, S. 933–937.

Vestrucci, Andrea (2022c): Artificial Intelligence and God´s Existence: Connecting Philosophy of Religion and Computation. In: Zygon 57, S. 1000–1018.

Vestrucci, Andrea et al. (2022): Philosophical Schools after 1950: International Conference: Warsaw, May 9-10, 2022. Warsaw: Wydział Filozofii Uniwersytetu Warszawskiego.

Benzmüller, Christoph/Fuenmayor, David (2021a): Value-Oriented Legal Argumentation in Isabelle/HOL. In: 12th International Conference on Interactive Theorem Proving (ITP 2021). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. S. 1–20. (= Leibniz International Proceedings in Informatics (LIPIcs) 193).

Benzmüller, Christoph/Fuenmayor, David (2021b): Cantor’s Theorem without Reductio Ad Absurdum. Research Gate. S. 1–3.

Benzmüller, Christoph/Reiche, Sebastian (2021): Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy. Online: arXiv. S. 1–28.

Fuenmayor, David/Benzmüller, Christoph (2020): Higher-order Logic as Lingua Franca -- Integrating Argumentative Discourse and Deep Logical Analysis. arXiv.

Wisniewski, Max et al. (2016): Effective Normalization Techniques for HOL. In: Automated Reasoning — 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016, Proceedings. Cham: Springer International Publishing. S. 362–370. (= Lecture Notes in Computer Science 9706).

Benzmüller, Christoph (1997): A calculus and a system architecture for extensional higher-order resolution. Pittsburgh, USA: Figshare. S. 1–27. (= Research Report 97-198 June,1997).

Benzmüller, Christoph (1993): HDMS-A und OBSCURE in KORSO: die Funktionale Essenz von HDMS-A aus Sicht der algorithmischen Spezifikationsmethode; Teil 3: Spezifikation der atomaren Funktionen. Universität des Saarlandes.