research
∙
08/21/2023
Normative Conditional Reasoning as a Fragment of HOL
We report some results regarding the mechanization of normative (prefere...
share
research
∙
07/10/2023
PapagAI:Automated Feedback for Reflective Essays
Written reflective practice is a regular exercise pre-service teachers p...
research
∙
06/15/2023
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
This paper presents meta-logical investigations based on category theory...
research
∙
05/24/2023
Theorem Proving in Dependently-Typed Higher-Order Logic – Extended Preprint
Higher-order logic HOL offers a very simple syntax and semantics for rep...
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...
research
∙
12/19/2022
Solving QMLTP Problems by Translation to Higher-order Logic
This paper describes an evaluation of Automated Theorem Proving (ATP) sy...
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...
research
∙
07/08/2022
Mathematical Proof Between Generations
A proof is one of the most important concepts of mathematics. However, t...
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...
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...
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...
research
∙
10/02/2020
Public Announcement Logic in HOL
A shallow semantical embedding for public announcement logic with relati...
research
∙
08/14/2020
Reasonable Machines: A Research Manifesto
Future intelligent autonomous systems (IAS) are inevitably deciding on m...
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...
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...
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...
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...
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...
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...
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 ...
research
∙
07/26/2019
Extensional Higher-Order Paramodulation in Leo-III
Leo-III is an automated theorem prover for extensional type theory with ...
research
∙
06/15/2019
A Computational-Hermeneutic Approach for Conceptual Explicitation
We present a computer-supported approach for the logical analysis and co...
research
∙
05/01/2019
Computer Science and Metaphysics: A Cross-Fertilization
Computational philosophy is the use of mechanized computational techniqu...
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...
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...
research
∙
04/09/2018
First Experiments with a Flexible Infrastructure for Normative Reasoning
A flexible infrastructure for normative reasoning is outlined. A small-s...
research
∙
03/26/2018
I/O Logic in HOL --- First Steps
A semantical embedding of input/output logic in classical higher-order l...
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...
research
∙
02/08/2018
The Higher-Order Prover Leo-III (Extended Version)
The automated theorem prover Leo-III for classical higher-order logic wi...
research
∙
02/08/2018
The Higher-Order Prover Leo-III
The automated theorem prover Leo-III for classical higher-order logic wi...
research
∙
11/16/2017
Mechanizing Principia Logico-Metaphysica in Functional Type Theory
Principia Logico-Metaphysica proposes a foundational logical theory for ...
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...
research
∙
09/06/2016
Axiomatizing Category Theory in Free Logic
Starting from a generalization of the standard axioms for a monoid we pr...
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 ...
research
∙
05/07/2015
LeoPARD --- A Generic Platform for the Implementation of Higher-Order Reasoners
LeoPARD supports the implementation of knowledge representation and reas...
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...
research
∙
03/15/2013