Omega: Towards a Mathematical Assistant. - Christoph Benzmüller; Lassaad Cheikhrouhou; Detlef Fehrer; Armin Fiedler; Xiaorong Huang; Manfred Kerber; Michael Kohlhase; Karsten Konrad; Andreas Meier 002; Erica Melis; Wolf Schaarschmidt; Jörg H. Siekmann; et al. (CADE, 1997)

A Blackboard Architecture for Guiding Interactive Proofs. - Christoph Benzmüller; Volker Sorge (AIMSA, 1998)

Extensional Higher-Order Resolution. - Christoph Benzmüller; Michael Kohlhase (CADE, 1998)

System Description: LEO - A Higher-Order Theorem Prover. - Christoph Benzmüller; Michael Kohlhase (CADE, 1998)

Extensional Higher-Order Paramodulation and RUE-Resolution. - Christoph Benzmüller (CADE, 1999)

Critical Agents Supporting Interactive Theorem Proving. - Christoph Benzmüller; Volker Sorge (EPIA, 1999)

Agent based mathematical reasoning. - Christoph Benzmüller; Mateja Jamnik; Manfred Kerber; Volker Sorge (Calculemus, 1999)

L<Omega>UI: Lovely <Omega>MEGA User Interface. - Jörg H. Siekmann; Stephan M. Hess; Christoph Benzmüller; Lassaad Cheikhrouhou; Armin Fiedler; Helmut Horacek; Michael Kohlhase; Karsten Konrad; Andreas Meier 002; Erica Melis; Martin Pollet; Volker Sorge (Formal Aspects Comput., 1999)

Integrating Tps and Omega. - Christoph Benzmüller; Matthew Bishop; Volker Sorge (J. Univers. Comput. Sci., 1999)

Equality and extensionality in automated higher order theorem proving. - Christoph Benzmüller (1999)

Resource Guided Concurrent Deduction. - Christoph Benzmüller; Mateja Jamnik; Manfred Kerber; Volker Sorge (ARW, 2000)

Experiments with an Agent-Oriented Reasoning System. - Christoph Benzmüller; Mateja Jamnik; Manfred Kerber; Volker Sorge (KI/ÖGAI, 2001)

Proof Development with OMEGA. - Jörg H. Siekmann; Christoph Benzmüller; Vladimir Brezhnev; Lassaad Cheikhrouhou; Armin Fiedler; Andreas Franke 001; Helmut Horacek; Michael Kohlhase; Andreas Meier 002; Erica Melis; Markus Moschner; Immanuel Normann; et al. (CADE, 2002)

Proof Development with Omega-MEGA: sqrt(2) Is Irrational. - Jörg H. Siekmann; Christoph Benzmüller; Armin Fiedler; Andreas Meier 002; Martin Pollet (LPAR, 2002)

Comparing Approaches To Resolution Based Higher-Order Theorem Proving. - Christoph Benzmüller (Synth., 2002)

Assertion Application in Theorem Proving and Proof Planning. - Quoc Bao Vo; Christoph Benzmüller; Serge Autexier (IJCAI, 2003)

Assertion-level Proof Representation with Under-Specification. - Serge Autexier; Christoph Benzmüller; Armin Fiedler; Helmut Horacek; Quoc Bao Vo (MKM Symposium, 2003)

Interactive Theorem Proving with Tasks. - Malte Hübner; Serge Autexier; Christoph Benzmüller; Andreas Meier 002 (UITP@TPHOLs, 2003)

Automatic Learning of Proof Methods in Proof Planning. - Mateja Jamnik; Manfred Kerber; Martin Pollet; Christoph Benzmüller (Log. J. IGPL, 2003)

Omega: Computer Supported Mathematics. - Jörg H. Siekmann; Christoph Benzmüller (KI, 2004)

Can a Higher-Order and a First-Order Theorem Prover Cooperate?. - Christoph Benzmüller; Volker Sorge; Mateja Jamnik; Manfred Kerber (LPAR, 2004)

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 Benzmüller (LREC, 2004)

Higher-order semantics and extensionality. - Christoph Benzmüller; Chad E. Brown; Michael Kohlhase (J. Symb. Log., 2004)

Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs. - Christoph Benzmüller; Quoc Bao Vo (AAAI, 2005)

