Christoph Benzmüller

research

∙ 01/25/2023

Automated multilingual detection of Pro-Kremlin propaganda in newspapers and Telegram posts

The full-scale conflict between the Russian Federation and Ukraine gener...

0 Veronika Solopova, et al. ∙

research

∙ 12/19/2022

Solving QMLTP Problems by Translation to Higher-order Logic

This paper describes an evaluation of Automated Theorem Proving (ATP) sy...

0 Alexander Steen, et al. ∙

research

∙ 08/14/2022

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

This paper reports on an exploration of variants of Boolos' curious infe...

0 Christoph Benzmüller, et al. ∙

research

∙ 07/08/2022

Mathematical Proof Between Generations

A proof is one of the most important concepts of mathematics. However, t...

0 Jonas Bayer, et al. ∙

research

∙ 02/20/2022

Automated Reasoning in Non-classical Logics in the TPTP World

Non-classical logics are used in a wide spectrum of disciplines, includi...

0 Alexander Steen, et al. ∙

research

∙ 02/13/2022

A Simplified Variant of Gödel's Ontological Argument

A simplified variant of Gödel's ontological argument is presented. The s...

0 Christoph Benzmüller, et al. ∙

research

∙ 11/02/2021

Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy

A shallow semantical embedding for public announcement logic with relati...

0 Christoph Benzmüller, et al. ∙

research

∙ 10/02/2020

Public Announcement Logic in HOL

A shallow semantical embedding for public announcement logic with relati...

0 Sebastian Reiche, et al. ∙

research

∙ 08/14/2020

Reasonable Machines: A Research Manifesto

Future intelligent autonomous systems (IAS) are inevitably deciding on m...

0 Christoph Benzmüller, et al. ∙

research

∙ 07/02/2020

Higher-order Logic as Lingua Franca – Integrating Argumentative Discourse and Deep Logical Analysis

We present an approach towards the deep, pluralistic logical analysis of...

0 David Fuenmayor, et al. ∙

research

∙ 06/23/2020

Encoding Legal Balancing: Automating an Abstract Ethico-Legal Value Ontology in Preference Logic

Enabling machines to legal balancing is a non-trivial task challenged by...

0 Christoph Benzmüller, et al. ∙

research

∙ 04/16/2020

On Reductions of Hintikka Sets for Higher-Order Logic

Steen's (2018) Hintikka set properties for Church's type theory based on...

0 Alexander Steen, et al. ∙

research

∙ 01/14/2020

A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument

An approach to universal (meta-)logical reasoning in classical higher-or...

0 Christoph Benzmüller, et al. ∙

research

∙ 01/14/2020

A (Simplified) Supreme Being Necessarily Exists – Says the Computer!

A simplified variant of Kurt Gödel's modal ontological argument is prese...

0 Christoph Benzmüller, et al. ∙

research

∙ 10/27/2019

Computer-supported Exploration of a Categorical Axiomatization of Modeloids

A modeloid, a certain set of partial bijections, emerges from the idea t...

0 Lucca Tiemens, et al. ∙

research

∙ 10/20/2019

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

Three variants of Kurt Gödel's ontological argument, as proposed byDana ...

0 Christoph Benzmüller, et al. ∙

research

∙ 07/26/2019

Extensional Higher-Order Paramodulation in Leo-III

Leo-III is an automated theorem prover for extensional type theory with ...

0 Alexander Steen, et al. ∙

research

∙ 06/15/2019

A Computational-Hermeneutic Approach for Conceptual Explicitation

We present a computer-supported approach for the logical analysis and co...

0 David Fuenmayor, et al. ∙

research

∙ 05/01/2019

Computer Science and Metaphysics: A Cross-Fertilization

Computational philosophy is the use of mechanized computational techniqu...

0 Daniel Kirchner, et al. ∙

research

∙ 03/25/2019

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

The area of formal ethics is experiencing a shift from a unique or stand...

0 Christoph Benzmüller, et al. ∙

research

∙ 03/23/2019

Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories

An ambitious explicit ethical theory, Gewirth's Principle of Generic Con...

0 David Fuenmayor, et al. ∙

research

∙ 04/09/2018

First Experiments with a Flexible Infrastructure for Normative Reasoning

A flexible infrastructure for normative reasoning is outlined. A small-s...

0 Christoph Benzmüller, et al. ∙

research

∙ 03/26/2018

I/O Logic in HOL --- First Steps

A semantical embedding of input/output logic in classical higher-order l...

0 Christoph Benzmüller, et al. ∙

research

∙ 02/23/2018

Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL

A shallow semantical embedding of a dyadic deontic logic by Carmo and Jo...

0 Christoph Benzmüller, et al. ∙

research

∙ 02/08/2018

The Higher-Order Prover Leo-III (Extended Version)

The automated theorem prover Leo-III for classical higher-order logic wi...

0 Alexander Steen, et al. ∙

research

∙ 02/08/2018

The Higher-Order Prover Leo-III

The automated theorem prover Leo-III for classical higher-order logic wi...

0 Alexander Steen, et al. ∙

research

∙ 11/16/2017

Mechanizing Principia Logico-Metaphysica in Functional Type Theory

Principia Logico-Metaphysica proposes a foundational logical theory for ...

0 Daniel Kirchner, et al. ∙

research

∙ 03/28/2017

Universal Reasoning, Rational Argumentation and Human-Machine Interaction

Classical higher-order logic, when utilized as a meta-logic in which var...

0 Christoph Benzmüller, et al. ∙

research

∙ 09/06/2016

Axiomatizing Category Theory in Free Logic

Starting from a generalization of the standard axioms for a monoid we pr...

0 Christoph Benzmüller, et al. ∙

research

∙ 07/31/2015

Systematic Verification of the Modal Logic Cube in Isabelle/HOL

We present an automated verification of the well-known modal logic cube ...

0 Christoph Benzmüller, et al. ∙

research

∙ 05/07/2015

LeoPARD --- A Generic Platform for the Implementation of Higher-Order Reasoners

LeoPARD supports the implementation of knowledge representation and reas...

0 Max Wisniewski, et al. ∙

research

∙ 08/21/2013

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

Gödel's ontological proof has been analysed for the first-time with an u...

0 Christoph Benzmüller, et al. ∙

research

∙ 03/15/2013

Update report: LEO-II version 1.5

Recent improvements of the LEO-II theorem prover are presented. These im...

0 Christoph Benzmüller, et al. ∙

Christoph Benzmüller

Featured Co-authors