Christoph Benzmüller

Orcid: 0000-0002-3392-3093

Affiliations:
  • University of Bamberg, Germany
  • FU Berlin, Department of Mathematics and Computer Science, Germany (former)
  • University of Luxembourg, Faculty of Science, Technology and Medicine, Luxembourg (former)


According to our database1, Christoph Benzmüller authored at least 181 papers between 1997 and 2024.

Collaborative distances:
  • Dijkstra number2 of two.
  • Erdős number3 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Who finds the short proof?
Log. J. IGPL, 2024

Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset).
Arch. Formal Proofs, 2024

Check News in One Click: NLP-Empowered Pro-Kremlin Propaganda Detection.
Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics, 2024

2023
Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy.
J. Log. Comput., August, 2023

Preface: Special Issue on Logic and Argumentation.
J. Log. Comput., March, 2023

Automated Multilingual Detection of Pro-Kremlin Propaganda in Newspapers and Telegram Posts.
Datenbank-Spektrum, March, 2023

Normative Conditional Reasoning as a Fragment of HOL.
CoRR, 2023

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation.
CoRR, 2023

Theorem Proving in Dependently-Typed Higher-Order Logic - Extended Preprint.
CoRR, 2023

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation.
Proceedings of the Intelligent Computer Mathematics - 16th International Conference, 2023

PapagAI: Automated Feedback for Reflective Essays.
Proceedings of the KI 2023: Advances in Artificial Intelligence, 2023

Solving Modal Logic Problems by Translation to Higher-Order Logic.
Proceedings of the Logic and Argumentation - 5th International Conference, 2023

Theorem Proving in Dependently-Typed Higher-Order Logic.
Proceedings of the Automated Deduction - CADE 29, 2023

2022
Collaborative Speculations on Future Themes for Participatory Design in Germany.
i-com, 2022

Solving QMLTP Problems by Translation to Higher-order Logic.
CoRR, 2022

Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers.
CoRR, 2022

Mathematical Proof Between Generations.
CoRR, 2022

A Simplified Variant of Gödel's Ontological Argument.
CoRR, 2022

Automation of Boolos' Curious Inference in Isabelle/HOL.
Arch. Formal Proofs, 2022

Automated Reasoning in Non-classical Logics in the TPTP World.
Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11, 2022

Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results.
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), 2022

2021
Leo-III - A Theorem Prover for Higher-Order Logic.
Dataset, January, 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).
Theory Pract. Log. Program., 2021

Extensional Higher-Order Paramodulation in Leo-III.
J. Autom. Reason., 2021

Modeling and Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy.
CoRR, 2021

Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL.
Arch. Formal Proofs, 2021

Exploring Simplified Variants of Gödel's Ontological Argument in Isabelle/HOL.
Arch. Formal Proofs, 2021

Value-Oriented Legal Argumentation in Isabelle/HOL.
Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

A German Corpus of Reflective Sentences.
Proceedings of the 18th International Conference on Natural Language Processing (ICON 2021), National Institute of Technology Silchar, Silchar, India, December 16, 2021

2020
Leo-III 1.5 - A Theorem Prover for Higher-Order Logic.
Dataset, October, 2020

Mechanizing Principia Logico-Metaphysica in Functional Type-Theory.
Rev. Symb. Log., 2020

Automating Free Logic in HOL, with an Experimental Application in Category Theory.
J. Autom. Reason., 2020

Higher-order Logic as Lingua Franca - Integrating Argumentative Discourse and Deep Logical Analysis.
CoRR, 2020

Encoding Legal Balancing: Automating an Abstract Ethico-Legal Value Ontology in Preference Logic.
CoRR, 2020

On Reductions of Hintikka Sets for Higher-Order Logic.
CoRR, 2020

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

Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support.
Artif. Intell., 2020

A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument.
Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, 2020

Positive Free Higher-Order Logic and Its Automation via a Semantical Embedding.
Proceedings of the KI 2020: Advances in Artificial Intelligence, 2020

Reasonable Machines: A Research Manifesto.
Proceedings of the KI 2020: Advances in Artificial Intelligence, 2020

The Higher-Order Prover Leo-III.
Proceedings of the ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020, 2020

Normative Reasoning with Expressive Logic Combinations.
Proceedings of the ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020, 2020

Public Announcement Logic in HOL.
Proceedings of the Dynamic Logic. New Trends and Applications, 2020