Bridging Theorem Proving and Mathematical Knowledge Retrieval. - Christoph Benzmüller; Andreas Meier 002; Volker Sorge (Mechanizing Mathematical Reasoning, 2005)

Natural Language Dialog with a Tutor System for Mathematical Proofs. - Christoph Benzmüller; Helmut Horacek; Ivana Kruijff-Korbayová; Manfred Pinkal; Jörg H. Siekmann; Magdalena Wolska (Cognitive Systems, 2005)

A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity. - Serge Autexier; Christoph Benzmüller; Dominik Dietrich; Andreas Meier 002; Claus-Peter Wirth (MKM, 2005)

A Structured Set of Higher-Order Problems. - Christoph Benzmüller; Chad E. Brown (TPHOLs, 2005)

Cut-Simulation in Impredicative Logics. - Christoph Benzmüller; Chad E. Brown; Michael Kohlhase (IJCAR, 2006)

An Agent-Based Architecture for Dialogue Systems. - Mark Buckley; Christoph Benzmüller (Ershov Memorial Conference, 2006)

DiaWOz-II - A Tool for Wizard-of-Oz Experiments in Mathematics. - Christoph Benzmüller; Helmut Horacek; Ivana Kruijff-Korbayová; Henri Lesourd; Marvin R. G. Schiller; Magdalena Wolska (KI, 2006)

A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material. - Christoph Benzmüller; Helmut Horacek; Henri Lesourd; Ivana Kruijff-Korbayová; Marvin R. G. Schiller; Magdalena Wolska (LREC, 2006)

Omega. - Christoph Benzmüller; Armin Fiedler; Andreas Meier 002; Martin Pollet; Jörg H. Siekmann (The Seventeen Provers of the World, 2006)

LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL) - Christoph Benzmüller; John Harrison 001; Carsten Schürmann (CoRR, 2006)

PlatOmega: A Mediator between Text-Editors and Proof Assistance Systems. - Marc Wagner 001; Serge Autexier; Christoph Benzmüller (UITP@FLoC, 2006)

Towards computer aided mathematics. - Christoph Benzmüller (J. Appl. Log., 2006)

Computer supported mathematics with Omegamega. - Jörg H. Siekmann; Christoph Benzmüller; Serge Autexier (J. Appl. Log., 2006)

Deep Inference for Automated Proof Tutoring? - Christoph Benzmüller; Dominik Dietrich; Marvin R. G. Schiller; Serge Autexier (KI, 2007)

LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). - Christoph Benzmüller; Lawrence C. Paulson; Frank Theiss; Arnaud Fietzke (IJCAR, 2008)

THF0 - The Core of the TPTP Language for Higher-Order Logic. - Christoph Benzmüller; Florian Rabe 001; Geoff Sutcliffe (IJCAR, 2008)

Evaluation of Systems for Higher-order Logic (ESHOL). - Christoph Benzmüller; Florian Rabe 001; Carsten Schürmann; Geoff Sutcliffe (PAAR/ESHOL, 2008)

Preface. - Serge Autexier; Christoph Benzmüller (UITP@TPHOLs, 2008)

Combined reasoning by automated cooperation. - Christoph Benzmüller; Volker Sorge; Mateja Jamnik; Manfred Kerber (J. Appl. Log., 2008)

Organization, Transformation, and Propagation of Mathematical Knowledge in Omegamega. - Serge Autexier; Christoph Benzmüller; Dominik Dietrich; Marc Wagner 001 (Math. Comput. Sci., 2008)

Granularity-Adaptive Proof Presentation. - Marvin R. G. Schiller; Christoph Benzmüller (AIED, 2009)

Progress in the Development of Automated Theorem Proving for Higher-Order Logic. - Geoff Sutcliffe; Christoph Benzmüller; Chad E. Brown; Frank Theiss (CADE, 2009)

Proof Granularity as an Empirical Problem? - Marvin R. G. Schiller; Christoph Benzmüller (CSEDU (1), 2009)

Presenting Proofs with Adapted Granularity. - Marvin R. G. Schiller; Christoph Benzmüller (KI, 2009)

Automating Access Control Logics in Simple Type Theory with LEO-II. - Christoph Benzmüller (SEC, 2009)

