Detachment in Normative Systems: Examples, Inference Patterns, Properties

in IfCoLog Journal of Logics and Their Applications (2022), 9(4), 1019-1062

There is a variety of ways to reason with normative systems. This partly reflects a variety of semantics developed for deontic logic, such as traditional semantics based on possible worlds, or alternative ... [more ▼]

There is a variety of ways to reason with normative systems. This partly reflects a variety of semantics developed for deontic logic, such as traditional semantics based on possible worlds, or alternative semantics based on algebraic methods, explicit norms or techniques from non-monotonic logic. This diversity raises the question how these reasoning methods are related, and which reasoning method should be chosen for a particular application. In this paper we discuss the use of examples, inference patterns, and more abstract properties. First, benchmark examples can be used to compare ways to reason with normative systems. We give an overview of several benchmark examples of normative reasoning and deontic logic: van Fraassen’s paradox, Forrester’s paradox, Prakken and Sergot’s cottage regulations, Jeffrey’s disarmament example, Chisholm’s paradox, Makinson’s Möbius strip, and Horty’s priority examples. Moreover, we distinguish various interpretations that can be given to these benchmark examples, such as consistent interpretations, dilemma interpretations, and violability interpretations. Second, inference patterns can be used to compare different ways to reason with normative systems. Instead of analysing the benchmark examples semantically, as it is usually done, in this paper we use inference patterns to analyse them at a higher level of abstraction. We discuss inference patterns reflecting typical logical properties such as strengthening of the antecedent or weakening of the consequent. Third, more abstract properties can be defined to compare different ways to reason with normative systems. To define these more abstract properties, we first present a formal framework around the notion of detachment. Some of the ten properties we introduce are derived from the inference patterns, but others are more abstract: factual detachment, violation detection, substitution, replacements of equivalents, implication, para-consistency, conjunction, factual monotony, norm monotony, and norm induction. We consider these ten properties as desirable for a reasoning method for normative systems, and thus they can be used also as requirements for the further development of formal methods for normative systems and deontic logic. [less ▲]

Report on the Second International Joint Conference on Rules and Reasoning

in AI Magazine (2019), 40(2), 73-74

Åqvist's Dyadic Deontic Logic E in HOL

in IfCoLog Journal of Logics and Their Applications (2019), 6(5), 733--755

A geometrical view of I/O logic

Report (2019)

Aqvist's Dyadic Deontic Logic E in HOL

Scientific Conference (2018, September 17)

We devise a shallow semantical embedding of \AA{}qvist's dyadic deontic logic {\bf E} in classical higher-order logic. This embedding is encoded in Isabelle/HOL, which turns this system into a proof ... [more ▼]

We devise a shallow semantical embedding of \AA{}qvist's dyadic deontic logic {\bf E} in classical higher-order logic. This embedding is encoded in Isabelle/HOL, which turns this system into a proof assistant for deontic logic reasoning. The experiments with this environment provide evidence that this logic \textit{implementation} fruitfully enables interactive and automated reasoning at the meta-level and the object-level. [less ▲]

A Faithful Semantic Embedding of the Dyadic Deontic Logic E in HOL

Poster (2018, June 16)

Implementation of Dyadic Deontic Logic E in Isabelle/HOL

Scientific Conference (2018, May 04)

We have devised a shallow semantical embedding of a dyadic deontic logic (by B.Hansson and \AA{}qvist) in classical higher-order logic. This embedding has been encoded in Isabelle/HOL, which turns this ... [more ▼]

We have devised a shallow semantical embedding of a dyadic deontic logic (by B.Hansson and \AA{}qvist) in classical higher-order logic. This embedding has been encoded in Isabelle/HOL, which turns this system into a proof assistant for deontic logic reasoning. The experiments with this environment provide evidence that this logic \textit{implementation} fruitfully enables interactive and automated reasoning at the meta-level and the object-level. [less ▲]

First Experiments with a Flexible Infrastructure for Normative Reasoning

E-print/Working paper (2018)

A flexible infrastructure for normative reasoning is outlined. A small-scale demonstrator version of the envisioned system has been implemented in the proof assistant Isabelle/HOL by utilising the first ... [more ▼]

A flexible infrastructure for normative reasoning is outlined. A small-scale demonstrator version of the envisioned system has been implemented in the proof assistant Isabelle/HOL by utilising the first authors universal logical reasoning approach based on shallow semantical embeddings in meta-logic HOL. The need for such a flexible reasoning infrastructure is motivated and illustrated with a contrary-to-duty example scenario selected from the General Data Protection Regulation. [less ▲]

Input/output logics with a consistency check

in Pigozzi, Gabriella; Broersen, Jan; Condoravdi, Cleo (Eds.) et al Deontic Logic and Normative Systems (DEON 2018) (2018)

Norm-based semantics to deontic logic typically come in an unconstrained and constrained version, where the unconstrained version comes with a proof system, and the constraints handle phenomena such as ... [more ▼]

Norm-based semantics to deontic logic typically come in an unconstrained and constrained version, where the unconstrained version comes with a proof system, and the constraints handle phenomena such as dilemmas, contrary-to-duty reasoning, uncertaintyanddefeasibility. Thisisanalogoustotheuseofrule-basedlanguagesin non-monotonic logic such as logic programming or default logic, but in contrast to the traditional modal framework. Traditionally, for example, specific modal deontic logics have been defined that make dilemmas inconsistent, as well as other modal deontic logics representing dilemmas in a consistent way. This issue was raised recently in the input/output logic framework, and weaker unconstrained logics have been defined handling phenomena like dilemmas and contrary-to-duty reasoning. In this paper we introduce a semantics and proof theory for a system with various desirable properties. We show that our new deontic logic satisfies a criterion posed several years ago by Broersen and van der Torre, allowing deontic detachment while preventing Prakken and Sergot’s pragmatic oddities as well as Sergot’s drowning problem. [less ▲]

A Model for Regulating of Ethical Preferences in Machine Ethics

in Proceedings of International Conference on Human-Computer Interaction (2018)