Computer-Supported Analysis of Arguments in Climate Engineering.
Proceedings of the Logic and Argumentation - Third International Conference, 2020

Computer-Supported Exploration of a Categorical Axiomatization of Modeloids.
Proceedings of the Relational and Algebraic Methods in Computer Science, 2020

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

åqvist's Dyadic Deontic Logic E in HOL.
FLAP, 2019

I/O Logic in HOL.
FLAP, 2019

Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument.
CoRR, 2019

A Computational-Hermeneutic Approach for Conceptual Explicitation.
CoRR, 2019

Computer Science and Metaphysics: A Cross-Fertilization.
CoRR, 2019

Designing Normative Theories of Ethical Reasoning: Formal Framework, Methodology, and Tool Support.
CoRR, 2019

Report on the Second International Joint Conference on Rules and Reasoning.
AI Mag., 2019

Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories.
Proceedings of the PRICAI 2019: Trends in Artificial Intelligence, 2019

The Higher-Order Prover Leo-III (Extended Abstract).
Proceedings of the KI 2019: Advances in Artificial Intelligence, 2019

Modelling the US Constitution to Establish Constitutional Dictatorship.
Proceedings of the 4th International Workshop on MIning and REasoning with Legal texts co-located with the 32nd International Conference on Legal Knowledge and Information Systems (JURIX 2019), 2019

Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations.
Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

2018
First Experiments with a Flexible Infrastructure for Normative Reasoning.
CoRR, 2018

I/O Logic in HOL - First Steps.
CoRR, 2018

Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL.
CoRR, 2018

Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL.
Arch. Formal Proofs, 2018

Axiom Systems for Category Theory in Free Logic.
Arch. Formal Proofs, 2018

A Dyadic Deontic Logic in HOL.
Proceedings of the Deontic Logic and Normative Systems - 14th International Conference, 2018

Computational Hermeneutics: An Integrated Approach for the Logical Analysis of Natural-Language Arguments.
Proceedings of the Dynamics, 2018

A Deontic Logic Reasoning Infrastructure.
Proceedings of the Sailing Routes in the World of Computation, 2018

System Demonstration: The Higher-Order Prover Leo-III.
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), 2018

2017
Computer-Assisted Analysis of the Anderson-Hájek Ontological Controversy.
Logica Universalis, 2017

Cut-Elimination for Quantified Conditional Logic.
J. Philos. Log., 2017

Universal Reasoning, Rational Argumentation and Human-Machine Interaction.
CoRR, 2017

Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument.
Arch. Formal Proofs, 2017

Types, Tableaus and Gödel's God in Isabelle/HOL.
Arch. Formal Proofs, 2017

Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract).
Proceedings of the Formal Methods: Foundations and Applications - 20th Brazilian Symposium, 2017

Capability Discovery for Automated Reasoning Systems.
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Going Polymorphic - TH1 Reasoning for Leo-III.
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Theorem Provers For Every Normal Modal Logic.
Proceedings of the LPAR-21, 2017

Leo-III Version 1.1 (System description).
Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic.
Proceedings of the KI 2017: Advances in Artificial Intelligence, 2017

2016
Axiomatizing Category Theory in Free Logic.
CoRR, 2016

Einsatz von Theorembeweisern in der Lehre.
Proceedings of the Hochschuldidaktik der Informatik, 2016

Translating Higher-Order Modal Logic from RuleML to TPTP.
Proceedings of the Supplementary Proceedings of the RuleML 2016 Challenge, 2016

The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics.
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, 2016

Agent-Based HOL Reasoning.
Proceedings of the Mathematical Software - ICMS 2016, 2016

Automating Free Logic in Isabelle/HOL.
Proceedings of the Mathematical Software - ICMS 2016, 2016

Is It Reasonable to Employ Agents in Automated Theorem Proving?.
Proceedings of the 8th International Conference on Agents and Artificial Intelligence (ICAART 2016), 2016

Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL.
Proceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19, 2016

Effective Normalization Techniques for HOL.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

TPTP and Beyond: Representation of Quantified Non-Classical Logics.
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)., 2016

2015
The Higher-Order Prover Leo-II.
J. Autom. Reason., 2015

Systematic Verification of the Modal Logic Cube in Isabelle/HOL.
Proceedings of the Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, 2015

Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2015