Automating Access Control Logics in Simple Type Theory with LEO-II (Techreport) - Christoph Benzmüller (CoRR, 2009)

Resource Adaptive Agents in Interactive Theorem Proving - Christoph Benzmüller; Volker Sorge (CoRR, 2009)

A remark on higher order RUE-resolution with EXTRUE - Christoph Benzmüller (CoRR, 2009)

Cut-Simulation and Impredicativity - Christoph Benzmüller; Chad E. Brown; Michael Kohlhase (Log. Methods Comput. Sci., 2009)

Lectures on Jacques Herbrand as a Logician - Claus-Peter Wirth; Jörg H. Siekmann; Christoph Benzmüller; Serge Autexier (CoRR, 2009)

Automating Quantified Multimodal Logics in Simple Type Theory – A Case Study - Christoph Benzmueller (CoRR, 2009)

Jacques Herbrand: Life, Logic, and Automated Deduction. - Claus-Peter Wirth; Jörg H. Siekmann; Christoph Benzmüller; Serge Autexier (Logic from Russell to Church, 2009)

Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners). - Christoph Benzmüller (Verification, Induction, Termination Analysis, 2010)

Progress in Automating Higher-Order Ontology Reasoning. - Christoph Benzmüller; Adam Pease (PAAR@IJCAR, 2010)

Adaptive Assertion-Level Proofs. - Christoph Benzmüller; Marvin R. G. Schiller (EMSQMS@IJCAR, 2010)

Combining Logics in Simple Type Theory. - Christoph Benzmüller (CLIMA, 2010)

Simple Type Theory as Framework for Combining Logics. - Christoph Benzmueller (CoRR, 2010)

Multimodal and intuitionistic logics in simple type theory. - Christoph Benzmüller; Lawrence C. Paulson (Log. J. IGPL, 2010)

Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. - Geoff Sutcliffe; Christoph Benzmüller (J. Formaliz. Reason., 2010)

Combining and automating classical and non-classical logics in classical higher-order logics. - Christoph Benzmüller (Ann. Math. Artif. Intell., 2011)

ΩMEGA: Resource-Adaptive Processes in an Automated Reasoning System. - Serge Autexier; Christoph Benzmüller; Dominik Dietrich; Jörg H. Siekmann (Resource-Adaptive Cognitive Processes, 2011)

Resource-Bounded Modelling and Analysis of Human-Level Interactive Proofs. - Christoph Benzmüller; Marvin R. G. Schiller; Jörg H. Siekmann (Resource-Adaptive Cognitive Processes, 2011)

Implementing Different Proof Calculi for First-order Modal Logics. - Christoph Benzmüller; Jens Otten; Thomas Raths (PAAR@IJCAR, 2012)

Implementing and Evaluating Provers for First-order Modal Logics. - Christoph Benzmüller; Jens Otten; Thomas Raths (ECAI, 2012)

Understanding LEO-II's proofs. - Nik Sultana; Christoph Benzmüller (IWIL@LPAR, 2012)

Embedding and automating conditional logics in classical higher-order logic. - Christoph Benzmüller; Dov M. Gabbay; Valerio Genovese; Daniele Rispoli (Ann. Math. Artif. Intell., 2012)

Quantified Conditional Logics are Fragments of HOL - Christoph Benzmueller; Valerio Genovese (CoRR, 2012)

FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends - Christoph Benzmueller; Thomas Raths (CoRR, 2012)

Higher-order aspects and context in SUMO. - Christoph Benzmüller; Adam Pease (J. Web Semant., 2012)

LEO-II Version 1.5. - Christoph Benzmüller; Nik Sultana (PxTP@CADE, 2013)

A Top-down Approach to Combining Logics. - Christoph Benzmüller (ICAART (2), 2013)

Automating Quantified Conditional Logics in HOL. - Christoph Benzmueller (IJCAI, 2013)

HOL Based First-Order Modal Logic Provers. - Christoph Benzmüller; Thomas Raths (LPAR, 2013)

Gödel's God in Isabelle/HOL. - Christoph Benzmueller; Bruno Woltzenlogel Paleo (Arch. Formal Proofs, 2013)

Sigma: An integrated development environment for formal ontology. - Adam Pease; Christoph Benzmüller (AI Commun., 2013)

