Chair for AI Systems Engineering

AI Systems Engineering (AISE)

The research activities of the AISE Chair lie at the intersection of artificial intelligence, philosophy, mathematics, computer science, and natural language. Current research of the team focuses on mechanization of formal reasoning and explanation in computers to develop trustworthy AI systems. A particular interest is the use of higher-order classical logic (HOL) as a universal meta-logic to automate various non-classical logics and use them in current applications, including machine ethics and machine law, metaphysics (e.g., Gödel's ontological argument), mathematical foundations (e.g., category theory), and rational argumentation. However, the research activities of the AISE team are broader, and also address, for example, the integration of automated reasoning, machine learning, and agent-based architectures. Prof. Dr. Benzmüller's core competencies are in the area of classical higher level logic (HOL), whose semantics and proof theory he has contributed to. Together with colleagues and students, he has also developed the Leo theorem provers for HOL.


AISE Science Communication

At the Science Slam of the University of Bamberg on October 27, Benzmüller presented central hypotheses of the AISE research landscape to a wider audience. Together with the rapper ,,Bambägga'' from Bamberg, Benzmüller won this Science Slam. Previously, Benzmüller had also very successfully contested other slams, e.g. in front of the roten Rathaus in Berlin and in the well-known Berliner Club SO3.

Aktuelle Publikationen des AISE Lehrstuhls (Auswahl seit 2022)

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

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.

Benzmüller, Christoph (2023): Reasonable, Trusted AI through Symbolic Ethico-legal Control and Reflection? (Keynote Abstract). In: The Florida Artificial Interlligence Research Society. Florida: LibraryPress@UF.

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 et al. (2023b): Who Finds the Short Proof?. In: Logic journal of the IGPL, S. 1–23.

Benzmüller, Christoph et al. (2023c): 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.

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.

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/Fuenmayor, David (2023): A formalization of abstract argumentation in higher-order logic. In: Journal of Logic and Computation, S. 1–32.

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.

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): Who Finds the Short Proof?: an Exploration of Variants of Boolos’ Curious Inference using Higher-order Automated Theorem Provers. arXiv.

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

Benzmüller, Christoph/Reiche, Sebastian (2022): 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.

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.

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 et al. (2022a): Automated Reasoning in Non-classical Logics in the TPTP World. arXiv.

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

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

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

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

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

Benzmüller, Christoph/Fuenmayor, David (2021): 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.

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.