Automated Reasoning in Deontic Logic
This work addresses the challenge of applying automated reasoning to deontic logic for domains like legal reasoning and multi-agent systems, but it appears incremental as it adapts existing methods to a specific logic.
The paper tackled the problem of automating reasoning in deontic logic by transforming it into description logic and DL-clauses, enabling processing with the Hyper theorem prover, and demonstrated this through two use cases in multi-agent systems and normative systems.
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.