Formalization, Mechanization and Automation of Gödel's Proof of God's Existence. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (CoRR, 2013)

Update report: LEO-II version 1.5 - Christoph Benzmüller; Nik Sultana (CoRR, 2013)

Quantified Multimodal Logics in Simple Type Theory. - Christoph Benzmüller; Lawrence C. Paulson (Logica Universalis, 2013)

HOL Provers for First-order Modal Logics - Experiments. - Christoph Benzmüller (ARQNL@IJCAR, 2014)

Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (ECAI, 2014)

On Logic Embeddings and Gödel's God. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (WADT, 2014)

Automation of Higher-Order Logic. - Christoph Benzmüller; Dale Miller 001 (Computational Logic, 2014)

Interacting with Modal Logics in the Coq Proof Assistant. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (CSR, 2015)

Proofs and Reconstructions. - Nik Sultana; Christoph Benzmüller; Lawrence C. Paulson (FroCos, 2015)

There Is No Best beta -Normalization Strategy for Higher-Order Reasoners. - Alexander Steen; Christoph Benzmüller (LPAR, 2015)

LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners. - Max Wisniewski; Alexander Steen; Christoph Benzmüller (CICM, 2015)

Higher-Order Modal Logics: Automation and Applications. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (Reasoning Web, 2015)

Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics. - Christoph Benzmüller (TABLEAUX, 2015)

Systematic Verification of the Modal Logic Cube in Isabelle/HOL. - Christoph Benzmüller; Maximilian Claus; Nik Sultana (PxTP@CADE, 2015)

The Higher-Order Prover Leo-II. - Christoph Benzmüller; Nik Sultana; Lawrence C. Paulson; Frank Theiss (J. Autom. Reason., 2015)

TPTP and Beyond: Representation of Quantified Non-Classical Logics. - Max Wisniewski; Alexander Steen; Christoph Benzmüller (ARQNL@IJCAR, 2016)

Effective Normalization Techniques for HOL. - Max Wisniewski; Alexander Steen; Kim Kern; Christoph Benzmüller (IJCAR, 2016)

Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL. - Alexander Steen; Max Wisniewski; Christoph Benzmüller (GCAI, 2016)

Is It Reasonable to Employ Agents in Automated Theorem Proving?. - Max Wisniewski; Christoph Benzmüller (ICAART (1), 2016)

Automating Free Logic in Isabelle/HOL. - Christoph Benzmüller; Dana S. Scott (ICMS, 2016)

Agent-Based HOL Reasoning. - Alexander Steen; Max Wisniewski; Christoph Benzmüller (ICMS, 2016)

The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics. - Christoph Benzmüller; Bruno Woltzenlogel Paleo (IJCAI, 2016)

Translating Higher-Order Modal Logic from RuleML to TPTP. - Harold Boley; Christoph Benzmüller; Meng Luan; Zhendong Sha (RuleML (Supplement), 2016)

Einsatz von Theorembeweisern in der Lehre. - Alexander Steen; Max Wisniewski; Christoph Benzmüller (HDI, 2016)

Axiomatizing Category Theory in Free Logic. - Christoph Benzmüller; Dana S. Scott (CoRR, 2016)

Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic. - David Fuenmayor; Christoph Benzmüller (KI, 2017)

Leo-III Version 1.1 (System description). - Christoph Benzmüller; Alexander Steen; Max Wisniewski (LPAR (Short Presentations), 2017)

Theorem Provers For Every Normal Modal Logic. - Tobias Gleißner; Alexander Steen; Christoph Benzmüller (LPAR, 2017)

Going Polymorphic - TH1 Reasoning for Leo-III. - Alexander Steen; Max Wisniewski; Christoph Benzmüller (IWIL@LPAR, 2017)

Capability Discovery for Automated Reasoning Systems. - Alexander Steen; Max Wisniewski; Hans-Jörg Schurr; Christoph Benzmüller (IWIL@LPAR, 2017)

Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract). - Christoph Benzmüller (SBMF, 2017)

Types, Tableaus and Gödel's God in Isabelle/HOL. - David Fuenmayor; Christoph Benzmüller (Arch. Formal Proofs, 2017)

Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument. - David Fuenmayor; Christoph Benzmüller (Arch. Formal Proofs, 2017)

