Christoph Benzmüller

223 papers A* 4A 19B 10C 6Misc 14Journal 92Unranked 54
YearRankTypeTitle / Venue / Authors
2026 — ch.
Symbolische Kontrolle für subsymbolische Künstliche Intelligenz?
Künstliche Intelligenz und Wir: Stand, Nutzung und Herausforderungen der KI
Christoph Benzmüller
2025 J jnl
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.
CoRR
Christoph Benzmüller
2025 J jnl
Faithful Logic Embeddings in HOL - Deep and Shallow (Isabelle/HOL dataset).
Arch. Formal Proofs
Christoph Benzmüller
2025 A conf
Faithful Logic Embeddings in HOL - Deep and Shallow.
CADE
Christoph Benzmüller
2025 C conf
Logical Modalities within the European AI Act: An Analysis.
ICAIL
Lara Lawniczak, Christoph Benzmüller
2025 J jnl
Logical Modalities within the European AI Act: An Analysis.
CoRR
Lara Lawniczak, Christoph Benzmüller
2025 J jnl
Notes on Gödel's and Scott's Variants of the Ontological Argument (Isabelle/HOL dataset).
Arch. Formal Proofs
Christoph Benzmüller, Dana S. Scott
2025 A conf
Reasoning with Epistemic Rights and Duties: Automating a Dynamic Logic of the Right to Know in LogiKEy.
ECAI
Lara Lawniczak, Luca Pasetto, Christoph Benzmüller, Xu Li, Réka Markovich
2025 — conf
Visualizing Kripke Models in LogiKEy: the Case of SDL.
ICLP Workshops
Luca Pasetto, Christoph Benzmüller
2024 — ed.
Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I
IJCAR (1)
Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt
2024 — ed.
Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II
IJCAR (2)
Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt
2024 J jnl
Challenges for Non-Classical Reasoning in Contemporary AI Applications.
Künstliche Intell.
Alexander Steen, Christoph Benzmüller
2024 — conf
Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection.
EACL (Demonstrations)
Veronika Solopova, Viktoriia Herman, Christoph Benzmüller, Tim Landgraf
2024 J jnl
Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection.
CoRR
Veronika Solopova, Viktoriia Herman, Christoph Benzmüller, Tim Landgraf
2024 J jnl
Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset).
Arch. Formal Proofs
Xavier Parent, Christoph Benzmüller
2024 J jnl
Conditional normative reasoning as a fragment of HOL.
J. Appl. Non Class. Logics
Xavier Parent, Christoph Benzmüller
2024 — conf
Implementing the Fatio Protocol for Multi-Agent Argumentation in LogiKEy.
ARQNL@IJCAR
Luca Pasetto, Christoph Benzmüller
2024 — ch.
Logikbasierte Wissensverarbeitung.
Künstliche Intelligenz für Lehrkräfte
Christoph Benzmüller
2024 J jnl
Non-Classical Reasoning for Contemporary AI Applications.
Künstliche Intell.
Alexander Steen, Christoph Benzmüller
2024 — ed.
Proceedings of the 5th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2024) affiliated with the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Nancy, France, July 1, 2024.
ARQNL@IJCAR
Christoph Benzmüller, Jens Otten, Revantha Ramanayake
2024 — ch.
Schließen aus Wissen.
Künstliche Intelligenz für Lehrkräfte
Ulrich Furbach, Christoph Benzmüller
2024 J jnl
Script-Based Dialog Policy Planning for LLM-Powered Conversational Agents: A Basic Architecture for an "AI Therapist".
CoRR
Robert Wasenmüller, Kevin Hilbert, Christoph Benzmüller
2024 — ch.
Verantwortung.
Künstliche Intelligenz für Lehrkräfte
Lukas Höper, Carsten Schulte, Christoph Benzmüller
2024 J jnl
What are Non-classical Logics and Why Do We Need Them? An Extended Interview with Dov Gabbay and Leon van der Torre.
Künstliche Intell.
Alexander Steen, Christoph Benzmüller
2024 J jnl
Who finds the short proof?
Log. J. IGPL
Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe
2023 J jnl
Automated Multilingual Detection of Pro-Kremlin Propaganda in Newspapers and Telegram Posts.
Datenbank-Spektrum
Veronika Solopova, Oana-Iuliana Popescu, Christoph Benzmüller, Tim Landgraf
2023 J jnl
Automated multilingual detection of Pro-Kremlin propaganda in newspapers and Telegram posts.
CoRR
Veronika Solopova, Oana-Iuliana Popescu, Christoph Benzmüller, Tim Landgraf
2023 J jnl
Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy.
J. Log. Comput.
Christoph Benzmüller, Sebastian Reiche
2023 C conf
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation.
CICM
Jonas Bayer, Alexey Gonus, Christoph Benzmüller, Dana S. Scott
2023 J jnl
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation.
CoRR
Jonas Bayer, Aleksey Gonus, Christoph Benzmüller, Dana S. Scott
2023 J jnl
Normative Conditional Reasoning as a Fragment of HOL.
CoRR
Xavier Parent, Christoph Benzmüller
2023 Misc conf
PapagAI: Automated Feedback for Reflective Essays.
KI
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, Tim Landgraf
2023 J jnl
PapagAI: Automated Feedback for Reflective Essays.
CoRR
Veronika Solopova, Adrian Gruszczynski, Eiad Rostom, Fritz Cremer, Sascha Witte, Chengming Zhang, Fernando Ramos López, Lea Plößl, Florian Hofmann, Ralf Romeike, Michaela Gläser-Zikuda, Christoph Benzmüller, Tim Landgraf
2023 J jnl
Preface: Special Issue on Logic and Argumentation.
J. Log. Comput.
Pietro Baroni, Christoph Benzmüller, Yì N. Wáng
2023 — ed.
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), Haifa, Israel, August 11, 2022.
ARQNL@IJCAR
Christoph Benzmüller, Jens Otten
2023 — conf
Solving Modal Logic Problems by Translation to Higher-Order Logic.
CLAR
Alexander Steen, Geoff Sutcliffe, Tobias Scholl, Christoph Benzmüller
2023 J jnl
Theorem Proving in Dependently-Typed Higher-Order Logic - Extended Preprint.
CoRR
Colin Rothgang, Florian Rabe, Christoph Benzmüller
2023 A conf
Theorem Proving in Dependently-Typed Higher-Order Logic.
CADE
Colin Rothgang, Florian Rabe, Christoph Benzmüller
2022 J jnl
A Simplified Variant of Gödel's Ontological Argument.
CoRR
Christoph Benzmüller
2022 — conf
Automated Reasoning in Non-classical Logics in the TPTP World.
PAAR@IJCAR
Alexander Steen, David Fuenmayor, Tobias Gleißner, Geoff Sutcliffe, Christoph Benzmüller
2022 J jnl
Automated Reasoning in Non-classical Logics in the TPTP World.
CoRR
Alexander Steen, David Fuenmayor, Tobias Gleißner, Geoff Sutcliffe, Christoph Benzmüller
2022 — conf
Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results.
ARQNL@IJCAR
Xavier Parent, Christoph Benzmüller
2022 J jnl
Automation of Boolos' Curious Inference in Isabelle/HOL.
Arch. Formal Proofs
Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe
2022 J jnl
Collaborative Speculations on Future Themes for Participatory Design in Germany.
i-com
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, Caroline Kortekaas, Albrecht Kurze, Diane Linke, Franzisca Maas, Nicola Marsden, Ricardo Melo, Susanne Michel, Claudia Müller-Birn, Monika Pröbster, Katja Antonia Rießenberger, Mirko Tobias Schäfer, Peter Sörries, Julia Stilke, Torben Volkmann, Anne Weibert, Wilhelm Weinhold, Sara Wolf, Isabel Zorn, Michael Heidt, Arne Berger
2022 J jnl
Mathematical Proof Between Generations.
CoRR
Jonas Bayer, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lamport, Yuri V. Matiyasevich, Lawrence C. Paulson, Dierk Schleicher, Benedikt Stock, Efim I. Zelmanov
2022 J jnl
Solving QMLTP Problems by Translation to Higher-order Logic.
CoRR
Alexander Steen, Geoff Sutcliffe, Tobias Gleißner, Christoph Benzmüller
2022 J jnl
Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers.
CoRR
Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe
2021 — conf
A German Corpus of Reflective Sentences.
ICON
Veronika Solopova, Oana-Iuliana Popescu, Margarita Chikobava, Ralf Romeike, Tim Landgraf, Christoph Benzmüller
2021 J jnl
Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL.
Arch. Formal Proofs
Christoph Benzmüller, Sebastian Reiche
2021 J jnl
Exploring Simplified Variants of Gödel's Ontological Argument in Isabelle/HOL.
Arch. Formal Proofs
Christoph Benzmüller
2021 J jnl
Extensional Higher-Order Paramodulation in Leo-III.
J. Autom. Reason.
Alexander Steen, Christoph Benzmüller
2021 J jnl
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 Pract. Log. Program.
Christoph Benzmüller, Xavier Parent, Francesco Ricca
2021 — ed.
Logic and Argumentation - 4th International Conference, CLAR 2021, Hangzhou, China, October 20-22, 2021, Proceedings
CLAR
Pietro Baroni, Christoph Benzmüller, Yì N. Wáng
2021 J jnl
Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy.
CoRR
Christoph Benzmüller, Sebastian Reiche
2021 B conf
Value-Oriented Legal Argumentation in Isabelle/HOL.
ITP
Christoph Benzmüller, David Fuenmayor
2020 J jnl
A (Simplified) Supreme Being Necessarily Exists - Says the Computer!
CoRR
Christoph Benzmüller
2020 A* conf
A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument.
KR
Christoph Benzmüller
2020 J jnl
Automating Free Logic in HOL, with an Experimental Application in Category Theory.
J. Autom. Reason.
Christoph Benzmüller, Dana S. Scott
2020 — conf
Computer-Supported Analysis of Arguments in Climate Engineering.
CLAR
David Fuenmayor, Christoph Benzmüller
2020 C conf
Computer-Supported Exploration of a Categorical Axiomatization of Modeloids.
RAMiCS
Lucca Tiemens, Dana S. Scott, Christoph Benzmüller, Miroslav Benda
2020 J jnl
Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support.
Artif. Intell.
Christoph Benzmüller, Xavier Parent, Leendert W. N. van der Torre
2020 J jnl
Encoding Legal Balancing: Automating an Abstract Ethico-Legal Value Ontology in Preference Logic.
CoRR
Christoph Benzmüller, David Fuenmayor, Bertram Lomfeld
2020 J jnl
Higher-order Logic as Lingua Franca - Integrating Argumentative Discourse and Deep Logical Analysis.
CoRR
David Fuenmayor, Christoph Benzmüller
2020 C ed.
Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings
CICM
Christoph Benzmüller, Bruce R. Miller
2020 J jnl
Mechanizing Principia Logico-Metaphysica in Functional Type-Theory.
Rev. Symb. Log.
Daniel Kirchner, Christoph Benzmüller, Edward N. Zalta
2020 A conf
Normative Reasoning with Expressive Logic Combinations.
ECAI
David Fuenmayor, Christoph Benzmüller
2020 J jnl
On Reductions of Hintikka Sets for Higher-Order Logic.
CoRR
Alexander Steen, Christoph Benzmüller
2020 Misc conf
Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding.
KI
Irina Makarenko, Christoph Benzmüller
2020 — conf
Public Announcement Logic in HOL.
DaLí
Sebastian Reiche, Christoph Benzmüller
2020 J jnl
Public Announcement Logic in HOL.
CoRR
Sebastian Reiche, Christoph Benzmüller
2020 Misc conf
Reasonable Machines: A Research Manifesto.
KI
Christoph Benzmüller, Bertram Lomfeld
2020 J jnl
Reasonable Machines: A Research Manifesto.
CoRR
Christoph Benzmüller, Bertram Lomfeld
2020 A conf
The Higher-Order Prover Leo-III.
ECAI
Alexander Steen, Christoph Benzmüller
2019 J jnl
A Computational-Hermeneutic Approach for Conceptual Explicitation.
CoRR
David Fuenmayor, Christoph Benzmüller
2019 J jnl
Computer Science and Metaphysics: A Cross-Fertilization.
CoRR
Daniel Kirchner, Christoph Benzmüller, Edward N. Zalta
2019 J jnl
Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument.
CoRR
Christoph Benzmüller, David Fuenmayor
2019 J jnl
Computer-supported Exploration of a Categorical Axiomatization of Modeloids.
CoRR
Lucca Tiemens, Dana S. Scott, Christoph Benzmüller, Miroslav Benda
2019 J jnl
Designing Normative Theories of Ethical Reasoning: Formal Framework, Methodology, and Tool Support.
CoRR
Christoph Benzmüller, Xavier Parent, Leendert W. N. van der Torre
2019 J jnl
Extensional Higher-Order Paramodulation in Leo-III.
CoRR
Alexander Steen, Christoph Benzmüller
2019 — conf
Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories.
PRICAI (1)
David Fuenmayor, Christoph Benzmüller
2019 J jnl
Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories.
CoRR
David Fuenmayor, Christoph Benzmüller
2019 J jnl
I/O Logic in HOL.
FLAP
Christoph Benzmüller, Ali Farjami, Paul Meder, Xavier Parent
2019 Misc ed.
KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AI, Kassel, Germany, September 23-26, 2019, Proceedings
KI
Christoph Benzmüller, Heiner Stuckenschmidt
2019 — conf
Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations.
FroCos
David Fuenmayor, Christoph Benzmüller
2019 — conf
Modelling the US Constitution to Establish Constitutional Dictatorship.
MIREL@JURIX
Valeria Zahoransky, Christoph Benzmüller
2019 J jnl
Report on the Second International Joint Conference on Rules and Reasoning.
AI Mag.
Christoph Benzmüller, Xavier Parent, Francesco Ricca
2019 — ed.
Selected Student Contributions and Workshop Papers of LuxLogAI 2018
LuxLogAI (Student / Workshop Papers)
Christoph Benzmüller, Xavier Parent, Alexander Steen
2019 Misc conf
The Higher-Order Prover Leo-III (Extended Abstract).
KI
Alexander Steen, Christoph Benzmüller
2019 J jnl
Universal (meta-)logical reasoning: Recent successes.
Sci. Comput. Program.
Christoph Benzmüller
2019 J jnl
åqvist's Dyadic Deontic Logic E in HOL.
FLAP
Christoph Benzmüller, Ali Farjami, Xavier Parent
2018 C conf
A Deontic Logic Reasoning Infrastructure.
CiE
Christoph Benzmüller, Xavier Parent, Leendert W. N. van der Torre
2018 — conf
A Dyadic Deontic Logic in HOL.
DEON
Christoph Benzmüller, Ali Farjami, Xavier Parent
2018 J jnl
Axiom Systems for Category Theory in Free Logic.
Arch. Formal Proofs
Christoph Benzmüller, Dana S. Scott
2018 — conf
Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments.
CLAR
David Fuenmayor, Christoph Benzmüller
2018 J jnl
Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL.
CoRR
Christoph Benzmüller, Ali Farjami, Xavier Parent
2018 J jnl
First Experiments with a Flexible Infrastructure for Normative Reasoning.
CoRR
Christoph Benzmüller, Xavier Parent
2018 J jnl
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL.
Arch. Formal Proofs
David Fuenmayor, Christoph Benzmüller
2018 J jnl
I/O Logic in HOL - First Steps.
CoRR
Christoph Benzmüller, Xavier Parent
2018 — ed.
Proceedings of the 3rd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2018) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2018), Oxford, UK, July 18, 2018.
ARQNL@IJCAR
Christoph Benzmüller, Jens Otten
2018 B ed.
Rules and Reasoning - Second International Joint Conference, RuleML+RR 2018, Luxembourg, September 18-21, 2018, Proceedings
RuleML+RR
Christoph Benzmüller, Francesco Ricca, Xavier Parent, Dumitru Roman
2018 — conf
System Demonstration: The Higher-Order Prover Leo-III.
ARQNL@IJCAR
Alexander Steen, Christoph Benzmüller
2018 A conf
The Higher-Order Prover Leo-III.
IJCAR
Alexander Steen, Christoph Benzmüller
2018 J jnl
The Higher-Order Prover Leo-III.
CoRR
Alexander Steen, Christoph Benzmüller
2017 Misc conf
Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic.
KI
David Fuenmayor, Christoph Benzmüller
2017 — conf
Capability Discovery for Automated Reasoning Systems.
IWIL@LPAR
Alexander Steen, Max Wisniewski, Hans-Jörg Schurr, Christoph Benzmüller
2017 J jnl
Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy.
Logica Universalis
Christoph Benzmüller, Leon Weber, Bruno Woltzenlogel Paleo
2017 J jnl
Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument.
Arch. Formal Proofs
David Fuenmayor, Christoph Benzmüller
2017 J jnl
Cut-Elimination for Quantified Conditional Logic.
J. Philos. Log.
Christoph Benzmüller
2017 — ed.
GCAI 2017, 3rd Global Conference on Artificial Intelligence, Miami, FL, USA, 18-22 October 2017.
GCAI
Christoph Benzmüller, Christine L. Lisetti, Martin Theobald
2017 — conf
Going Polymorphic - TH1 Reasoning for Leo-III.
IWIL@LPAR
Alexander Steen, Max Wisniewski, Christoph Benzmüller
2017 — conf
Leo-III Version 1.1 (System description).
LPAR (Short Presentations)
Christoph Benzmüller, Alexander Steen, Max Wisniewski
2017 J jnl
Mechanizing Principia Logico-Metaphysica in Functional Type Theory.
CoRR
Daniel Kirchner, Christoph Benzmüller, Edward N. Zalta
2017 — conf
Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract).
SBMF
Christoph Benzmüller
2017 B conf
Theorem Provers For Every Normal Modal Logic.
LPAR
Tobias Gleißner, Alexander Steen, Christoph Benzmüller
2017 J jnl
Types, Tableaus and Gödel's God in Isabelle/HOL.
Arch. Formal Proofs
David Fuenmayor, Christoph Benzmüller
2017 J jnl
Universal Reasoning, Rational Argumentation and Human-Machine Interaction.
CoRR
Christoph Benzmüller
2016 — conf
Agent-Based HOL Reasoning.
ICMS
Alexander Steen, Max Wisniewski, Christoph Benzmüller
2016 — conf
Automating Free Logic in Isabelle/HOL.
ICMS
Christoph Benzmüller, Dana S. Scott
2016 J jnl
Axiomatizing Category Theory in Free Logic.
CoRR
Christoph Benzmüller, Dana S. Scott
2016 A conf
Effective Normalization Techniques for HOL.
IJCAR
Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmüller
2016 — conf
Einsatz von Theorembeweisern in der Lehre.
HDI
Alexander Steen, Max Wisniewski, Christoph Benzmüller
2016 — ed.
GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19 - October 2, 2016, Berlin, Germany
GCAI
Christoph Benzmüller, Geoff Sutcliffe, Raúl Rojas
2016 — conf
Is It Reasonable to Employ Agents in Automated Theorem Proving?.
ICAART (1)
Max Wisniewski, Christoph Benzmüller
2016 — ed.
Proceedings of the 2nd International Workshop Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016)., Coimbra, Portugal, July 1, 2016.
ARQNL@IJCAR
Christoph Benzmüller, Jens Otten
2016 — conf
TPTP and Beyond: Representation of Quantified Non-Classical Logics.
ARQNL@IJCAR
Max Wisniewski, Alexander Steen, Christoph Benzmüller
2016 A* conf
The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics.
IJCAI
Christoph Benzmüller, Bruno Woltzenlogel Paleo
2016 — conf
Translating Higher-Order Modal Logic from RuleML to TPTP.
RuleML (Supplement)
Harold Boley, Christoph Benzmüller, Meng Luan, Zhendong Sha
2016 — conf
Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL.
GCAI
Alexander Steen, Max Wisniewski, Christoph Benzmüller
2015 — ed.
Automated Reasoning in Quantified Non-Classical Logics, ARQNL@IJCAR 2014, Vienna, Austria, July 23, 2014
ARQNL@IJCAR
Christoph Benzmüller, Jens Otten
2015 — conf
Higher-Order Modal Logics: Automation and Applications.
Reasoning Web
Christoph Benzmüller, Bruno Woltzenlogel Paleo
2015 Misc conf
Interacting with Modal Logics in the Coq Proof Assistant.
CSR
Christoph Benzmüller, Bruno Woltzenlogel Paleo
2015 B conf
Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics.
TABLEAUX
Christoph Benzmüller
2015 C conf
LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners.
CICM
Max Wisniewski, Alexander Steen, Christoph Benzmüller
2015 J jnl
LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners.
CoRR
Max Wisniewski, Alexander Steen, Christoph Benzmüller
2015 — conf
Proofs and Reconstructions.
FroCos
Nik Sultana, Christoph Benzmüller, Lawrence C. Paulson
2015 — conf
Systematic Verification of the Modal Logic Cube in Isabelle/HOL.
PxTP@CADE
Christoph Benzmüller, Maximilian Claus, Nik Sultana
2015 J jnl
The Higher-Order Prover Leo-II.
J. Autom. Reason.
Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson, Frank Theiss
2015 B conf
There Is No Best \beta -Normalization Strategy for Higher-Order Reasoners.
LPAR
Alexander Steen, Christoph Benzmüller
2014 A conf
Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers.
ECAI
Christoph Benzmüller, Bruno Woltzenlogel Paleo
2014 — ch.
Automation of Higher-Order Logic.
Computational Logic
Christoph Benzmüller, Dale Miller
2014 — conf
HOL Provers for First-order Modal Logics - Experiments.
ARQNL@IJCAR
Christoph Benzmüller
2014 — conf
On Logic Embeddings and Gödel's God.
WADT
Christoph Benzmüller, Bruno Woltzenlogel Paleo
2014 — ed.
Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, UITP 2014, Vienna, Austria, 17th July 2014.
UITP
Christoph Benzmüller, Bruno Woltzenlogel Paleo
2013 — conf
A Top-down Approach to Combining Logics.
ICAART (2)
Christoph Benzmüller
2013 J jnl
Formalization, Mechanization and Automation of Gödel's Proof of God's Existence.
CoRR
Christoph Benzmüller, Bruno Woltzenlogel Paleo
2013 B conf
HOL Based First-Order Modal Logic Provers.
LPAR
Christoph Benzmüller, Thomas Raths
2013 — conf
LEO-II Version 1.5.
PxTP@CADE
Christoph Benzmüller, Nik Sultana
2013 J jnl
Quantified Multimodal Logics in Simple Type Theory.
Logica Universalis
Christoph Benzmüller, Lawrence C. Paulson
2013 J jnl
Sigma: An integrated development environment for formal ontology.
AI Commun.
Adam Pease, Christoph Benzmüller
2013 J jnl
Update report: LEO-II version 1.5
CoRR
Christoph Benzmüller, Nik Sultana
2012 J jnl
Embedding and automating conditional logics in classical higher-order logic.
Ann. Math. Artif. Intell.
Christoph Benzmüller, Dov M. Gabbay, Valerio Genovese, Daniele Rispoli
2012 J jnl
Higher-order aspects and context in SUMO.
J. Web Semant.
Christoph Benzmüller, Adam Pease
2012 — conf
Implementing Different Proof Calculi for First-order Modal Logics.
PAAR@IJCAR
Christoph Benzmüller, Jens Otten, Thomas Raths
2012 A conf
Implementing and Evaluating Provers for First-order Modal Logics.
ECAI
Christoph Benzmüller, Jens Otten, Thomas Raths
2012 — conf
Understanding LEO-II's proofs.
IWIL@LPAR
Nik Sultana, Christoph Benzmüller
2011 J jnl
Combining and automating classical and non-classical logics in classical higher-order logics.
Ann. Math. Artif. Intell.
Christoph Benzmüller
2011 — ch.
Resource-Bounded Modelling and Analysis of Human-Level Interactive Proofs.
Resource-Adaptive Cognitive Processes
Christoph Benzmüller, Marvin R. G. Schiller, Jörg H. Siekmann
2011 — ch.
ΩMEGA: Resource-Adaptive Processes in an Automated Reasoning System.
Resource-Adaptive Cognitive Processes
Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Jörg H. Siekmann
2010 — conf
Adaptive Assertion-Level Proofs.
EMSQMS@IJCAR
Christoph Benzmüller, Marvin R. G. Schiller
2010 J jnl
Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure.
J. Formaliz. Reason.
Geoff Sutcliffe, Christoph Benzmüller
2010 — conf
Combining Logics in Simple Type Theory.
CLIMA
Christoph Benzmüller
2010 J jnl
Multimodal and intuitionistic logics in simple type theory.
Log. J. IGPL
Christoph Benzmüller, Lawrence C. Paulson
2010 — conf
Progress in Automating Higher-Order Ontology Reasoning.
PAAR@IJCAR
Christoph Benzmüller, Adam Pease
2010 — conf
Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners).
Verification, Induction, Termination Analysis
Christoph Benzmüller
2009 J jnl
A remark on higher order RUE-resolution with EXTRUE
CoRR
Christoph Benzmüller
2009 J jnl
Automating Access Control Logics in Simple Type Theory with LEO-II (Techreport)
CoRR
Christoph Benzmüller
2009 Misc conf
Automating Access Control Logics in Simple Type Theory with LEO-II.
SEC
Christoph Benzmüller
2009 J jnl
Cut-Simulation and Impredicativity
Log. Methods Comput. Sci.
Christoph Benzmüller, Chad E. Brown, Michael Kohlhase
2009 J jnl
Granularity-Adaptive Proof Presentation
CoRR
Marvin R. G. Schiller, Christoph Benzmüller
2009 A conf
Granularity-Adaptive Proof Presentation.
AIED
Marvin R. G. Schiller, Christoph Benzmüller
2009 — ch.
Jacques Herbrand: Life, Logic, and Automated Deduction.
Logic from Russell to Church
Claus-Peter Wirth, Jörg H. Siekmann, Christoph Benzmüller, Serge Autexier
2009 J jnl
Lectures on Jacques Herbrand as a Logician
CoRR
Claus-Peter Wirth, Jörg H. Siekmann, Christoph Benzmüller, Serge Autexier
2009 Misc conf
Presenting Proofs with Adapted Granularity.
KI
Marvin R. G. Schiller, Christoph Benzmüller
2009 — ed.
Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, UITP@TPHOLs 2008, Montréal, Canada, August 22, 2008
UITP@TPHOLs
Serge Autexier, Christoph Benzmüller
2009 A conf
Progress in the Development of Automated Theorem Proving for Higher-Order Logic.
CADE
Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss
2009 — conf
Proof Granularity as an Empirical Problem?
CSEDU (1)
Marvin R. G. Schiller, Christoph Benzmüller
2009 J jnl
Quantified Multimodal Logics in Simple Type Theory
CoRR
Christoph Benzmüller, Lawrence C. Paulson
2009 J jnl
Resource Adaptive Agents in Interactive Theorem Proving
CoRR
Christoph Benzmüller, Volker Sorge
2008 J jnl
Combined reasoning by automated cooperation.
J. Appl. Log.
Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber
2008 — conf
Evaluation of Systems for Higher-order Logic (ESHOL).
PAAR/ESHOL
Christoph Benzmüller, Florian Rabe, Carsten Schürmann, Geoff Sutcliffe
2008 A conf
LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description).
IJCAR
Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke
2008 J jnl
Organization, Transformation, and Propagation of Mathematical Knowledge in Omegamega.
Math. Comput. Sci.
Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Marc Wagner
2008 — conf
Preface.
UITP@TPHOLs
Serge Autexier, Christoph Benzmüller
2008 A conf
THF0 - The Core of the TPTP Language for Higher-Order Logic.
IJCAR
Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe
2007 Misc conf
Deep Inference for Automated Proof Tutoring?
KI
Christoph Benzmüller, Dominik Dietrich, Marvin R. G. Schiller, Serge Autexier
2007 — ed.
Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, UITP@FLoC 2006, Seattle, WA, USA, August 21, 2006
UITP@FLoC
Serge Autexier, Christoph Benzmüller
2006 B conf
A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material.
LREC
Christoph Benzmüller, Helmut Horacek, Henri Lesourd, Ivana Kruijff-Korbayová, Marvin R. G. Schiller, Magdalena Wolska
2006 — conf
An Agent-Based Architecture for Dialogue Systems.
Ershov Memorial Conference
Mark Buckley, Christoph Benzmüller
2006 J jnl
Computer supported mathematics with Omegamega.
J. Appl. Log.
Jörg H. Siekmann, Christoph Benzmüller, Serge Autexier
2006 A conf
Cut-Simulation in Impredicative Logics.
IJCAR
Christoph Benzmüller, Chad E. Brown, Michael Kohlhase
2006 Misc conf
DiaWOz-II - A Tool for Wizard-of-Oz Experiments in Mathematics.
KI
Christoph Benzmüller, Helmut Horacek, Ivana Kruijff-Korbayová, Henri Lesourd, Marvin R. G. Schiller, Magdalena Wolska
2006 J jnl
LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)
CoRR
Christoph Benzmüller, John Harrison, Carsten Schürmann
2006 — ch.
Omega.
The Seventeen Provers of the World
Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet, Jörg H. Siekmann
2006 — conf
PlatOmega: A Mediator between Text-Editors and Proof Assistance Systems.
UITP@FLoC
Marc Wagner, Serge Autexier, Christoph Benzmüller
2006 — conf
Preface.
UITP@FLoC
Serge Autexier, Christoph Benzmüller
2006 J jnl
Towards computer aided mathematics.
J. Appl. Log.
Christoph Benzmüller
2005 — conf
A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity.
MKM
Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier, Claus-Peter Wirth
2005 — conf
A Structured Set of Higher-Order Problems.
TPHOLs
Christoph Benzmüller, Chad E. Brown
2005 — conf
Bridging Theorem Proving and Mathematical Knowledge Retrieval.
Mechanizing Mathematical Reasoning
Christoph Benzmüller, Andreas Meier, Volker Sorge
2005 A* conf
Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs.
AAAI
Christoph Benzmüller, Quoc Bao Vo
2005 — conf
Natural Language Dialog with a Tutor System for Mathematical Proofs.
Cognitive Systems
Christoph Benzmüller, Helmut Horacek, Ivana Kruijff-Korbayová, Manfred Pinkal, Jörg H. Siekmann, Magdalena Wolska
2004 B conf
An Annotated Corpus of Tutorial Dialogs on Mathematical Theorem Proving.
LREC
Magdalena Wolska, Quoc Bao Vo, Dimitra Tsovaltzi, Ivana Kruijff-Korbayová, Elena Karagjosova, Helmut Horacek, Armin Fiedler, Christoph Benzmüller
2004 B conf
Can a Higher-Order and a First-Order Theorem Prover Cooperate?.
LPAR
Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber
2004 J jnl
Higher-order semantics and extensionality.
J. Symb. Log.
Christoph Benzmüller, Chad E. Brown, Michael Kohlhase
2004 Misc conf
Omega: Computer Supported Mathematics.
KI
Jörg H. Siekmann, Christoph Benzmüller
2003 A* conf
Assertion Application in Theorem Proving and Proof Planning.
IJCAI
Quoc Bao Vo, Christoph Benzmüller, Serge Autexier
2003 — conf
Assertion-level Proof Representation with Under-Specification.
MKM Symposium
Serge Autexier, Christoph Benzmüller, Armin Fiedler, Helmut Horacek, Quoc Bao Vo
2003 J jnl
Automatic Learning of Proof Methods in Proof Planning.
Log. J. IGPL
Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller
2003 — conf
Interactive Theorem Proving with Tasks.
UITP@TPHOLs
Malte Hübner, Serge Autexier, Christoph Benzmüller, Andreas Meier
2002 J jnl
Comparing Approaches To Resolution Based Higher-Order Theorem Proving.
Synth.
Christoph Benzmüller
2002 A conf
Proof Development with OMEGA.
CADE
Jörg H. Siekmann, Christoph Benzmüller, 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, Jürgen Zimmer
2002 B conf
Proof Development with Omega-MEGA: sqrt(2) Is Irrational.
LPAR
Jörg H. Siekmann, Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet
2001 — conf
Experiments with an Agent-Oriented Reasoning System.
KI/ÖGAI
Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge
2000 — conf
Resource Guided Concurrent Deduction.
ARW
Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge
1999 — conf
Agent based mathematical reasoning.
Calculemus
Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge
1999 Misc conf
Critical Agents Supporting Interactive Theorem Proving.
EPIA
Christoph Benzmüller, Volker Sorge
1999 — —
Equality and extensionality in automated higher order theorem proving.
Christoph Benzmüller
1999 A conf
Extensional Higher-Order Paramodulation and RUE-Resolution.
CADE
Christoph Benzmüller
1999 J jnl
Integrating Tps and Omega.
J. Univers. Comput. Sci.
Christoph Benzmüller, Matthew Bishop, Volker Sorge
1998 Misc conf
A Blackboard Architecture for Guiding Interactive Proofs.
AIMSA
Christoph Benzmüller, Volker Sorge
1998 A conf
Extensional Higher-Order Resolution.
CADE
Christoph Benzmüller, Michael Kohlhase
1998 A conf
System Description: LEO - A Higher-Order Theorem Prover.
CADE
Christoph Benzmüller, Michael Kohlhase
1997 A conf
Omega: Towards a Mathematical Assistant.
CADE
Christoph Benzmüller, Lassaad Cheikhrouhou, Detlef Fehrer, Armin Fiedler, Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Wolf Schaarschmidt, Jörg H. Siekmann, Volker Sorge