A Kelsenian Deontic Logic

Inspired by Kelsen’s view that norms establish causal-like connections between facts and sanctions, we develop a deontic logic in which a proposition is obligatory iff its complement causes a violation. We provide a logic for normative causality, define non-contextual and contextual notions of illicit and duty, and show that the logic of such duties is well-behaved and solves the main deontic paradoxes.

Timed Dyadic Deontic Logic

In this paper, we introduce TDDL, a timed dyadic deontic logic. Our starting point is a version of a dyadic deontic logic with conditional obligations, permissions, and obligations, and with a “reparation” operator for representing contrary-to-duties and contrary-to-prohibitions. We also consider a sequence operator allowing us to define norms as sequences of individual norms and most importantly with timed intervals, allowing us to express deadlines of norms. We provide a trace semantics capturing both satisfaction and violation of norms and discuss fulfillment of TDDL specifications.

Algorithmic Ethics: Formalization and Verification of Autonomous Vehicle Obligations

In this article, we develop a formal framework for automatic reasoning about the obligations of autonomous cyber-physical systems, including their social and ethical obligations. Obligations, permissions, and prohibitions are distinct from a system's mission, and are a necessary part of specifying advanced, adaptive AI-equipped systems. They need a dedicated deontic logic of obligations to formalize them. Most existing deontic logics lack corresponding algorithms and system models that permit automatic verification. We demonstrate how a particular deontic logic, Dominance Act Utilitarianism (DAU) [23], is a suitable starting point for formalizing the obligations of autonomous systems like self-driving cars. We demonstrate its usefulness by formalizing a subset of Responsibility-Sensitive Safety (RSS) in DAU; RSS is an industrial proposal for how self-driving cars should and should not behave in traffic. We show that certain logical consequences of RSS are undesirable, indicating a need to further refine the proposal. We also demonstrate how obligations can change over time, which is necessary for long-term autonomy. We then demonstrate a model-checking algorithm for DAU formulas on weighted transition systems and illustrate it by model-checking obligations of a self-driving car controller from the literature.

Formalizing commitments using the event calculus and RuleML

Smart Contracts enable the automated execution of exchanges on the blockchain. From an ontological perspective, smart contracts create and automate the fulfillment of social commitments between actors. Whereas traditional deontic logic is used to make a legal determination in contractual multi-actor interactions, this paper focuses on the consequences of these actions resulting from that determination, thereby shifting the focus from monitoring to execution. The interactions between actors and the consequences in terms of commitments have not yet been formalized for smart contracts. The perspective of smart contracts is interesting, since they are considered to be autonomous agents, able to generate automated actions. We use the Event Calculus as a formal logic to represent and reason about the effects of these automated actions and the resulting commitments. Since the Event Calculus deals with local events and the consideration of time, this approach enables the uniform representation of commitments, including their operations and reasoning rules.

An impossibility result on methodological individualism

Methodological individualists often claim that any social phenomenon can ultimately be explained in terms of the actions and interactions of individuals. Any Nagelian version of methodological individualism requires that there be bridge laws that translate social statements into individualistic ones. We show that Nagelian individualism can be put to logical scrutiny by making the relevant social and individualistic languages fully explicit and mathematically precise. In particular, we prove that the social statement that a group of (at least two) agents performs a deontically admissible group action cannot be expressed in a well-established deontic logic of agency that models every combination of actions, omissions, abilities, and obligations of finitely many individual agents.

On Computable Expressions of Policies for Digital Health: Use for Privacy Consent

This paper proposes a formal model for expressing policies in digital health. The aim is to support computable expressions of legislative, regulative and organizational policies. The model is grounded in the semantics of deontic logic [1] and in modelling concepts for expressing accountability, specified in the new RM-ODP Enterprise Language standard [2]. An example of privacy consent based on the FHIR consent resource [3] is used to explain the use of these modelling concepts. The example involves multiple stakeholders and illustrates the complexity associated with the use of machine learning and artificial intelligence systems as part of healthcare delivery governed by informed consent policies.