Automated Reasoning for Robot Ethics

TL;DR

This paper demonstrates how standard deontic logic can model ethical codes in multi-agent systems and utilizes the Hyper theorem prover to verify properties of these codes, advancing automated ethical reasoning.

Contribution

It introduces a method to apply deontic logic to model and verify ethical codes in multi-agent systems using the Hyper theorem prover.

Findings

Deontic logic effectively models ethical codes.

Hyper prover can verify properties of ethical codes.

The approach supports automated ethical reasoning in multi-agent systems.

Abstract

Deontic logic is a very well researched branch of mathematical logic and philosophy. Various kinds of deontic logics are considered 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 used to model ethical codes for multi-agent systems. Furthermore we show how Hyper, a high performance theorem prover, can be used to prove properties of these ethical codes.