| 2026 | KI | Neuro-Symbolic Verification of LLM Outputs for Data-Sensitive Domains. | Paul Sigloch, Christoph Benzmller |
| 2025 | CADE | Faithful Logic Embeddings in HOL - Deep and Shallow. | Christoph Benzmller |
| 2025 | ECAI | Reasoning with Epistemic Rights and Duties: Automating a Dynamic Logic of the Right to Know in LogiKEy. | Lara Lawniczak, Luca Pasetto, Christoph Benzmller, Xu Li, Rka Markovich |
| 2025 | ICAIL | Logical Modalities within the European AI Act: An Analysis. | Lara Lawniczak, Christoph Benzmller |
| 2025 | ICLP | Visualizing Kripke Models in LogiKEy: the Case of SDL. | Luca Pasetto, Christoph Benzmller |
| 2024 | EACL | Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection. | Veronika Solopova, Viktoriia Herman, Christoph Benzmller, Tim Landgraf |
| 2023 | CADE | Theorem Proving in Dependently-Typed Higher-Order Logic. | Colin Rothgang, Florian Rabe, Christoph Benzmller |
| 2023 | KI | PapagAI: Automated Feedback for Reflective Essays. | Veronika Solopova, Eiad Rostom, Fritz Cremer, Adrian Gruszczynski, Sascha Witte, Chengming Zhang, Fernando Ramos Lpez, Lea Pll, Florian Hofmann, Ralf Romeike, Michaela Glser-Zikuda, Christoph Benzmller, Tim Landgraf |
| 2022 | CADE | Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results. | Xavier Parent, Christoph Benzmller |
| 2021 | ITP | Value-Oriented Legal Argumentation in Isabelle/HOL. | Christoph Benzmller, David Fuenmayor |
| 2020 | ECAI | Normative Reasoning with Expressive Logic Combinations. | David Fuenmayor, Christoph Benzmller |
| 2020 | ECAI | The Higher-Order Prover Leo-III. | Alexander Steen, Christoph Benzmller |
| 2020 | KI | Reasonable Machines: A Research Manifesto. | Christoph Benzmller, Bertram Lomfeld |
| 2020 | KI | Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding. | Irina Makarenko, Christoph Benzmller |
| 2020 | KR | A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gdel's Ontological Argument. | Christoph Benzmller |
| 2019 | JURIX | Modelling the US Constitution to Establish Constitutional Dictatorship. | Valeria Zahoransky, Christoph Benzmller |
| 2019 | KI | The Higher-Order Prover Leo-III (Extended Abstract). | Alexander Steen, Christoph Benzmller |
| 2019 | PRICAI | Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories. | David Fuenmayor, Christoph Benzmller |
| 2018 | CADE | The Higher-Order Prover Leo-III. | Alexander Steen, Christoph Benzmller |
| 2018 | CADE | System Demonstration: The Higher-Order Prover Leo-III. | Alexander Steen, Christoph Benzmller |
| 2018 | CiE | A Deontic Logic Reasoning Infrastructure. | Christoph Benzmller, Xavier Parent, Leendert W. N. van der Torre |
| 2017 | KI | Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic. | David Fuenmayor, Christoph Benzmller |
| 2017 | LPAR | Leo-III Version 1.1 (System description). | Christoph Benzmller, Alexander Steen, Max Wisniewski |
| 2017 | LPAR | Theorem Provers For Every Normal Modal Logic. | Tobias Gleiner, Alexander Steen, Christoph Benzmller |
| 2017 | LPAR | Going Polymorphic - TH1 Reasoning for Leo-III. | Alexander Steen, Max Wisniewski, Christoph Benzmller |
| 2017 | LPAR | Capability Discovery for Automated Reasoning Systems. | Alexander Steen, Max Wisniewski, Hans-Jrg Schurr, Christoph Benzmller |
| 2016 | CADE | TPTP and Beyond: Representation of Quantified Non-Classical Logics. | Max Wisniewski, Alexander Steen, Christoph Benzmller |
| 2016 | CADE | Effective Normalization Techniques for HOL. | Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmller |
| 2016 | ICAART | Is It Reasonable to Employ Agents in Automated Theorem Proving?. | Max Wisniewski, Christoph Benzmller |
| 2016 | IJCAI | The Inconsistency in Gdel's Ontological Argument: A Success Story for AI in Metaphysics. | Christoph Benzmller, Bruno Woltzenlogel Paleo |
| 2015 | CSR | Interacting with Modal Logics in the Coq Proof Assistant. | Christoph Benzmller, Bruno Woltzenlogel Paleo |
| 2015 | LPAR | There Is No Best \beta -Normalization Strategy for Higher-Order Reasoners. | Alexander Steen, Christoph Benzmller |
| 2015 | TABLEAUX | Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics. | Christoph Benzmller |
| 2014 | CADE | HOL Provers for First-order Modal Logics - Experiments. | Christoph Benzmller |
| 2014 | ECAI | Automating Gdel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers. | Christoph Benzmller, Bruno Woltzenlogel Paleo |
| 2013 | CADE | LEO-II Version 1.5. | Christoph Benzmller, Nik Sultana |
| 2013 | ICAART | A Top-down Approach to Combining Logics. | Christoph Benzmller |
| 2013 | LPAR | HOL Based First-Order Modal Logic Provers. | Christoph Benzmller, Thomas Raths |
| 2012 | CADE | Implementing Different Proof Calculi for First-order Modal Logics. | Christoph Benzmller, Jens Otten, Thomas Raths |
| 2012 | ECAI | Implementing and Evaluating Provers for First-order Modal Logics. | Christoph Benzmller, Jens Otten, Thomas Raths |
| 2012 | LPAR | Understanding LEO-II's proofs. | Nik Sultana, Christoph Benzmller |
| 2010 | CADE | Progress in Automating Higher-Order Ontology Reasoning. | Christoph Benzmller, Adam Pease |
| 2010 | CADE | Adaptive Assertion-Level Proofs. | Christoph Benzmller, Marvin R. G. Schiller |
| 2009 | AIED | Granularity-Adaptive Proof Presentation. | Marvin R. G. Schiller, Christoph Benzmller |
| 2009 | CADE | Progress in the Development of Automated Theorem Proving for Higher-Order Logic. | Geoff Sutcliffe, Christoph Benzmller, Chad E. Brown, Frank Theiss |
| 2009 | CSEDU | Proof Granularity as an Empirical Problem? | Marvin R. G. Schiller, Christoph Benzmller |
| 2009 | KI | Presenting Proofs with Adapted Granularity. | Marvin R. G. Schiller, Christoph Benzmller |
| 2009 | SEC | Automating Access Control Logics in Simple Type Theory with LEO-II. | Christoph Benzmller |
| 2008 | CADE | LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). | Christoph Benzmller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke |
| 2008 | CADE | THF0 - The Core of the TPTP Language for Higher-Order Logic. | Christoph Benzmller, Florian Rabe, Geoff Sutcliffe |
| 2008 | CADE | Evaluation of Systems for Higher-order Logic (ESHOL). | Christoph Benzmller, Florian Rabe, Carsten Schrmann, Geoff Sutcliffe |
| 2007 | KI | Deep Inference for Automated Proof Tutoring? | Christoph Benzmller, Dominik Dietrich, Marvin R. G. Schiller, Serge Autexier |
| 2006 | CADE | Cut-Simulation in Impredicative Logics. | Christoph Benzmller, Chad E. Brown, Michael Kohlhase |
| 2006 | KI | DiaWOz-II - A Tool for Wizard-of-Oz Experiments in Mathematics. | Christoph Benzmller, Helmut Horacek, Ivana Kruijff-Korbayov, Henri Lesourd, Marvin R. G. Schiller, Magdalena Wolska |
| 2006 | LREC | A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material. | Christoph Benzmller, Helmut Horacek, Henri Lesourd, Ivana Kruijff-Korbayov, Marvin R. G. Schiller, Magdalena Wolska |
| 2005 | AAAI | Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs. | Christoph Benzmller, Quoc Bao Vo |
| 2004 | KI | Omega: Computer Supported Mathematics. | Jrg H. Siekmann, Christoph Benzmller |
| 2004 | LPAR | Can a Higher-Order and a First-Order Theorem Prover Cooperate?. | Christoph Benzmller, Volker Sorge, Mateja Jamnik, Manfred Kerber |
| 2004 | LREC | An Annotated Corpus of Tutorial Dialogs on Mathematical Theorem Proving. | Magdalena Wolska, Quoc Bao Vo, Dimitra Tsovaltzi, Ivana Kruijff-Korbayov, Elena Karagjosova, Helmut Horacek, Armin Fiedler, Christoph Benzmller |
| 2003 | IJCAI | Assertion Application in Theorem Proving and Proof Planning. | Quoc Bao Vo, Christoph Benzmller, Serge Autexier |
| 2002 | CADE | Proof Development with OMEGA. | Jrg H. Siekmann, Christoph Benzmller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, Helmut Horacek, Michael Kohlhase, Andreas Meier, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth, Jrgen Zimmer |
| 2002 | LPAR | Proof Development with Omega-MEGA: sqrt(2) Is Irrational. | Jrg H. Siekmann, Christoph Benzmller, Armin Fiedler, Andreas Meier, Martin Pollet |
| 2001 | KI | Experiments with an Agent-Oriented Reasoning System. | Christoph Benzmller, Mateja Jamnik, Manfred Kerber, Volker Sorge |
| 1999 | CADE | Extensional Higher-Order Paramodulation and RUE-Resolution. | Christoph Benzmller |
| 1999 | EPIA | Critical Agents Supporting Interactive Theorem Proving. | Christoph Benzmller, Volker Sorge |
| 1998 | AIMSA | A Blackboard Architecture for Guiding Interactive Proofs. | Christoph Benzmller, Volker Sorge |
| 1998 | CADE | Extensional Higher-Order Resolution. | Christoph Benzmller, Michael Kohlhase |
| 1998 | CADE | System Description: LEO - A Higher-Order Theorem Prover. | Christoph Benzmller, Michael Kohlhase |
| 1997 | CADE | Omega: Towards a Mathematical Assistant. | Christoph Benzmller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt, Jrg H. Siekmann, Volker Sorge |