Automated Reasoning with Complex Ethical Theories--A Case Study Towards Responsible AI

in 16th International Congress on Logic, Methodology and Philosophy of Science and Technology (CLMPST 2019) --- Bridging across Academic Cultures, Book of Abstracts (2019)

Aqvist's Dyadic Deontic Logic E in HOL

Scientific Conference (2018, September 17)

We devise a shallow semantical embedding of \AA{}qvist's dyadic deontic logic {\bf E} in classical higher-order logic. This embedding is encoded in Isabelle/HOL, which turns this system into a proof ... [more ▼]

We devise a shallow semantical embedding of \AA{}qvist's dyadic deontic logic {\bf E} in classical higher-order logic. This embedding is encoded in Isabelle/HOL, which turns this system into a proof assistant for deontic logic reasoning. The experiments with this environment provide evidence that this logic \textit{implementation} fruitfully enables interactive and automated reasoning at the meta-level and the object-level. [less ▲]

ARQNL 2018 Automated Reasoning in Quantified Non-Classical Logics

in CEUR Workshop Proceedings (2018), 2095

A Dyadic Deontic Logic in HOL

in Broersen, Jan; Condoravdi, Cleo; Nair, Shyam (Eds.) et al Deontic Logic and Normative Systems --- 14th International Conference, DEON 2018, Utrecht, The Netherlands, 3-6 July, 2018 (2018, June 11)

A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. This embedding is proven sound and complete, that is, faithful. The work presented ... [more ▼]

A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. This embedding is proven sound and complete, that is, faithful. The work presented here provides the theoretical foundation for the implementation and automation of dyadic deontic logic within off-the-shelf higher-order theorem provers and proof assistants. [less ▲]

Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL

Report (2018)

A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. This embedding is proven sound and complete, that is, faithful. The work presented ... [more ▼]

A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. This embedding is proven sound and complete, that is, faithful. The work presented here provides the theoretical foundation for the implementation and automation of dyadic deontic logic within off-the-shelf higher-order theorem provers and proof assistants. [less ▲]

First Experiments with a Flexible Infrastructure for Normative Reasoning

E-print/Working paper (2018)

A flexible infrastructure for normative reasoning is outlined. A small-scale demonstrator version of the envisioned system has been implemented in the proof assistant Isabelle/HOL by utilising the first ... [more ▼]

A flexible infrastructure for normative reasoning is outlined. A small-scale demonstrator version of the envisioned system has been implemented in the proof assistant Isabelle/HOL by utilising the first authors universal logical reasoning approach based on shallow semantical embeddings in meta-logic HOL. The need for such a flexible reasoning infrastructure is motivated and illustrated with a contrary-to-duty example scenario selected from the General Data Protection Regulation. [less ▲]

The Higher-Order Prover Leo-III

in Automated Reasoning 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings (2018)

Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL

in Archive of Formal Proofs (2018)

An ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency"--- is encoded and analysed in Isabelle/HOL. Gewirth's theory has stirred much attention in philosophy and ethics and has ... [more ▼]

An ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency"--- is encoded and analysed in Isabelle/HOL. Gewirth's theory has stirred much attention in philosophy and ethics and has been proposed as a potential means to bound the impact of artificial general intelligence. [less ▲]

Axiom Systems for Category Theory in Free Logic

in Archive of Formal Proofs (2018)

A Deontic Logic Reasoning Infrastructure

in Sailing Routes in the World of Computation, 14th Conference on Computability in Europe, CiE 2018, Kiel, Germany, July 30 – August 3, 2018, Proceedings (2018)

A flexible infrastructure for the automation of deontic and normative reasoning is presented. Our motivation is the development, study and provision of legal and moral reasoning competencies in future ... [more ▼]

A flexible infrastructure for the automation of deontic and normative reasoning is presented. Our motivation is the development, study and provision of legal and moral reasoning competencies in future intelligent machines. Since there is no consensus on the “best” deontic logic formalisms and since the answer may be application specific, a flexible infrastructure is proposed in which candidate logic formalisms can be varied, assessed and compared in experimental ethics application studies. Our work thus links the historically rich research areas of classical higher-order logic, deontic logics, normative reasoning and formal ethics. [less ▲]