Universal Reasoning, Rational Argumentation and Human-Machine Interaction. - Christoph Benzmüller (CoRR, 2017)

Cut-Elimination for Quantified Conditional Logic. - Christoph Benzmüller (J. Philos. Log., 2017)

Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy. - Christoph Benzmüller; L. Weber; Bruno Woltzenlogel Paleo (Logica Universalis, 2017)

System Demonstration: The Higher-Order Prover Leo-III. - Alexander Steen; Christoph Benzmüller (ARQNL@IJCAR, 2018)

A Deontic Logic Reasoning Infrastructure. - Christoph Benzmüller; Xavier Parent 001; Leendert W. N. van der Torre (CiE, 2018)

Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments. - David Fuenmayor; Christoph Benzmüller (CLAR, 2018)

A Dyadic Deontic Logic in HOL. - Christoph Benzmüller; Ali Farjami; Xavier Parent 001 (DEON, 2018)

Axiom Systems for Category Theory in Free Logic. - Christoph Benzmüller; Dana S. Scott (Arch. Formal Proofs, 2018)

Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL. - David Fuenmayor; Christoph Benzmüller (Arch. Formal Proofs, 2018)

Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL. - Christoph Benzmüller; Ali Farjami; Xavier Parent 001 (CoRR, 2018)

I/O Logic in HOL - First Steps. - Christoph Benzmüller; Xavier Parent 001 (CoRR, 2018)

First Experiments with a Flexible Infrastructure for Normative Reasoning. - Christoph Benzmüller; Xavier Parent 001 (CoRR, 2018)

Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations. - David Fuenmayor; Christoph Benzmüller (FroCos, 2019)

Modelling the US Constitution to Establish Constitutional Dictatorship. - Valeria Zahoransky; Christoph Benzmüller (MIREL@JURIX, 2019)

The Higher-Order Prover Leo-III (Extended Abstract). - Alexander Steen; Christoph Benzmüller (KI, 2019)

Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories. - David Fuenmayor; Christoph Benzmüller (PRICAI (1), 2019)

Report on the Second International Joint Conference on Rules and Reasoning. - Christoph Benzmüller; Xavier Parent 001; Francesco Ricca (AI Mag., 2019)

Designing Normative Theories of Ethical Reasoning: Formal Framework, Methodology, and Tool Support. - Christoph Benzmüller; Xavier Parent 001; Leendert W. N. van der Torre (CoRR, 2019)

Computer Science and Metaphysics: A Cross-Fertilization. - Daniel Kirchner; Christoph Benzmüller; Edward N. Zalta (CoRR, 2019)

A Computational-Hermeneutic Approach for Conceptual Explicitation. - David Fuenmayor; Christoph Benzmüller (CoRR, 2019)

Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument. - Christoph Benzmüller; David Fuenmayor (CoRR, 2019)

I/O Logic in HOL. - Christoph Benzmüller; Ali Farjami; Paul Meder; Xavier Parent 001 (FLAP, 2019)

åqvist's Dyadic Deontic Logic E in HOL. - Christoph Benzmüller; Ali Farjami; Xavier Parent 001 (FLAP, 2019)

Universal (meta-)logical reasoning: Recent successes. - Christoph Benzmüller (Sci. Comput. Program., 2019)

Computer-Supported Exploration of a Categorical Axiomatization of Modeloids. - Lucca Tiemens; Dana S. Scott; Christoph Benzmüller; Miroslav Benda (RAMiCS, 2020)

Computer-Supported Analysis of Arguments in Climate Engineering. - David Fuenmayor; Christoph Benzmüller (CLAR, 2020)

Public Announcement Logic in HOL. - Sebastian Reiche; Christoph Benzmüller (DaLí, 2020)

Normative Reasoning with Expressive Logic Combinations. - David Fuenmayor; Christoph Benzmüller (ECAI, 2020)

The Higher-Order Prover Leo-III. - Alexander Steen; Christoph Benzmüller (ECAI, 2020)

Reasonable Machines: A Research Manifesto. - Christoph Benzmüller; Bertram Lomfeld (KI, 2020)

Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding. - Irina Makarenko; Christoph Benzmüller (KI, 2020)

