In this article we introduce a logical structure for normative reasoning, called Normative Detachment Structure with Ideal Conditions, that can be used to represent the content of certain legal texts in a normalized way. The structure exploits the deductive properties of a system of bimodal logic able to distinguish between ideal and actual normative statements, as well as a novel formalization of conditional normative statements able to capture interesting cases of contrary-to-duty reasoning and to avoid deontic paradoxes. Furthermore, we illustrate (...) how the theoretical framework proposed can be mechanized to get an automated procedure of query-answering on an example of legal text. (shrink)

In the present work we illustrate how two sorts of defeasible reasoning that are fundamental in the normative domain, that is, reasoning about exceptions and reasoning about violations, can be simulated via monotonic propositional theories based on a bimodal language with primitive operators representing knowledge and obligation. The proposed theoretical framework paves the way to using native theorem provers for multimodal logic, such as MleanCoP, in order to automate normative reasoning.