Higher-Order Modal Logics: Automation and Applications.
Proceedings of the Reasoning Web. Web Logic Rules - 11th International Summer School 2015, Berlin, Germany, July 31, 2015

LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

There Is No Best \beta -Normalization Strategy for Higher-Order Reasoners.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Proofs and Reconstructions.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Interacting with Modal Logics in the Coq Proof Assistant.
Proceedings of the Computer Science - Theory and Applications, 2015

2014
Automation of Higher-Order Logic.
Proceedings of the Computational Logic, 2014

On Logic Embeddings and Gödel's God.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2014

Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers.
Proceedings of the ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic, 2014

HOL Provers for First-order Modal Logics - Experiments.
Proceedings of the Automated Reasoning in Quantified Non-Classical Logics, 2014

2013
Quantified Multimodal Logics in Simple Type Theory.
Logica Universalis, 2013

Update report: LEO-II version 1.5
CoRR, 2013

Formalization, Mechanization and Automation of Gödel's Proof of God's Existence.
CoRR, 2013

Sigma: An integrated development environment for formal ontology.
AI Commun., 2013

Gödel's God in Isabelle/HOL.
Arch. Formal Proofs, 2013

HOL Based First-Order Modal Logic Provers.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Automating Quantified Conditional Logics in HOL.
Proceedings of the IJCAI 2013, 2013

A Top-down Approach to Combining Logics.
Proceedings of the ICAART 2013, 2013

LEO-II Version 1.5.
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012
Higher-order aspects and context in SUMO.
J. Web Semant., 2012

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

Quantified Conditional Logics are Fragments of HOL
CoRR, 2012

Embedding and automating conditional logics in classical higher-order logic.
Ann. Math. Artif. Intell., 2012

Understanding LEO-II's proofs.
Proceedings of the IWIL 2012: The 9th International Workshop on the Implementation of Logics, 2012

Implementing and Evaluating Provers for First-order Modal Logics.
Proceedings of the ECAI 2012, 2012

Implementing Different Proof Calculi for First-order Modal Logics.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

2011
Resource-Bounded Modelling and Analysis of Human-Level Interactive Proofs.
Proceedings of the Resource-Adaptive Cognitive Processes, 2011

ΩMEGA: Resource-Adaptive Processes in an Automated Reasoning System.
Proceedings of the Resource-Adaptive Cognitive Processes, 2011

Combining and automating classical and non-classical logics in classical higher-order logics.
Ann. Math. Artif. Intell., 2011

2010
Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure.
J. Formaliz. Reason., 2010

Multimodal and intuitionistic logics in simple type theory.
Log. J. IGPL, 2010

Simple Type Theory as Framework for Combining Logics.
CoRR, 2010

Combining Logics in Simple Type Theory.
Proceedings of the Computational Logic in Multi-Agent Systems, 11th International Workshop, 2010

Adaptive Assertion-Level Proofs.
Proceedings of the Workshop on Evaluation Methods for Solvers, 2010

Progress in Automating Higher-Order Ontology Reasoning.
Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, 2010

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

2009
Jacques Herbrand: Life, Logic, and Automated Deduction.
Proceedings of the Logic from Russell to Church, 2009

Automating Quantified Multimodal Logics in Simple Type Theory -- A Case Study
CoRR, 2009

Lectures on Jacques Herbrand as a Logician
CoRR, 2009

Cut-Simulation and Impredicativity
Log. Methods Comput. Sci., 2009

A remark on higher order RUE-resolution with EXTRUE
CoRR, 2009

Resource Adaptive Agents in Interactive Theorem Proving
CoRR, 2009

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

Automating Access Control Logics in Simple Type Theory with LEO-II.
Proceedings of the Emerging Challenges for Security, 2009

Presenting Proofs with Adapted Granularity.
Proceedings of the KI 2009: Advances in Artificial Intelligence, 2009

Proof Granularity as an Empirical Problem?
Proceedings of the CSEDU 2009 - Proceedings of the First International Conference on Computer Supported Education, Lisboa, Portugal, March 23-26, 2009, 2009

Progress in the Development of Automated Theorem Proving for Higher-Order Logic.
Proceedings of the Automated Deduction, 2009

Granularity-Adaptive Proof Presentation.
Proceedings of the Artificial Intelligence in Education: Building Learning Systems that Care: From Knowledge Representation to Affective Modelling, 2009