A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument. - Christoph Benzmüller (KR, 2020)

Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. - Christoph Benzmüller; Xavier Parent 001; Leendert W. N. van der Torre (Artif. Intell., 2020)

A (Simplified) Supreme Being Necessarily Exists - Says the Computer! - Christoph Benzmüller (CoRR, 2020)

On Reductions of Hintikka Sets for Higher-Order Logic. - Alexander Steen; Christoph Benzmüller (CoRR, 2020)

Encoding Legal Balancing: Automating an Abstract Ethico-Legal Value Ontology in Preference Logic. - Christoph Benzmüller; David Fuenmayor; Bertram Lomfeld (CoRR, 2020)

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

Automating Free Logic in HOL, with an Experimental Application in Category Theory. - Christoph Benzmüller; Dana S. Scott (J. Autom. Reason., 2020)

Mechanizing Principia Logico-Metaphysica in Functional Type-Theory. - Daniel Kirchner; Christoph Benzmüller; Edward N. Zalta (Rev. Symb. Log., 2020)

Leo-III 1.5 - A Theorem Prover for Higher-Order Logic. - Alexander Steen; Christoph Benzmueller (Zenodo, 2020)

A German Corpus of Reflective Sentences. - Veronika Solopova; Oana-Iuliana Popescu; Margarita Chikobava; Ralf Romeike; Tim Landgraf; Christoph Benzmüller (ICON, 2021)

Value-Oriented Legal Argumentation in Isabelle/HOL. - Christoph Benzmüller; David Fuenmayor (ITP, 2021)

Exploring Simplified Variants of Gödel's Ontological Argument in Isabelle/HOL. - Christoph Benzmüller (Arch. Formal Proofs, 2021)

Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL. - Christoph Benzmüller; Sebastian Reiche (Arch. Formal Proofs, 2021)

Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy. - Christoph Benzmüller; Sebastian Reiche (CoRR, 2021)

Extensional Higher-Order Paramodulation in Leo-III. - Alexander Steen; Christoph Benzmüller (J. Autom. Reason., 2021)

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). - Christoph Benzmüller; Xavier Parent 001; Francesco Ricca (Theory Pract. Log. Program., 2021)

Leo-III - A Theorem Prover for Higher-Order Logic. - Alexander Steen; Christoph Benzmueller (Zenodo, 2021)

Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results. - Xavier Parent 001; Christoph Benzmüller (ARQNL@IJCAR, 2022)

Automated Reasoning in Non-classical Logics in the TPTP World. - Alexander Steen; David Fuenmayor; Tobias Gleißner; Geoff Sutcliffe; Christoph Benzmüller (PAAR@IJCAR, 2022)

Automation of Boolos' Curious Inference in Isabelle/HOL. - Christoph Benzmüller; David Fuenmayor; Alexander Steen; Geoff Sutcliffe (Arch. Formal Proofs, 2022)

A Simplified Variant of Gödel's Ontological Argument. - Christoph Benzmüller (CoRR, 2022)

Mathematical Proof Between Generations. - Jonas Bayer; Christoph Benzmüller; Kevin Buzzard; Marco David; Leslie Lamport; Yuri V. Matiyasevich; Lawrence C. Paulson; Dierk Schleicher; Benedikt Stock; Efim I. Zelmanov (CoRR, 2022)

Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers. - Christoph Benzmüller; David Fuenmayor; Alexander Steen; Geoff Sutcliffe (CoRR, 2022)

Solving QMLTP Problems by Translation to Higher-order Logic. - Alexander Steen; Geoff Sutcliffe; Tobias Gleißner; Christoph Benzmüller (CoRR, 2022)

Collaborative Speculations on Future Themes for Participatory Design in Germany. - Henrik Mucha; Ana Correia de Barros; Jesse Josua Benjamin; Christoph Benzmüller; Andreas Bischof; Sandra Buchmüller; Alexandra de Carvalho; Anna-Katharina Dhungel; Claude Draude; Marc-Julian Fleck; Juliane Jarke; Stefanie Klein; et al. (i-com, 2022)

Theorem Proving in Dependently-Typed Higher-Order Logic. - Colin Rothgang; Florian Rabe 001; Christoph Benzmüller (CADE, 2023)

Solving Modal Logic Problems by Translation to Higher-Order Logic. - Alexander Steen; Geoff Sutcliffe; Tobias Scholl; Christoph Benzmüller (CLAR, 2023)

