Automated Reasoning in Deontic Logic

ABSTRACT. Deontic logic is a very well researched branch of mathematical logic and philosophy. Various kinds of deontic logics are discussed for different applications like argumentation theory, legal reasoning and actions in multi-agent systems. Recently there also is growing interest in modelling human reasoning and testing the models with psychological findings. Deontic logic is an obvious tool to this end, because norms and licenses in human societies can be described easily. This paper concentrates on automated reasoning in deontic logic. We show that deontic logic can be translated into the description logic ALC, for which the first oder reasoning system Hyper offers a decision procedure.