2008
Organization, Transformation, and Propagation of Mathematical Knowledge in Omegamega.
Math. Comput. Sci., 2008

Combined reasoning by automated cooperation.
J. Appl. Log., 2008

Preface.
Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, 2008

Evaluation of Systems for Higher-order Logic (ESHOL).
Proceedings of the First International Workshop on Practical Aspects of Automated Reasoning, 2008

THF0 - The Core of the TPTP Language for Higher-Order Logic.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description).
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
Deep Inference for Automated Proof Tutoring?
Proceedings of the KI 2007: Advances in Artificial Intelligence, 2007

2006
Computer supported mathematics with Omegamega.
J. Appl. Log., 2006

Towards computer aided mathematics.
J. Appl. Log., 2006

PlatOmega: A Mediator between Text-Editors and Proof Assistance Systems.
Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 2006

LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)
CoRR, 2006

Omega.
Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

A corpus of tutorial dialogs on theorem proving; the influence of the presentation of the study-material.
Proceedings of the Fifth International Conference on Language Resources and Evaluation, 2006

DiaWOz-II - A Tool for Wizard-of-Oz Experiments in Mathematics.
Proceedings of the KI 2006: Advances in Artificial Intelligence, 2006

An Agent-Based Architecture for Dialogue Systems.
Proceedings of the Perspectives of Systems Informatics, 2006

Cut-Simulation in Impredicative Logics.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005
A Structured Set of Higher-Order Problems.
Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity.
Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

Natural Language Dialog with a Tutor System for Mathematical Proofs.
Proceedings of the Cognitive Systems, Joint Chinese-German Workshop, Shanghai, 2005

Bridging Theorem Proving and Mathematical Knowledge Retrieval.
Proceedings of the Mechanizing Mathematical Reasoning, 2005

Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs.
Proceedings of the Proceedings, 2005

2004
Higher-order semantics and extensionality.
J. Symb. Log., 2004

An Annotated Corpus of Tutorial Dialogs on Mathematical Theorem Proving.
Proceedings of the Fourth International Conference on Language Resources and Evaluation, 2004

Can a Higher-Order and a First-Order Theorem Prover Cooperate?.
Proceedings of the Logic for Programming, 2004

Omega: Computer Supported Mathematics.
Proceedings of the KI 2004: Advances in Artificial Intelligence, 2004

2003
Automatic Learning of Proof Methods in Proof Planning.
Log. J. IGPL, 2003

Interactive Theorem Proving with Tasks.
Proceedings of the User Interfaces for Theorem Provers Workshop, 2003

Assertion-level Proof Representation with Under-Specification.
Proceedings of the Mathematical Knowledge Management Symposium, 2003

Assertion Application in Theorem Proving and Proof Planning.
Proceedings of the IJCAI-03, 2003

2002
Comparing Approaches To Resolution Based Higher-Order Theorem Proving.
Synth., 2002

Proof Development with Omega-MEGA: sqrt(2) Is Irrational.
Proceedings of the Logic for Programming, 2002


2001
Experiments with an Agent-Oriented Reasoning System.
Proceedings of the KI 2001: Advances in Artificial Intelligence, 2001

2000
Resource Guided Concurrent Deduction.
Proceedings of the Seventh Workshop on Automated Reasoning, 2000

1999
Equality and extensionality in automated higher order theorem proving.
PhD thesis, 1999

Integrating Tps and Omega.
J. Univers. Comput. Sci., 1999

<i>L</i><Omega><i>UI</i>: <i>L</i>ovely <Omega>MEGA <i>U</i>ser <i>I</i>nterface.
Formal Aspects Comput., 1999

Agent based mathematical reasoning.
Proceedings of the Systems for Integrated Computation and Deduction, 1999

Critical Agents Supporting Interactive Theorem Proving.
Proceedings of the Progress in Artificial Intelligence, 1999

Extensional Higher-Order Paramodulation and RUE-Resolution.
Proceedings of the Automated Deduction, 1999

1998
System Description: LEO - A Higher-Order Theorem Prover.
Proceedings of the Automated Deduction, 1998

Extensional Higher-Order Resolution.
Proceedings of the Automated Deduction, 1998

A Blackboard Architecture for Guiding Interactive Proofs.
Proceedings of the Artificial Intelligence: Methodology, 1998

1997


  Loading...