PapagAI: Automated Feedback for Reflective Essays. - Veronika Solopova; Eiad Rostom; Fritz Cremer; Adrian Gruszczynski; Sascha Witte; Chengming Zhang; Fernando Ramos López; Lea Plößl; Florian Hofmann; Ralf Romeike; Michaela Gläser-Zikuda; Christoph Benzmüller; et al. (KI, 2023)

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. - Jonas Bayer; Alexey Gonus; Christoph Benzmüller; Dana S. Scott (CICM, 2023)

Theorem Proving in Dependently-Typed Higher-Order Logic - Extended Preprint. - Colin Rothgang; Florian Rabe 001; Christoph Benzmüller (CoRR, 2023)

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. - Jonas Bayer; Aleksey Gonus; Christoph Benzmüller; Dana S. Scott (CoRR, 2023)

Normative Conditional Reasoning as a Fragment of HOL. - Xavier Parent 001; Christoph Benzmüller (CoRR, 2023)

Automated Multilingual Detection of Pro-Kremlin Propaganda in Newspapers and Telegram Posts. - Veronika Solopova; Oana-Iuliana Popescu; Christoph Benzmüller; Tim Landgraf (Datenbank-Spektrum, 2023)

Preface: Special Issue on Logic and Argumentation. - Pietro Baroni; Christoph Benzmüller; Yì N. Wáng (J. Log. Comput., 2023)

Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy. - Christoph Benzmüller; Sebastian Reiche (J. Log. Comput., 2023)

Logikbasierte Wissensverarbeitung. - Christoph Benzmüller (Künstliche Intelligenz für Lehrkräfte, 2024)

Schließen aus Wissen. - Ulrich Furbach; Christoph Benzmüller (Künstliche Intelligenz für Lehrkräfte, 2024)

Verantwortung. - Lukas Höper; Carsten Schulte 001; Christoph Benzmüller (Künstliche Intelligenz für Lehrkräfte, 2024)

Implementing the Fatio Protocol for Multi-Agent Argumentation in LogiKEy. - Luca Pasetto; Christoph Benzmüller (ARQNL@IJCAR, 2024)

Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection. - Veronika Solopova; Viktoriia Herman; Christoph Benzmüller; Tim Landgraf (EACL (Demonstrations), 2024)

Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset). - Xavier Parent 001; Christoph Benzmüller (Arch. Formal Proofs, 2024)

Script-Based Dialog Policy Planning for LLM-Powered Conversational Agents: A Basic Architecture for an "AI Therapist". - Robert Wasenmüller; Kevin Hilbert; Christoph Benzmüller (CoRR, 2024)

Who finds the short proof? - Christoph Benzmüller; David Fuenmayor; Alexander Steen; Geoff Sutcliffe (Log. J. IGPL, 2024)

Supplemental material to "Solving Quantified Modal Logic Problems by Translation to Classical Logics". - Alexander Steen; Geoff Sutcliffe; Christoph Benzmüller (Zenodo, 2024)

Non-Classical Reasoning for Contemporary AI Applications. - Alexander Steen; Christoph Benzmüller (Künstliche Intell., 2024)

Challenges for Non-Classical Reasoning in Contemporary AI Applications. - Alexander Steen; Christoph Benzmüller (Künstliche Intell., 2024)

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

Conditional normative reasoning as a fragment of HOL. - Xavier Parent 001; Christoph Benzmüller (J. Appl. Non Class. Logics, 2024)

Faithful Logic Embeddings in HOL - Deep and Shallow. - Christoph Benzmüller (CADE, 2025)

Faithful Logic Embeddings in HOL - Deep and Shallow (Isabelle/HOL dataset). - Christoph Benzmüller (Arch. Formal Proofs, 2025)

Notes on Gödel's and Scott's Variants of the Ontological Argument (Isabelle/HOL dataset). - Christoph Benzmüller; Dana S. Scott (Arch. Formal Proofs, 2025)

Logical Modalities within the European AI Act: An Analysis. - Lara Lawniczak; Christoph Benzmüller (CoRR, 2025)

Faithful Logic Embeddings in HOL - A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level. - Christoph Benzmüller (CoRR, 2025)