Automated Reasoning in Deontic Logic

TL;DR

This paper presents a method to transform standard deontic logic into description logic and DL-clauses, enabling the use of high-performance theorem proving for applications in multi-agent systems and normative systems.

Contribution

It introduces a stepwise transformation process from deontic logic to description logic, facilitating automated reasoning with Hyper theorem prover.

Findings

Successful transformation of deontic logic into description logic

Application of Hyper theorem prover to two real-world use cases

Enhanced reasoning capabilities in multi-agent and normative system contexts

Abstract

Deontic logic is a very well researched branch of mathematical logic and philosophy. Various kinds of deontic logics are discussed for different application domains like argumentation theory, legal reasoning, and acts in multi-agent systems. In this paper, we show how standard deontic logic can be stepwise transformed into description logic and DL- clauses, such that it can be processed by Hyper, a high performance theorem prover which uses a hypertableau calculus. Two use cases, one from multi-agent research and one from the development of normative system are investigated.