default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDChristoph Benzmüller
Christoph Benzmueller
2020 – today
- 2025
[j48]Christoph Benzmüller, Dana S. Scott:
Notes on Gödel's and Scott's Variants of the Ontological Argument (Isabelle/HOL dataset). Arch. Formal Proofs 2025 (2025)- [i50]Lara Lawniczak, Christoph Benzmüller
:
Logical Modalities within the European AI Act: An Analysis. CoRR abs/2501.19112 (2025) - [i49]Christoph Benzmüller:
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 abs/2502.19311 (2025) - 2024
- [j47]Xavier Parent, Christoph Benzmüller:
Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset). Arch. Formal Proofs 2024 (2024) - [j46]Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe:
Who finds the short proof? Log. J. IGPL 32(3): 442-464 (2024) - [j45]Xavier Parent, Christoph Benzmüller:
Conditional normative reasoning as a fragment of HOL. J. Appl. Non Class. Logics 34(4): 561-592 (2024) - [j44]Alexander Steen, Christoph Benzmüller:
Non-Classical Reasoning for Contemporary AI Applications. Künstliche Intell. 38(1-2): 3-5 (2024) - [j43]Alexander Steen, Christoph Benzmüller:
Challenges for Non-Classical Reasoning in Contemporary AI Applications. Künstliche Intell. 38(1-2): 7-16 (2024) - [j42]Alexander Steen, Christoph Benzmüller:
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. 38(1-2): 17-23 (2024) - [c101]Luca Pasetto, Christoph Benzmüller:
Implementing the Fatio Protocol for Multi-Agent Argumentation in LogiKEy. ARQNL@IJCAR 2024: 38-47 - [c100]Veronika Solopova, Viktoriia Herman, Christoph Benzmüller, Tim Landgraf:
Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection. EACL (Demonstrations) 2024: 44-51 - [p6]Ulrich Furbach, Christoph Benzmüller:
Schließen aus Wissen. Künstliche Intelligenz für Lehrkräfte 2024: 39-50 - [p5]Christoph Benzmüller:
Logikbasierte Wissensverarbeitung. Künstliche Intelligenz für Lehrkräfte 2024: 139-162 - [p4]Lukas Höper, Carsten Schulte, Christoph Benzmüller:
Verantwortung. Künstliche Intelligenz für Lehrkräfte 2024: 219-236 - [e17]Christoph Benzmüller, Jens Otten, Revantha Ramanayake:
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. CEUR Workshop Proceedings 3875, CEUR-WS.org 2024 [contents] - [e16]Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt:
Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I. Lecture Notes in Computer Science 14739, Springer 2024, ISBN 978-3-031-63497-0 [contents] - [e15]Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt:
Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part II. Lecture Notes in Computer Science 14740, Springer 2024, ISBN 978-3-031-63500-7 [contents] - [d3]Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller:
Supplemental material to "Solving Quantified Modal Logic Problems by Translation to Classical Logics". Zenodo, 2024
- [i48]Veronika Solopova, Viktoriia Herman, Christoph Benzmüller, Tim Landgraf:
Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection. CoRR abs/2401.15717 (2024) - [i47]Robert Wasenmüller, Kevin Hilbert, Christoph Benzmüller:
Script-Based Dialog Policy Planning for LLM-Powered Conversational Agents: A Basic Architecture for an "AI Therapist". CoRR abs/2412.15242 (2024) - 2023
- [j41]Veronika Solopova, Oana-Iuliana Popescu, Christoph Benzmüller, Tim Landgraf:
Automated Multilingual Detection of Pro-Kremlin Propaganda in Newspapers and Telegram Posts. Datenbank-Spektrum 23(1): 5-14 (2023) - [j40]Pietro Baroni, Christoph Benzmüller, Yì N. Wáng:
Preface: Special Issue on Logic and Argumentation. J. Log. Comput. 33(2): 189-191 (2023) - [j39]Christoph Benzmüller, Sebastian Reiche:
Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy. J. Log. Comput. 33(6): 1243-1269 (2023) - [c99]Colin Rothgang, Florian Rabe, Christoph Benzmüller:
Theorem Proving in Dependently-Typed Higher-Order Logic. CADE 2023: 438-455 - [c98]Alexander Steen, Geoff Sutcliffe, Tobias Scholl, Christoph Benzmüller:
Solving Modal Logic Problems by Translation to Higher-Order Logic. CLAR 2023: 25-43 - [c97]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:
PapagAI: Automated Feedback for Reflective Essays. KI 2023: 198-206 - [c96]Jonas Bayer, Alexey Gonus, Christoph Benzmüller, Dana S. Scott:
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. CICM 2023: 69-83 - [e14]Christoph Benzmüller, Jens Otten:
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. CEUR Workshop Proceedings 3326, CEUR-WS.org 2023 [contents] - [i46]Veronika Solopova, Oana-Iuliana Popescu, Christoph Benzmüller, Tim Landgraf:
Automated multilingual detection of Pro-Kremlin propaganda in newspapers and Telegram posts. CoRR abs/2301.10604 (2023) - [i45]Colin Rothgang, Florian Rabe, Christoph Benzmüller:
Theorem Proving in Dependently-Typed Higher-Order Logic - Extended Preprint. CoRR abs/2305.15382 (2023) - [i44]Jonas Bayer, Aleksey Gonus, Christoph Benzmüller, Dana S. Scott:
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. CoRR abs/2306.09074 (2023) - [i43]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:
PapagAI: Automated Feedback for Reflective Essays. CoRR abs/2307.07523 (2023) - [i42]Xavier Parent, Christoph Benzmüller:
Normative Conditional Reasoning as a Fragment of HOL. CoRR abs/2308.10686 (2023) - 2022
- [j38]Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe:
Automation of Boolos' Curious Inference in Isabelle/HOL. Arch. Formal Proofs 2022 (2022) - [j37]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:
Collaborative Speculations on Future Themes for Participatory Design in Germany. i-com 21(2): 283-298 (2022) - [c95]Xavier Parent, Christoph Benzmüller:
Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results. ARQNL@IJCAR 2022: 92-108 - [c94]Alexander Steen, David Fuenmayor, Tobias Gleißner, Geoff Sutcliffe, Christoph Benzmüller:
Automated Reasoning in Non-classical Logics in the TPTP World. PAAR@IJCAR 2022 - [i41]Christoph Benzmüller:
A Simplified Variant of Gödel's Ontological Argument. CoRR abs/2202.06264 (2022) - [i40]Alexander Steen, David Fuenmayor, Tobias Gleißner, Geoff Sutcliffe, Christoph Benzmüller:
Automated Reasoning in Non-classical Logics in the TPTP World. CoRR abs/2202.09836 (2022) - [i39]Jonas Bayer, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lamport, Yuri V. Matiyasevich, Lawrence C. Paulson, Dierk Schleicher, Benedikt Stock, Efim I. Zelmanov:
Mathematical Proof Between Generations. CoRR abs/2207.04779 (2022) - [i38]Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe:
Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers. CoRR abs/2208.06879 (2022) - [i37]Alexander Steen, Geoff Sutcliffe, Tobias Gleißner, Christoph Benzmüller:
Solving QMLTP Problems by Translation to Higher-order Logic. CoRR abs/2212.09570 (2022) - 2021
- [j36]Christoph Benzmüller:
Exploring Simplified Variants of Gödel's Ontological Argument in Isabelle/HOL. Arch. Formal Proofs 2021 (2021) - [j35]Christoph Benzmüller, Sebastian Reiche:
Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL. Arch. Formal Proofs 2021 (2021) - [j34]Alexander Steen, Christoph Benzmüller:
Extensional Higher-Order Paramodulation in Leo-III. J. Autom. Reason. 65(6): 775-807 (2021) - [j33]Christoph Benzmüller, Xavier Parent, Francesco Ricca:
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. 21(1): 1-3 (2021) - [c93]Veronika Solopova, Oana-Iuliana Popescu, Margarita Chikobava, Ralf Romeike, Tim Landgraf, Christoph Benzmüller:
A German Corpus of Reflective Sentences. ICON 2021: 593-600 - [c92]Christoph Benzmüller, David Fuenmayor:
Value-Oriented Legal Argumentation in Isabelle/HOL. ITP 2021: 7:1-7:20 - [e13]Pietro Baroni, Christoph Benzmüller, Yì N. Wáng:
Logic and Argumentation - 4th International Conference, CLAR 2021, Hangzhou, China, October 20-22, 2021, Proceedings. Lecture Notes in Computer Science 13040, Springer 2021, ISBN 978-3-030-89390-3 [contents] - [d2]Alexander Steen, Christoph Benzmueller:
Leo-III - A Theorem Prover for Higher-Order Logic. Version v1.5.2. Zenodo, 2021 [all versions] - [i36]Christoph Benzmüller, Sebastian Reiche:
Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy. CoRR abs/2111.01654 (2021) - 2020
- [j32]Christoph Benzmüller, Xavier Parent, Leendert W. N. van der Torre:
Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. Artif. Intell. 287: 103348 (2020) - [j31]Christoph Benzmüller, Dana S. Scott:
Automating Free Logic in HOL, with an Experimental Application in Category Theory. J. Autom. Reason. 64(1): 53-72 (2020) - [j30]Daniel Kirchner, Christoph Benzmüller, Edward N. Zalta:
Mechanizing Principia Logico-Metaphysica in Functional Type-Theory. Rev. Symb. Log. 13(1): 206-218 (2020) - [c91]Lucca Tiemens, Dana S. Scott, Christoph Benzmüller, Miroslav Benda:
Computer-Supported Exploration of a Categorical Axiomatization of Modeloids. RAMiCS 2020: 302-317 - [c90]David Fuenmayor, Christoph Benzmüller:
Computer-Supported Analysis of Arguments in Climate Engineering. CLAR 2020: 104-115 - [c89]Sebastian Reiche, Christoph Benzmüller:
Public Announcement Logic in HOL. DaLí 2020: 222-238 - [c88]David Fuenmayor, Christoph Benzmüller:
Normative Reasoning with Expressive Logic Combinations. ECAI 2020: 2903-2904 - [c87]Alexander Steen, Christoph Benzmüller:
The Higher-Order Prover Leo-III. ECAI 2020: 2937-2938 - [c86]Irina Makarenko, Christoph Benzmüller:
Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding. KI 2020: 116-131 - [c85]Christoph Benzmüller, Bertram Lomfeld:
Reasonable Machines: A Research Manifesto. KI 2020: 251-258 - [c84]Christoph Benzmüller:
A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument. KR 2020: 779-789 - [e12]Christoph Benzmüller, Bruce R. Miller:
Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings. Lecture Notes in Computer Science 12236, Springer 2020, ISBN 978-3-030-53517-9 [contents] - [d1]Alexander Steen, Christoph Benzmueller:
Leo-III 1.5 - A Theorem Prover for Higher-Order Logic. Version v1.5. Zenodo, 2020 [all versions] - [i35]Christoph Benzmüller:
A (Simplified) Supreme Being Necessarily Exists - Says the Computer! CoRR abs/2001.04701 (2020) - [i34]Alexander Steen, Christoph Benzmüller:
On Reductions of Hintikka Sets for Higher-Order Logic. CoRR abs/2004.07506 (2020) - [i33]Christoph Benzmüller, David Fuenmayor, Bertram Lomfeld:
Encoding Legal Balancing: Automating an Abstract Ethico-Legal Value Ontology in Preference Logic. CoRR abs/2006.12789 (2020) - [i32]David Fuenmayor, Christoph Benzmüller:
Higher-order Logic as Lingua Franca - Integrating Argumentative Discourse and Deep Logical Analysis. CoRR abs/2007.01019 (2020) - [i31]Christoph Benzmüller, Bertram Lomfeld:
Reasonable Machines: A Research Manifesto. CoRR abs/2008.06250 (2020) - [i30]Sebastian Reiche, Christoph Benzmüller:
Public Announcement Logic in HOL. CoRR abs/2010.00810 (2020)
2010 – 2019
- 2019
- [j29]Christoph Benzmüller, Xavier Parent, Francesco Ricca:
Report on the Second International Joint Conference on Rules and Reasoning. AI Mag. 40(2): 73-74 (2019) - [j28]Christoph Benzmüller, Ali Farjami, Paul Meder, Xavier Parent:
I/O Logic in HOL. FLAP 6(5): 715-732 (2019) - [j27]Christoph Benzmüller, Ali Farjami, Xavier Parent:
åqvist's Dyadic Deontic Logic E in HOL. FLAP 6(5): 733-754 (2019) - [j26]Christoph Benzmüller:
Universal (meta-)logical reasoning: Recent successes. Sci. Comput. Program. 172: 48-62 (2019) - [c83]David Fuenmayor, Christoph Benzmüller:
Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations. FroCos 2019: 112-128 - [c82]Valeria Zahoransky, Christoph Benzmüller:
Modelling the US Constitution to Establish Constitutional Dictatorship. MIREL@JURIX 2019 - [c81]Alexander Steen, Christoph Benzmüller:
The Higher-Order Prover Leo-III (Extended Abstract). KI 2019: 333-337 - [c80]David Fuenmayor, Christoph Benzmüller:
Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories. PRICAI (1) 2019: 418-432 - [e11]Christoph Benzmüller, Heiner Stuckenschmidt:
KI 2019: Advances in Artificial Intelligence - 42nd German Conference on AI, Kassel, Germany, September 23-26, 2019, Proceedings. Lecture Notes in Computer Science 11793, Springer 2019, ISBN 978-3-030-30178-1 [contents] - [e10]Christoph Benzmüller, Xavier Parent, Alexander Steen:
Selected Student Contributions and Workshop Papers of LuxLogAI 2018. Kalpa Publications in Computing 10, EasyChair 2019 [contents] - [i29]David Fuenmayor, Christoph Benzmüller:
Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories. CoRR abs/1903.09818 (2019) - [i28]Christoph Benzmüller, Xavier Parent, Leendert W. N. van der Torre:
Designing Normative Theories of Ethical Reasoning: Formal Framework, Methodology, and Tool Support. CoRR abs/1903.10187 (2019) - [i27]Daniel Kirchner, Christoph Benzmüller, Edward N. Zalta:
Computer Science and Metaphysics: A Cross-Fertilization. CoRR abs/1905.00787 (2019) - [i26]David Fuenmayor, Christoph Benzmüller:
A Computational-Hermeneutic Approach for Conceptual Explicitation. CoRR abs/1906.06582 (2019) - [i25]Alexander Steen, Christoph Benzmüller:
Extensional Higher-Order Paramodulation in Leo-III. CoRR abs/1907.11501 (2019) - [i24]Christoph Benzmüller, David Fuenmayor:
Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument. CoRR abs/1910.08955 (2019) - [i23]Lucca Tiemens, Dana S. Scott, Christoph Benzmüller, Miroslav Benda:
Computer-supported Exploration of a Categorical Axiomatization of Modeloids. CoRR abs/1910.12863 (2019) - 2018
- [j25]Christoph Benzmüller, Dana S. Scott:
Axiom Systems for Category Theory in Free Logic. Arch. Formal Proofs 2018 (2018) - [j24]David Fuenmayor, Christoph Benzmüller:
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL. Arch. Formal Proofs 2018 (2018) - [c79]Alexander Steen, Christoph Benzmüller:
System Demonstration: The Higher-Order Prover Leo-III. ARQNL@IJCAR 2018: 79-85 - [c78]Alexander Steen, Christoph Benzmüller:
The Higher-Order Prover Leo-III. IJCAR 2018: 108-116 - [c77]Christoph Benzmüller, Xavier Parent, Leendert W. N. van der Torre:
A Deontic Logic Reasoning Infrastructure. CiE 2018: 60-69 - [c76]David Fuenmayor, Christoph Benzmüller:
Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments. CLAR 2018: 187-207 - [c75]Christoph Benzmüller, Ali Farjami, Xavier Parent:
A Dyadic Deontic Logic in HOL. DEON 2018: 33-49 - [e9]Christoph Benzmüller, Jens Otten:
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. CEUR Workshop Proceedings 2095, CEUR-WS.org 2018 [contents] - [e8]Christoph Benzmüller, Francesco Ricca, Xavier Parent, Dumitru Roman:
Rules and Reasoning - Second International Joint Conference, RuleML+RR 2018, Luxembourg, September 18-21, 2018, Proceedings. Lecture Notes in Computer Science 11092, Springer 2018, ISBN 978-3-319-99905-0 [contents] - [i22]Alexander Steen, Christoph Benzmüller:
The Higher-Order Prover Leo-III. CoRR abs/1802.02732 (2018) - [i21]Christoph Benzmüller, Ali Farjami, Xavier Parent:
Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL. CoRR abs/1802.08454 (2018) - [i20]Christoph Benzmüller, Xavier Parent:
I/O Logic in HOL - First Steps. CoRR abs/1803.09681 (2018) - [i19]Christoph Benzmüller, Xavier Parent:
First Experiments with a Flexible Infrastructure for Normative Reasoning. CoRR abs/1804.02929 (2018) - 2017
- [j23]David Fuenmayor, Christoph Benzmüller:
Types, Tableaus and Gödel's God in Isabelle/HOL. Arch. Formal Proofs 2017 (2017) - [j22]David Fuenmayor, Christoph Benzmüller:
Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument. Arch. Formal Proofs 2017 (2017) - [j21]Christoph Benzmüller:
Cut-Elimination for Quantified Conditional Logic. J. Philos. Log. 46(3): 333-353 (2017) - [j20]Christoph Benzmüller, L. Weber, Bruno Woltzenlogel Paleo:
Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy. Logica Universalis 11(1): 139-151 (2017) - [c74]David Fuenmayor, Christoph Benzmüller:
Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic. KI 2017: 114-127 - [c73]Christoph Benzmüller, Alexander Steen, Max Wisniewski:
Leo-III Version 1.1 (System description). LPAR (Short Presentations) 2017: 11-26 - [c72]Tobias Gleißner, Alexander Steen, Christoph Benzmüller:
Theorem Provers For Every Normal Modal Logic. LPAR 2017: 14-30 - [c71]Alexander Steen, Max Wisniewski, Christoph Benzmüller:
Going Polymorphic - TH1 Reasoning for Leo-III. IWIL@LPAR 2017: 100-112 - [c70]Alexander Steen, Max Wisniewski, Hans-Jörg Schurr, Christoph Benzmüller:
Capability Discovery for Automated Reasoning Systems. IWIL@LPAR 2017: 113-118 - [c69]Christoph Benzmüller:
Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract). SBMF 2017: 7-11 - [e7]Christoph Benzmüller, Christine L. Lisetti, Martin Theobald:
GCAI 2017, 3rd Global Conference on Artificial Intelligence, Miami, FL, USA, 18-22 October 2017. EPiC Series in Computing 50, EasyChair 2017 [contents] - [i18]Christoph Benzmüller:
Universal Reasoning, Rational Argumentation and Human-Machine Interaction. CoRR abs/1703.09620 (2017) - [i17]Daniel Kirchner, Christoph Benzmüller, Edward N. Zalta:
Mechanizing Principia Logico-Metaphysica in Functional Type Theory. CoRR abs/1711.06542 (2017) - 2016
- [c68]Max Wisniewski, Alexander Steen, Christoph Benzmüller:
TPTP and Beyond: Representation of Quantified Non-Classical Logics. ARQNL@IJCAR 2016: 51-65 - [c67]Max Wisniewski, Alexander Steen, Kim Kern, Christoph Benzmüller:
Effective Normalization Techniques for HOL. IJCAR 2016: 362-370 - [c66]Alexander Steen, Max Wisniewski, Christoph Benzmüller:
Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL. GCAI 2016: 1-10 - [c65]Max Wisniewski, Christoph Benzmüller:
Is It Reasonable to Employ Agents in Automated Theorem Proving?. ICAART (1) 2016: 281-286 - [c64]Christoph Benzmüller, Dana S. Scott:
Automating Free Logic in Isabelle/HOL. ICMS 2016: 43-50 - [c63]Alexander Steen, Max Wisniewski, Christoph Benzmüller:
Agent-Based HOL Reasoning. ICMS 2016: 75-81 - [c62]Christoph Benzmüller, Bruno Woltzenlogel Paleo:
The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics. IJCAI 2016: 936-942 - [c61]Harold Boley, Christoph Benzmüller, Meng Luan, Zhendong Sha:
Translating Higher-Order Modal Logic from RuleML to TPTP. RuleML (Supplement) 2016 - [c60]Alexander Steen, Max Wisniewski, Christoph Benzmüller:
Einsatz von Theorembeweisern in der Lehre. HDI 2016: 81-92 - [e6]Christoph Benzmüller, Jens Otten:
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. CEUR Workshop Proceedings 1770, CEUR-WS.org 2016 [contents] - [e5]Christoph Benzmüller, Geoff Sutcliffe, Raúl Rojas:
GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19 - October 2, 2016, Berlin, Germany. EPiC Series in Computing 41, EasyChair 2016 [contents] - [i16]Christoph Benzmüller, Dana S. Scott:
Axiomatizing Category Theory in Free Logic. CoRR abs/1609.01493 (2016) - 2015
- [j19]Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson, Frank Theiss:
The Higher-Order Prover Leo-II. J. Autom. Reason. 55(4): 389-404 (2015) - [c59]Christoph Benzmüller, Bruno Woltzenlogel Paleo:
Interacting with Modal Logics in the Coq Proof Assistant. CSR 2015: 398-411 - [c58]Nik Sultana, Christoph Benzmüller, Lawrence C. Paulson:
Proofs and Reconstructions. FroCos 2015: 256-271 - [c57]Alexander Steen, Christoph Benzmüller:
There Is No Best \beta -Normalization Strategy for Higher-Order Reasoners. LPAR 2015: 329-339 - [c56]Max Wisniewski, Alexander Steen, Christoph Benzmüller:
LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners. CICM 2015: 325-330 - [c55]Christoph Benzmüller, Bruno Woltzenlogel Paleo:
Higher-Order Modal Logics: Automation and Applications. Reasoning Web 2015: 32-74 - [c54]Christoph Benzmüller:
Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics. TABLEAUX 2015: 213-220 - [c53]Christoph Benzmüller, Maximilian Claus, Nik Sultana:
Systematic Verification of the Modal Logic Cube in Isabelle/HOL. PxTP@CADE 2015: 27-41 - [e4]Christoph Benzmüller, Jens Otten:
Automated Reasoning in Quantified Non-Classical Logics, ARQNL@IJCAR 2014, Vienna, Austria, July 23, 2014. EPiC Series in Computing 33, EasyChair 2015 [contents] - [i15]Max Wisniewski, Alexander Steen, Christoph Benzmüller:
LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners. CoRR abs/1505.01629 (2015) - 2014
- [c52]Christoph Benzmüller:
HOL Provers for First-order Modal Logics - Experiments. ARQNL@IJCAR 2014: 37-41 - [c51]Christoph Benzmüller, Bruno Woltzenlogel Paleo:
Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers. ECAI 2014: 93-98 - [c50]Christoph Benzmüller, Bruno Woltzenlogel Paleo:
On Logic Embeddings and Gödel's God. WADT 2014: 3-6 - [e3]Christoph Benzmüller, Bruno Woltzenlogel Paleo:
Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, UITP 2014, Vienna, Austria, 17th July 2014. EPTCS 167, 2014 [contents] - [r2]Christoph Benzmüller, Dale Miller:
Automation of Higher-Order Logic. Computational Logic 2014: 215-254 - 2013
- [j18]Christoph Benzmueller, Bruno Woltzenlogel Paleo:
Gödel's God in Isabelle/HOL. Arch. Formal Proofs 2013 (2013) - [j17]Adam Pease, Christoph Benzmüller:
Sigma: An integrated development environment for formal ontology. AI Commun. 26(1): 79-97 (2013) - [j16]Christoph Benzmüller, Lawrence C. Paulson:
Quantified Multimodal Logics in Simple Type Theory. Logica Universalis 7(1): 7-20 (2013) - [c49]Christoph Benzmüller, Nik Sultana:
LEO-II Version 1.5. PxTP@CADE 2013: 2-10 - [c48]Christoph Benzmüller:
A Top-down Approach to Combining Logics. ICAART (2) 2013: 346-351 - [c47]Christoph Benzmueller:
Automating Quantified Conditional Logics in HOL. IJCAI 2013: 746-753 - [c46]Christoph Benzmüller, Thomas Raths:
HOL Based First-Order Modal Logic Provers. LPAR 2013: 127-136 - [i14]Christoph Benzmüller, Nik Sultana:
Update report: LEO-II version 1.5. CoRR abs/1303.3761 (2013) - [i13]Christoph Benzmüller, Bruno Woltzenlogel Paleo:
Formalization, Mechanization and Automation of Gödel's Proof of God's Existence. CoRR abs/1308.4526 (2013) - 2012
- [j15]Christoph Benzmüller, Dov M. Gabbay, Valerio Genovese, Daniele Rispoli:
Embedding and automating conditional logics in classical higher-order logic. Ann. Math. Artif. Intell. 66(1-4): 257-271 (2012) - [j14]Christoph Benzmüller, Adam Pease:
Higher-order aspects and context in SUMO. J. Web Semant. 12: 104-117 (2012) - [c45]Christoph Benzmüller, Jens Otten, Thomas Raths:
Implementing Different Proof Calculi for First-order Modal Logics. PAAR@IJCAR 2012: 12-18 - [c44]Christoph Benzmüller, Jens Otten, Thomas Raths:
Implementing and Evaluating Provers for First-order Modal Logics. ECAI 2012: 163-168 - [c43]Nik Sultana, Christoph Benzmüller:
Understanding LEO-II's proofs. IWIL@LPAR 2012: 33-52 - [i12]Christoph Benzmueller, Valerio Genovese:
Quantified Conditional Logics are Fragments of HOL. CoRR abs/1204.5920 (2012) - [i11]Christoph Benzmueller, Thomas Raths:
FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends. CoRR abs/1207.6685 (2012) - 2011
- [j13]Christoph Benzmüller:
Combining and automating classical and non-classical logics in classical higher-order logics. Ann. Math. Artif. Intell. 62(1-2): 103-128 (2011) - [p3]Christoph Benzmüller, Marvin R. G. Schiller, Jörg H. Siekmann:
Resource-Bounded Modelling and Analysis of Human-Level Interactive Proofs. Resource-Adaptive Cognitive Processes 2011: 291-311 - [p2]Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Jörg H. Siekmann:
ΩMEGA: Resource-Adaptive Processes in an Automated Reasoning System. Resource-Adaptive Cognitive Processes 2011: 389-423 - [i10]Christoph Benzmueller, Dov M. Gabbay, Valerio Genovese, Daniele Rispoli:
Embedding and Automating Conditional Logics in Classical Higher-Order Logic. CoRR abs/1106.3685 (2011) - 2010
- [j12]Christoph Benzmüller, Lawrence C. Paulson:
Multimodal and intuitionistic logics in simple type theory. Log. J. IGPL 18(6): 881-892 (2010) - [j11]Geoff Sutcliffe, Christoph Benzmüller:
Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. J. Formaliz. Reason. 3(1): 1-27 (2010) - [c42]Christoph Benzmüller:
Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners). Verification, Induction, Termination Analysis 2010: 117-128 - [c41]Christoph Benzmüller, Adam Pease:
Progress in Automating Higher-Order Ontology Reasoning. PAAR@IJCAR 2010: 22-32 - [c40]Christoph Benzmüller, Marvin R. G. Schiller:
Adaptive Assertion-Level Proofs. EMSQMS@IJCAR 2010: 39-40 - [c39]Christoph Benzmüller:
Combining Logics in Simple Type Theory. CLIMA 2010: 33-48 - [i9]Christoph Benzmueller:
Simple Type Theory as Framework for Combining Logics. CoRR abs/1004.5500 (2010)
2000 – 2009
- 2009
- [j10]Christoph Benzmüller, Chad E. Brown, Michael Kohlhase:
Cut-Simulation and Impredicativity. Log. Methods Comput. Sci. 5(1) (2009) - [c38]Marvin R. G. Schiller, Christoph Benzmüller:
Granularity-Adaptive Proof Presentation. AIED 2009: 599-601 - [c37]Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss:
Progress in the Development of Automated Theorem Proving for Higher-Order Logic. CADE 2009: 116-130 - [c36]Marvin R. G. Schiller, Christoph Benzmüller:
Proof Granularity as an Empirical Problem? CSEDU (1) 2009: 350-354 - [c35]Marvin R. G. Schiller, Christoph Benzmüller:
Presenting Proofs with Adapted Granularity. KI 2009: 289-297 - [c34]Christoph Benzmüller:
Automating Access Control Logics in Simple Type Theory with LEO-II. SEC 2009: 387-398 - [e2]Serge Autexier, Christoph Benzmüller:
Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, UITP@TPHOLs 2008, Montréal, Canada, August 22, 2008. Electronic Notes in Theoretical Computer Science 226, Elsevier 2009 [contents] - [r1]Claus-Peter Wirth, Jörg H. Siekmann, Christoph Benzmüller, Serge Autexier:
Jacques Herbrand: Life, Logic, and Automated Deduction. Logic from Russell to Church 2009: 195-254 - [i8]Christoph Benzmüller:
Automating Access Control Logics in Simple Type Theory with LEO-II (Techreport). CoRR abs/0901.3574 (2009) - [i7]Christoph Benzmüller, Volker Sorge:
Resource Adaptive Agents in Interactive Theorem Proving. CoRR abs/0901.3585 (2009) - [i6]Christoph Benzmüller:
A remark on higher order RUE-resolution with EXTRUE. CoRR abs/0901.3608 (2009) - [i5]Claus-Peter Wirth, Jörg H. Siekmann, Christoph Benzmüller, Serge Autexier:
Lectures on Jacques Herbrand as a Logician. CoRR abs/0902.4682 (2009) - [i4]Marvin R. G. Schiller, Christoph Benzmüller:
Granularity-Adaptive Proof Presentation. CoRR abs/0903.0314 (2009) - [i3]Christoph Benzmüller, Lawrence C. Paulson:
Quantified Multimodal Logics in Simple Type Theory. CoRR abs/0905.2435 (2009) - [i2]Christoph Benzmueller:
Automating Quantified Multimodal Logics in Simple Type Theory -- A Case Study. CoRR abs/0905.4369 (2009) - 2008
- [j9]Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber:
Combined reasoning by automated cooperation. J. Appl. Log. 6(3): 318-342 (2008) - [j8]Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Marc Wagner:
Organization, Transformation, and Propagation of Mathematical Knowledge in Omegamega. Math. Comput. Sci. 2(2): 253-277 (2008) - [c33]Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, Arnaud Fietzke:
LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). IJCAR 2008: 162-170 - [c32]Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe:
THF0 - The Core of the TPTP Language for Higher-Order Logic. IJCAR 2008: 491-506 - [c31]Christoph Benzmüller, Florian Rabe, Carsten Schürmann, Geoff Sutcliffe:
Evaluation of Systems for Higher-order Logic (ESHOL). PAAR/ESHOL 2008 - [c30]Serge Autexier, Christoph Benzmüller:
Preface. UITP@TPHOLs 2008: 1-2 - 2007
- [c29]Christoph Benzmüller, Dominik Dietrich, Marvin R. G. Schiller, Serge Autexier:
Deep Inference for Automated Proof Tutoring? KI 2007: 435-439 - [e1]Serge Autexier, Christoph Benzmüller:
Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, UITP@FLoC 2006, Seattle, WA, USA, August 21, 2006. Electronic Notes in Theoretical Computer Science 174(2), Elsevier 2007 [contents] - 2006
- [j7]Christoph Benzmüller:
Towards computer aided mathematics. J. Appl. Log. 4(4): 359-365 (2006) - [j6]Jörg H. Siekmann, Christoph Benzmüller, Serge Autexier:
Computer supported mathematics with Omegamega. J. Appl. Log. 4(4): 533-559 (2006) - [c28]Christoph Benzmüller, Chad E. Brown, Michael Kohlhase:
Cut-Simulation in Impredicative Logics. IJCAR 2006: 220-234 - [c27]Mark Buckley, Christoph Benzmüller:
An Agent-Based Architecture for Dialogue Systems. Ershov Memorial Conference 2006: 135-147 - [c26]Christoph Benzmüller, Helmut Horacek, Ivana Kruijff-Korbayová, Henri Lesourd, Marvin R. G. Schiller, Magdalena Wolska:
DiaWOz-II - A Tool for Wizard-of-Oz Experiments in Mathematics. KI 2006: 159-173 - [c25]Christoph Benzmüller, Helmut Horacek, Henri Lesourd, Ivana Kruijff-Korbayová, Marvin R. G. Schiller, Magdalena Wolska:
A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material. LREC 2006: 1766-1769 - [c24]Serge Autexier, Christoph Benzmüller:
Preface. UITP@FLoC 2006: 1-2 - [c23]Marc Wagner, Serge Autexier, Christoph Benzmüller:
PlatOmega: A Mediator between Text-Editors and Proof Assistance Systems. UITP@FLoC 2006: 87-107 - [p1]Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet, Jörg H. Siekmann:
Omega. The Seventeen Provers of the World 2006: 127-141 - [i1]Christoph Benzmüller, John Harrison, Carsten Schürmann:
LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL). CoRR abs/cs/0601042 (2006) - 2005
- [c22]Christoph Benzmüller, Quoc Bao Vo:
Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs. AAAI 2005: 516-522 - [c21]Christoph Benzmüller, Andreas Meier, Volker Sorge:
Bridging Theorem Proving and Mathematical Knowledge Retrieval. Mechanizing Mathematical Reasoning 2005: 277-296 - [c20]Christoph Benzmüller, Helmut Horacek, Ivana Kruijff-Korbayová, Manfred Pinkal, Jörg H. Siekmann, Magdalena Wolska:
Natural Language Dialog with a Tutor System for Mathematical Proofs. Cognitive Systems 2005: 1-14 - [c19]Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier, Claus-Peter Wirth:
A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity. MKM 2005: 126-142 - [c18]Christoph Benzmüller, Chad E. Brown:
A Structured Set of Higher-Order Problems. TPHOLs 2005: 66-81 - 2004
- [j5]Christoph Benzmüller, Chad E. Brown, Michael Kohlhase:
Higher-order semantics and extensionality. J. Symb. Log. 69(4): 1027-1088 (2004) - [c17]Jörg H. Siekmann, Christoph Benzmüller:
Omega: Computer Supported Mathematics. KI 2004: 3-28 - [c16]Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber:
Can a Higher-Order and a First-Order Theorem Prover Cooperate?. LPAR 2004: 415-431 - [c15]Magdalena Wolska, Quoc Bao Vo, Dimitra Tsovaltzi, Ivana Kruijff-Korbayová, Elena Karagjosova, Helmut Horacek, Armin Fiedler, Christoph Benzmüller:
An Annotated Corpus of Tutorial Dialogs on Mathematical Theorem Proving. LREC 2004 - 2003
- [j4]Mateja Jamnik, Manfred Kerber, Martin Pollet, Christoph Benzmüller:
Automatic Learning of Proof Methods in Proof Planning. Log. J. IGPL 11(6): 647-673 (2003) - [c14]Quoc Bao Vo, Christoph Benzmüller, Serge Autexier:
Assertion Application in Theorem Proving and Proof Planning. IJCAI 2003: 1343- - [c13]Serge Autexier, Christoph Benzmüller, Armin Fiedler, Helmut Horacek, Quoc Bao Vo:
Assertion-level Proof Representation with Under-Specification. MKM Symposium 2003: 5-23 - [c12]Malte Hübner, Serge Autexier, Christoph Benzmüller, Andreas Meier:
Interactive Theorem Proving with Tasks. UITP@TPHOLs 2003: 161-181 - 2002
- [j3]Christoph Benzmüller:
Comparing Approaches To Resolution Based Higher-Order Theorem Proving. Synth. 133(1-2): 203-335 (2002) - [c11]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:
Proof Development with OMEGA. CADE 2002: 144-149 - [c10]Jörg H. Siekmann, Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet:
Proof Development with Omega-MEGA: sqrt(2) Is Irrational. LPAR 2002: 367-387 - 2001
- [c9]Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge:
Experiments with an Agent-Oriented Reasoning System. KI/ÖGAI 2001: 409-424 - 2000
- [c8]Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge:
Resource Guided Concurrent Deduction. ARW 2000
1990 – 1999
- 1999
- [b1]Christoph Benzmüller:
Equality and extensionality in automated higher order theorem proving. Saarland University, Saarbrücken, Germany, 1999, pp. 1-134 - [j2]Jörg H. Siekmann, Stephan M. Hess, Christoph Benzmüller, Lassaad Cheikhrouhou, Armin Fiedler, Helmut Horacek, Michael Kohlhase, Karsten Konrad, Andreas Meier, Erica Melis, Martin Pollet, Volker Sorge:
L<Omega>UI: Lovely <Omega>MEGA User Interface. Formal Aspects Comput. 11(3): 326-342 (1999) - [j1]Christoph Benzmüller, Matthew Bishop, Volker Sorge:
Integrating Tps and Omega. J. Univers. Comput. Sci. 5(3): 188-207 (1999) - [c7]Christoph Benzmüller:
Extensional Higher-Order Paramodulation and RUE-Resolution. CADE 1999: 399-413 - [c6]Christoph Benzmüller, Volker Sorge:
Critical Agents Supporting Interactive Theorem Proving. EPIA 1999: 208-221 - [c5]Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge:
Agent based mathematical reasoning. Calculemus 1999: 340-351 - 1998
- [c4]Christoph Benzmüller, Volker Sorge:
A Blackboard Architecture for Guiding Interactive Proofs. AIMSA 1998: 102-114 - [c3]Christoph Benzmüller, Michael Kohlhase:
Extensional Higher-Order Resolution. CADE 1998: 56-71 - [c2]Christoph Benzmüller, Michael Kohlhase:
System Description: LEO - A Higher-Order Theorem Prover. CADE 1998: 139-144 - 1997
- [c1]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:
Omega: Towards a Mathematical Assistant. CADE 1997: 252-255
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
[+][–] Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
[+][–] Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-05-14 23:16 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
