Automated Reasoning in Deontic Logic
  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.
