
Public Announcement Logic in HOL
A shallow semantical embedding for public announcement logic with relati...
read it

Reasonable Machines: A Research Manifesto
Future intelligent autonomous systems (IAS) are inevitably deciding on m...
read it

Higherorder Logic as Lingua Franca – Integrating Argumentative Discourse and Deep Logical Analysis
We present an approach towards the deep, pluralistic logical analysis of...
read it

Encoding Legal Balancing: Automating an Abstract EthicoLegal Value Ontology in Preference Logic
Enabling machines to legal balancing is a nontrivial task challenged by...
read it

On Reductions of Hintikka Sets for HigherOrder Logic
Steen's (2018) Hintikka set properties for Church's type theory based on...
read it

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 higheror...
read it

A (Simplified) Supreme Being Necessarily Exists – Says the Computer!
A simplified variant of Kurt Gödel's modal ontological argument is prese...
read it

Computersupported Exploration of a Categorical Axiomatization of Modeloids
A modeloid, a certain set of partial bijections, emerges from the idea t...
read it

Computersupported 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 ...
read it

Extensional HigherOrder Paramodulation in LeoIII
LeoIII is an automated theorem prover for extensional type theory with ...
read it

A ComputationalHermeneutic Approach for Conceptual Explicitation
We present a computersupported approach for the logical analysis and co...
read it

Computer Science and Metaphysics: A CrossFertilization
Computational philosophy is the use of mechanized computational techniqu...
read it

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...
read it

Harnessing HigherOrder (Meta)Logic to Represent and Reason with Complex Ethical Theories
An ambitious explicit ethical theory, Gewirth's Principle of Generic Con...
read it

First Experiments with a Flexible Infrastructure for Normative Reasoning
A flexible infrastructure for normative reasoning is outlined. A smalls...
read it

I/O Logic in HOL  First Steps
A semantical embedding of input/output logic in classical higherorder l...
read it

Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL
A shallow semantical embedding of a dyadic deontic logic by Carmo and Jo...
read it

The HigherOrder Prover LeoIII (Extended Version)
The automated theorem prover LeoIII for classical higherorder logic wi...
read it

The HigherOrder Prover LeoIII
The automated theorem prover LeoIII for classical higherorder logic wi...
read it

Mechanizing Principia LogicoMetaphysica in Functional Type Theory
Principia LogicoMetaphysica proposes a foundational logical theory for ...
read it

Universal Reasoning, Rational Argumentation and HumanMachine Interaction
Classical higherorder logic, when utilized as a metalogic in which var...
read it

Axiomatizing Category Theory in Free Logic
Starting from a generalization of the standard axioms for a monoid we pr...
read it

Systematic Verification of the Modal Logic Cube in Isabelle/HOL
We present an automated verification of the wellknown modal logic cube ...
read it

LeoPARD  A Generic Platform for the Implementation of HigherOrder Reasoners
LeoPARD supports the implementation of knowledge representation and reas...
read it

Formalization, Mechanization and Automation of Gödel's Proof of God's Existence
Gödel's ontological proof has been analysed for the firsttime with an u...
read it

Update report: LEOII version 1.5
Recent improvements of the LEOII theorem prover are presented. These im...
read it
Christoph Benzmüller
is this you? claim profile
University of Luxembourg, FSTC (Visiting Scholar). Freie Universität Berlin, Dep. of Maths and CS (Outside Lecturer). Saarland University, Dep. CS (Outside Lecturer).