Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support

TL;DR

The paper introduces LogiKEy, a comprehensive framework and methodology for designing ethical and legal reasoning systems using higher-order logic, supported by powerful theorem proving tools for flexible experimentation.

Contribution

It presents a unifying formal framework based on semantical embeddings in HOL, enabling the development and testing of normative theories and ethical reasoners with tool support.

Findings

HOL's undecidability does not significantly hinder practical experimentation.

Tool support with theorem provers facilitates flexible logic and domain theory testing.

Case studies demonstrate effective application of the LogiKEy framework.

Abstract

A framework and methodology---termed LogiKEy---for the design and engineering of ethical reasoners, normative theories and deontic logics is presented. The overall motivation is the development of suitable means for the control and governance of intelligent autonomous systems. LogiKEy's unifying formal framework is based on semantical embeddings of deontic logics, logic combinations and ethico-legal domain theories in expressive classic higher-order logic (HOL). This meta-logical approach enables the provision of powerful tool support in LogiKEy: off-the-shelf theorem provers and model finders for HOL are assisting the LogiKEy designer of ethical intelligent agents to flexibly experiment with underlying logics and their combinations, with ethico-legal domain theories, and with concrete examples---all at the same time. Continuous improvements of these off-the-shelf provers, without further ado, leverage the reasoning performance in LogiKEy. Case studies, in which the LogiKEy framework and methodology has been applied and tested, give evidence that HOL's undecidability often does not hinder efficient experimentation.

Figures

Equations

$$◊\forall x.Px$$

$$s,t::=$$

$$\varphi ::=p\mid \neg \varphi \mid \varphi \wedge \varphi \mid \square \varphi \mid ◯(\varphi /\varphi )$$

$${\mathrm{opt}}_{⪰}(\Vert \varphi \Vert )$$

$$\displaystyle\phi\mbox{, where $\phi$ is a tautology from PL}$$

$$\square (\varphi \to \psi )\to (\square \varphi \to \square \psi )$$

$$\square \varphi \to \square \square \varphi$$

$$\neg \square \varphi \to \square \neg \square \varphi$$

$$◯(\psi \to \chi /\varphi )\to (◯(\psi /\varphi )\to ◯(\chi /\varphi ))$$

$$◯(\varphi /\varphi )$$

$$◯(\chi /(\varphi \wedge \psi ))\to ◯((\psi \to \chi )/\varphi )$$

$$◯(\psi /\varphi )\to \square ◯(\psi /\varphi )$$

$$\square \psi \to ◯(\psi /\varphi )$$

$$\square (\varphi \leftrightarrow \psi )\to (◯(\chi /\varphi )\leftrightarrow ◯(\chi /\psi ))$$

$$\text{mbox}If⊢\varphi \text{mbox}and⊢\varphi \to \psi \text{mbox}then⊢\psi$$

$$\text{mbox}If⊢\varphi \text{mbox}then⊢\square \varphi$$

$$\begin{array}[]{lcl}\lfloor\Box\phi\rfloor&=&\Box_{\tau\shortrightarrow\tau}\,\lfloor\phi\rfloor\\ \lfloor\bigcirc(\psi/\phi)\rfloor&=&\bigcirc_{\tau\shortrightarrow\tau\shortrightarrow\tau}\,\lfloor\psi\rfloor\lfloor\phi\rfloor\\ \end{array}$$

$$\begin{array}[]{ll}\Box_{\tau\shortrightarrow\tau}&=\lambda\phi_{\tau}.\lambda x_{i}.\forall y_{i}.(\phi\,y)\\ \bigcirc_{\tau\shortrightarrow\tau\shortrightarrow\tau}&=\lambda\psi_{\tau}.\lambda\phi_{\tau}.\lambda x_{i}.\forall w_{i}.((\lambda v_{i}.(\phi\,v\wedge(\forall y_{i}.(\phi\,y\rightarrow R_{i\shortrightarrow\tau}v\,y))))\,w\rightarrow\psi\,w)\end{array}$$

$$\begin{array}[]{ll}&\lambda x_{i}.((\forall w_{i}.(\phi w\wedge(\forall y_{i}.(\phi y\rightarrow Rwy))\rightarrow\psi w))\end{array}$$

$$\text{vld}\lfloor \varphi \rfloor =\forall z_i.\lfloor \varphi \rfloor z$$

$$\begin{array}[]{ll}&\forall z_{i}.(\phi z\wedge(\forall y_{i}.(\phi y\rightarrow Rzy))\rightarrow\psi z)\end{array}$$

$${\models }^{\mathcal{P}}\varphi \text{ if and only if }{\models }^{\text{HOL}}\text{vld}\lfloor \varphi \rfloor$$

Full text

††journal: Artificial Intelligencemyfootnotemyfootnotefootnotetext: Benzmüller was funded by the VolkswagenStiftung under grant CRAP (Consistent Rational Argumentation in Politics). Parent and van der Torre were supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement MIREL (MIning and REasoning with Legal texts) No 690974.

1 Introduction

The explicit representation-of and reasoning-with ethical and legal knowledge capacitates ethical intelligent systems with increasing levels of autonomy in their decision making [1, 2]. It also supports sufficient degrees of reliability and accountability, and it enables human intuitive interaction means regarding explainability and transparency of decisions. The ethical and/or legal theories—we often call them ethico-legal theories in the remainder—can thereby be represented as normative systems formalized on top of suitably selected underlying deontic logics [3, 4, 5] and logic combinations [6, 7]. In this article we introduce our Logic and Knowledge Engineering Framework and Methodology, termed LogiKEy, to apply off-the-shelf theorem proving and model finding technology to the design and engineering of specifically tailored normative systems and deontic logics for deployment in ethical intelligent reasoners.

An overall objective of LogiKEy is to enable and support the practical development of computational tools for normative reasoning based on formal methods. To this end we introduce the concept of experimentation in the formal study of ethical and legal reasoning: by representing examples, ethico-legal domain theories, deontic logics and logic combinations in a computational system we enable predictions and their assessment, and apply formal methods. Given this motivation to experiment-with, explore and assess different theories and logics in the design of ethical intelligent reasoners we address the following research questions:

1. A:

Which formal framework to choose, 2. B:

which methodology to apply, and 3. C:

which tool support to consult

for experimentation with ethico-legal theories?

Several examples of computational tools to experiment with ethical reasoners, normative systems and deontic logics have been introduced in the recent literature [8, 9, 10, 11, 12, 13] and are used in this article to illustrate the feasibility of the proposed solutions. LogiKEy extracts the general insights from these prior case studies and bundles them into a coherent approach.

1.1 Formal framework: expressive classical higher-order logic

We first explain why we use classical higher-order logic (HOL), i.e., Church’s type theory [14], as our formal framework. To understand the challenge of the choice of a formal framework (cf. our research question A), consider the requirements of a typical ethical agent architecture as visualized in Fig. 1.

The displayed architecture for an intelligent autonomous system [15] with explicit ethical competency distinguishes an explicit ethical reasoner and ethico-legal domain theories from an AI reasoner/planner and from other components, including also application data and knowledge available to both reasoners. The ethical reasoner takes as input suggested actions from the AI reasoner/planner, hints to relevant application data and knowledge, and the ethico-legal domain theories, and it produces as output assessments and judgements concerning which actions are acceptable or not, and it also provides corresponding explanations. That is, the actions suggested by the AI reasoners in Fig. 1 are not executed immediately, but additionally assessed by the ethical reasoner for compliance with respect to the given ethico-legal domain theories. This assessment is intended to provide an additional, explicit layer of explanation and control on top of the AI reasoner, which ideally already comes with solid own ethical competency. For the aims in this article, the details of the ethical agent architecture are not important. For example, it does not matter whether computations on the level of the AI reasoner are based on sub-symbolic or symbolic techniques, or combinations of them, since the suggested actions are not executed immediately—at least not those considered most critical. Instead they are internally assessed, before execution, against some explicitly modelled ethico-legal theories. These theories govern and control the behaviour of the entire system, and they also support—at this upper-level—system verification and intuitive user explanations. What counts, in particular, in highly critical contexts, is not only how an AI reasoner computed the critical action it wants to perform, but in particular whether this action passes the additional assessment by the upper-level explicit ethical reasoner before its execution.

The formal framework of the ethical reasoner has to be populated with ethico-legal domain theories, be able to combine logics, reason about the encoded domain theories, and experiment with concrete applications and examples, as visualized in Fig. 2.

This leads to an apparent paradox: on the one hand, the area of knowledge representation and reasoning in artificial intelligence is built on highly specialized and efficient formalisms;111In formalized mathematics, in contrast, practical developments are interestingly progressing already in the opposite direction; proof assistants such as Lean [16], Coq [17], or Agda [18], for example, are being developed and deployed, which, due to their rich type systems, are practically even more expressive than the HOL provers we utilize in LogiKEy: Isabelle/HOL [19] and Leo-III [20]. The latter provers, however, provide a very good degree of proof automation, and this, combined with a sufficient degree of expressivity for our purposes, is the reason we prefer them so far. on the other hand to combine all these aspects in a single formalism and to experiment with it, we need a highly expressive language. For example, as we explain in more detail in Sect. 3, the handling of normative concepts such as obligation, permission and prohibition is actually far more complex than one would initially think. This is illustrated, among others, by the notorious paradoxes of normative reasoning [21], and appropriate solutions to this challenge require sophisticated deontic logics. In LogiKEy we therefore model and implement ethical reasoners, normative systems and deontic logics in the expressive meta-logic HOL. This often triggers scepticism, in particular, in the AI knowledge representation and reasoning community, since HOL has known theoretical drawbacks, such as undecidability. However, HOL, just like first-order logic, has decidable fragments, and our shallow semantical embedding (SSE) approach, cf. Sect. 2, is capable of translating decidable proof problems, say in propositional modal logic, into corresponding decidable proof problems in (a fragment of) HOL. For example, the modal formula $\Box(\varphi\wedge\psi)$ is—assuming a request about its global validity—rewritten in the SSE approach into the guarded fragment formula $\forall w.\forall v.\neg(Rwv)\vee(\varphi v\wedge\psi v)$, where $R$ is denoting the accessibility relation associated with $\Box$. The (in-)validity of formulas in the guarded fragment is decidable, and our example formula can be effectively handled by Isabelle/HOLand Leo-III. The reason why these system can handle such decidable problems effectively is simple: they internally collaborate with state-of-the-art SAT & SMT (satisfiability modulo theories) solvers, and with first-order automated theorem proving systems; this ensures that fragments of HOL are indeed attacked with tools that are specialized for these fragments. Moreover, the framework we provide is universal, and this makes it an ideal approach for experimentation.

1.2 Methodology: LogiKEy

The LogiKEy methodology, a high-level development protocol that will be explained in detail in Sect. 7, constitutes our answer to research question B. This methodology supports and guides the simultaneous development of the three layers depicted in Fig. 2: combining logics, ethico-legal theories, and concrete examples and applications. The black arrows between these three levels symbolize dependencies. The normative governance applications developed at layer L3 depend on ethico-legal domain theories imported from layer L2, which in turn are formalized within a specific logic or logic combination provided at layer L1.222In this article we utilize a uniform coloring scheme in all our conceptual figures: layers L1 and L2 are displayed using dark red and light red coloring, respectively. Applications and experiments are displayed in blue, and the meta-logical HOL framework that is supporting the layers L1 and L2 is shown in green. The engineering process at the different layers has backtracking points and several work cycles may be required; thereby the higher layers may also pose modification requests to the lower layers. The white arrows symbolize such possible requests, and they may, unlike in most other approaches, also include far-reaching modifications of the logical foundations engineered at layer L1; such modifications at the logic layer are flexibly facilitated in our meta-logical approach.

As a concrete application, consider a smart home visualized in Fig. 3 [22].

This one uses an argumentation engine [23] in order to make ethical decisions based on normative systems of stakeholders. The argumentation-based mechanism is used to find an agreement in case of moral dilemmas, and to offer an explanation as to how a specific morally sensitive decision has been made. Liao et al. assume the existence of pre-defined systems of norms, coming from the outside and constraining the agent’s behavior. Like humans, intelligent systems evolve in a highly regulated environment. For instance, a smart home processes personal data 24/7, and, as will be discussed in Sect. 6.1, there are legal rules one must comply with when processing personal data; in the European Union such rules include the General Data Protection Regulation (GDPR, Regulation EU 2016/679). Given a description of the current situation, the smart home should thus be able, for example, to check compliance with these rules, and act accordingly in case of non-compliance.

1.3 Tool support: Isabelle/HOL and Leo-III

Our use of higher-order tool support, cf. our research question C, is visualized in Fig. 4. The LogiKEy methodology supports experimentation with different normative theories, in different application scenarios, and it is not tied to a specific deontic logic and also not restricted to decidable logics only. Since ethico-legal theories as well as suitable normative reasoning formalisms are both subject to exploration in LogiKEy, we introduce a flexible workbench to support empirical studies in which both can be varied, complemented, assessed and compared.

The enabling technology are higher-order theorem proving systems via the SSE technique [24]. We benefit from good improvements in the past decade in interactive theorem proving (ITP) and automated theorem proving (ATP) for HOL, and also from the overall coalescence of heterogeneous theorem proving systems, as witnessed, in particular, by Isabelle/HOL, LEO-II [25] and Leo-III, which fruitfully integrate other specialist ATP systems. In this way—as a sort of relevant byproduct of our research—we build a bridge between the classical and non-classical logics communities, the deduction systems community, and the formal ethics community;333The formal ethics community, among others, includes: Normative Multi-Agent Systems (http://icr.uni.lu/normas), Deontic Logic and Normative Systems (http://deonticlogic.org) and Formal Ethics (http://www.fe2019.ugent.be). With deduction systems community we refer to the areas of Automated Reasoning (http://aarinc.org) and Interactive Theorem Proving (https://itp2018.inria.fr); these are in turn composed of several subcommunities. cf. also Fig. 5, which will be explained in more detail in Sect. 2.1.

Theorem proving was a major impetus for the development of computer science, and ATP and ITP systems have been applied to a variety of domains, including mathematics and software & hardware verification. However, comparably little work has been invested so far to apply such systems to deontic logic and normative reasoning.

1.4 Contributions

The core contributions of this article are on various levels:

Motivated by our position in the trustworthy AI debate—where we defend the need for explicit ethico-legal governance of intelligent autonomous systems—we provide a survey of various technical results pertaining to the application of automated theorem proving to ethical reasoners, normative systems and deontic logics. 2. 2.

This survey is targeted to a general audience in AI. Instead of presenting selected formal definitions and proofs, we discuss motivations, commonalities and applications. Moreover, we provide an entry-level user-guide to our framework and methodology, called LogiKEy. Existing approaches [26, 27, 28, 29] are always tied to rather specific logical settings. We introduce a flexible workbench to support empirical studies with such theories in which the preferred logic formalisms themselves can be varied, complemented, assessed and compared. 3. 3.

Our ambition is to build a library of ethical reasoners, normative systems and deontic logics, and with this article we make a first step in that direction by providing a collection of Isabelle/HOL source files that can be reused by researchers and students interested in adopting LogiKEy in their own work.444Our data set is available at http://logikey.org; see also the associated article [30] in Data in brief.

We briefly clarify some terminology as used in the article. With experimentation we refer to the action or process of trying out new ideas, methods, or activities; this can be, for instance, the drafting of a new logic or combination of logics, or a new ethical theory, where one may want to see what would be the consequences of its adoption in a given application context. Methodology refers to the principles underlying the organization and the conduct of a design and knowledge engineering process; hereby design means the depiction of the main features of the system we want to achieve, and (knowledge or logic) engineering refers to all the technical and scientific aspects involved in building, maintaining and using a knowledge-based, resp. logic-based, system. Infrastructure is the framework that supports different components and functionalities of a system, and by logic implementation we here mean an engineering process that returns an executable computer program, a theorem prover, for a given logic; this can be done in very different ways, for example, by coding software from scratch or, as we prefer, by adopting the SSE approach, which utilizes HOL as a meta-level programming language within existing reasoners such as Isabelle/HOL or Leo-III.

The structure of this article is as follows. Section 2 further motivates the need for a flexible normative reasoning infrastructure and presents LogiKEy’s expressive reasoning framework. Section 3 briefly surveys and discusses the challenging area of normative reasoning; this section also explains which particular deontic logics have already been implemented. A concrete example implementation of a state-of-the-art deontic logic, Åqvist system E, is presented in further detail in Sect. 4. Tool support is discussed in Sect. 5, and subsequently two case studies are presented in Sect. 6. The first case study illustrates contrary-to-duty compliant reasoning in the context of the general data protection regulation. A second, larger case study shows how our framework scales for the formalization and automation of challenging ethical theories (Gewirth’s “Principle of Generic Consistency” [31]) on the computer. To enable the latter work an extended contrary-to-duty compliant higher-order deontic logic has been provided and utilized in our framework. Section 7 provides a detailed description of LogiKEy’s 3-layered logic and knowledge engineering methodology; it may thus provide useful guidance to future LogiKEy users. Sections 8 and 9 discuss related work and further research, and Sect. 10 concludes the article.

2 The LogiKEy expressive reasoning framework: meta-logic

HOL

This section presents and discusses LogiKEy’s expressive reasoning framework, cf. Fig. 5, which utilizes and adapts Benzmüller’s SSE approach [24].

The implementation of specialist theorem provers and model finders for, e.g., ambitious deontic logics and their extensions and combinations, is very tedious and requires expertise. LogiKEy therefore focuses on reuse and adaptation of existing technology rather than new implementations from first principles. A particular interest is to enable novices to become acquainted with the area of normative reasoning in short time and in a computer-assisted, hands-on fashion; this should enable them to gradually acquire much needed background expertise. An initial goal of our work therefore has been to build up a starting basis of mechanized deontic logics at layer L1 and ethico-legal domain theories at layer L2, and to make them accessible for experimentation to students and researchers. Our approach pays much attention to intuitive interaction within sophisticated user-interfaces to access, explore, assess and modify both the used foundational logic and logic combination and the encoded domain theories. The tools we reuse are state-of-the-art reasoning systems for classical logic that are actively developed by the deduction systems community. That relieves us from resource intensive investments in the implementation and maintenance of new technology. However, to enable this reuse of technology, a bridge between deontic logics (and their combinations with other modal logics) and classical logic was needed. This bridge is provided by the SSE approach.

The framework, methodology and technology we contribute requires some modest background knowledge to be acquired. The logic developers’ perspective, as relevant at LogiKEy layer L1, is a bit more ambitious and requires some familiarity with meta-logic HOL (cf. Sect. 2.2), and also a good mastery of the SSE technique (cf. Sect. 2.1). However, also at that level we support the adoption of initial skills by providing a library of example encodings of deontic logics, and other relevant logics and logic combinations, to start with; this is helpful, since it, among others, enables copying and pasting from these encodings. Several successful student projects at BSc, MSc and PhD level meanwhile provide good evidence for the practical relevance of our approach at the developers level [10, 11, 12, 13, 32, 33, 34, 35, 36, 37, 38].

2.1 Logic engineering and implementation methodology: SSEs in

HOL

Our expressive reasoning framework, depicted graphically in Fig. 5, is based on the SSE approach [39, 24]. HOL is utilized in this approach as a universal meta-logic in which different deontic logics are semantically embedded in a shallow way by directly encoding their semantics in meta-logic HOL; commonalities in the semantics of both logics are thereby typically shared as much as possible.555Shallow semantical embeddings are different from deep embeddings of a target logic. In the latter case the syntax of the target logic is represented using an inductive data structure (e.g., following the definition of the language). The semantics of a formula is then evaluated by recursively traversing the data structure, and additionally a proof theory for the logic maybe be encoded. Deep embeddings typically require technical inductive proofs, which hinder proof automation, that can be avoided when shallow semantical embeddings are used instead. For more information on shallow and deep embeddings we refer to the literature [40, 41].

We have extended this approach in our project for ambitious deontic logics, their extensions and combinations with other relevant logics. This enables the use of interactive proof assistants, such as Isabelle/HOL, which comes with a sophisticated user-interface and, in addition, integrates various state-of-the-art reasoning tools. The ATP systems integrated with Isabelle/HOL via the sledgehammer [42] tool comprise higher-order ATP systems, first-order ATP systems and satisfiability modulo theories (SMT) solvers, and many of these systems internally again employ efficient SAT solving technology. Isabelle/HOL also provides two model finders, Nitpick [43] and Nunchaku [44].

The SSE approach utilizes the syntactic capabilities of the higher-order theorem prover to represent the semantics of a target logic and to define the original syntax of the target theory within the prover. The overall infrastructure, in combination with the SSE approach, meets our demanding requirements regarding flexibility along different axes; cf. Sect. 5.

An initial focus in the SSE approach has been on quantified modal logics [39]. One core aspect is that the standard translation [45] from propositional modal logic to first-order logic can be semantically embedded, in HOL without requiring an external translation mechanism. The modal operator $\Diamond$, for example, can be explicitly defined by the $\lambda$-term $\lambda\varphi.\lambda w.\exists v.(Rwv\wedge\varphi v)$, where $R$ denotes the accessibility relation associated with $\Diamond$. This definition, however, can be hidden from the user, who can construct now modal logic formulas involving $\Diamond\varphi$ and use them to represent and prove theorems.

Most importantly, however, such an embedding of modal logic operators in HOL can be extended to also include quantifiers. We briefly illustrate this idea using an example (omitting types, as above, for better readability). First, it is relevant to note that $\forall x.\phi x$ is shorthand in HOL for $\Pi(\lambda x.\phi x)$, where the logical constant symbol $\Pi$ is given an obvious semantics, namely to check whether the set of objects denoted by $(\lambda x.\phi x)$ is the set of all objects (of the respective type). $\exists x.\phi x$ is hence shorthand for $\neg\Pi(\lambda x.\neg\phi x)$. The important and interesting aspect thus is that additional binding mechanisms for universal and existential quantifiers can be avoided in HOL by reusing $\lambda$-notation. This principle can now be applied also to obtain SSEs for quantified modal logics and, analogously, for many other quantified non-classical logics. For example, $\Diamond\forall x.Px$ is represented as $\Diamond\Pi^{\prime}(\lambda x.\lambda w.Pxw)$, where $\Pi^{\prime}$ stands for the $\lambda$-term $\lambda\Phi.\lambda w.\Pi(\lambda x.\Phi xw)$ and where the $\Diamond$ gets resolved as described above. The following series of conversions explains this encoding in more detail:

[TABLE]

This illustrates the embedding of $\Diamond\forall xPx$ in HOL.666In the implementation of our approach in Isabelle/HOL such conversions are hidden by default, so that the user may interact with the system at the level of the target logic and enter formulas such as $\Diamond\forall x.Px$. Definition unfolding is handled in the background, but can made visible upon request by the user. Moreover, this embedding can be accompanied with different notions of validity. For example, we say $\Diamond\forall x.Px$ is globally valid (valid for all worlds $w$) if and only if $\forall w.((\Diamond\forall x.Px)\ w)$ holds. Local validity for a particular actual world, denoted by a constant symbol $aw$, then amounts to checking whether $((\Diamond\forall x.Px)\ aw)$ is true in HOL.

What has been sketched above is an SSE for a first-order quantified modal logic K with a possibilist notion of quantification. However, depending on the type we assign to variable $x$ in $\Diamond\forall x.Px$, the sketched solution scales for arbitrary higher-order types. Since provers such as Isabelle/HOL and Leo-III support restricted forms of polymorphism, respective universal and existential quantifiers for the entire type hierarchy can be introduced with a single definition.777See, e.g., lines 14–17 in Fig. 6, where respective polymorphic quantifier definitions, including binder notation, are provided for Åqvist’s system E. Further details on the SSE of quantified modal logics in HOL, including a proof of faithfulness, are available in the literature [39]. Standard deontic logic (modal logic KD) can easily be obtained from this work. To do so we simply postulate in meta-logic HOL that the accessibility relation $R$ underlying the $\Diamond$ operator is serial. The corresponding D axiom $\Box\varphi\supset\neg\Box\neg\varphi$, or, equivalently, $\neg(\Box\varphi\wedge\Box\neg\varphi)$, then becomes derivable as a corollary from this postulate and the SSE (and so does the K-schema and the necessitation rule, already in base logic K). Further emendations of the presented framework to obtain multi-modal logics and an actualist notion of quantification have been proposed by Benzmüller et al.; cf. [24] and the references therein for further details.

2.2 Meta-logic HOL

HOL has its roots in the logic of Frege’s Begriffsschrift [46]. However, the version of HOL as addressed here refers to a simply typed logic of functions, which has been put foward by Church [14]. It provides $\lambda$-notation, as an elegant and useful means to denote unnamed functions, predicates and sets. Types in HOL eliminate paradoxes and inconsistencies.

To keep this article sufficiently self-contained we briefly introduce HOL; the reader may want to skip this subsection and get back again later. More detailed information on HOL and its automation can be found in the literature [14, 47, 48].

Definition 1** (Types).**

The set ${T}$ of simple types in HOL is freely generated from a set of basic types $BT\supseteq\{o,i\}$ using the function type constructor $\shortrightarrow$. Usually, type $o$ denotes the (bivalent) set of Booleans, and $i$ denotes a non-empty set of individuals. Further base types may be added.

Definition 2** (Terms and Formulas).**

The terms of HOL are defined as follows (where $C_{\alpha}$ denotes typed constants and $x_{\alpha}$ typed variables distinct from $C_{\alpha}$; $\alpha,\beta,o\in{T}$):

[TABLE]

Complex typed HOL terms are thus constructed via $\lambda$-abstraction and function application, and HOL terms of type $o$ are called formulas.

As primitive logical connectives we choose $\neg_{o\shortrightarrow o},\vee_{o\shortrightarrow o\shortrightarrow o}$ and $\Pi_{(\alpha\shortrightarrow o)\shortrightarrow o}$ (for each type $\alpha$), that is, we assume that these symbols are always contained in the signature. Binder notation $\forall x_{\alpha}.s_{o}$ is used as an abbreviation for $\Pi_{(\alpha\shortrightarrow o)\shortrightarrow o}\lambda x_{\alpha}.s_{o}$. Additionally, description or choice operators $\epsilon_{(\alpha\shortrightarrow o)\shortrightarrow\alpha}$ (for each type $\alpha$) or primitive equality $=_{\alpha\shortrightarrow\alpha\shortrightarrow o}$ (for each type $\alpha$), abbreviated as $=^{\alpha}$, may be added. From the selected set of primitive logical connectives, other logical connectives can be introduced as abbreviations. Equality can also be defined by exploiting Leibniz’ principle, expressing that two objects are equal if they share the same properties. Type information as well as brackets may be omitted if obvious from the context or irrelevant.

We consider two terms to be equal if the terms are the same up to the names of bound variables (i.e., $\alpha$-conversion is handled implicitly).

Substitution of a term $s_{\alpha}$ for a variable $x_{\alpha}$ in a term $t_{\beta}$ is denoted by $[s/x]t$. Since we consider $\alpha$-conversion implicitly, we assume the bound variables of $t$ are disjunct from the variables in $s$ (to avoid variable capture).

Prominent operations and relations on HOL terms include $\beta\eta$-normalization and $\beta\eta$-equality, $\beta$-reduction and $\eta$-reduction: a $\beta$-redex $(\lambda x.s)t$ $\beta$-reduces to $[t/x]s$; an $\eta$-redex $\lambda x.(sx)$ where variable $x$ is not free in $s$, $\eta$-reduces to $s$. It is well known, that for each simply typed $\lambda$-term there is a unique $\beta$-normal form and a unique $\beta\eta$-normal form. Two terms $l$ and $r$ are $\beta\eta$-equal, denoted as $l=_{\beta\eta}r$, if their $\beta\eta$-normal forms are identical (up to $\alpha$-conversion). Examples of $\lambda$-conversions have been presented on p. 2.1 (types were omitted there).

The semantics of HOL is well understood and thoroughly documented in the literature [47, 49]. The semantics of choice for our work is Henkin [50]’s general semantics. The following sketch of standard and Henkin semantics for HOL closely follows Benzmüller and Andrews [14].

A frame is a collection $\{D_{\alpha}\}_{\alpha\in{T}}$ of nonempty sets, called domains, such that $D_{o}=\{T,F\}$, where $T$ represents truth and $F$ falsehood, $D_{i}\not=\emptyset$ and $D_{u}\not=\emptyset$ are chosen arbitrary, and $D_{\alpha\shortrightarrow\beta}$ are collections of total functions mapping $D_{\alpha}$ into $D_{\beta}$.

Definition 3** (Interpretation).**

An interpretation is a tuple $\langle\{D_{\alpha}\}_{\alpha\in{T}},I\rangle$, where $\{D_{\alpha}\}_{\alpha\in{T}}$ is a frame, and where function $I$ maps each typed constant symbol $c_{\alpha}$ to an appropriate element of $D_{\alpha}$, which is called the denotation of $c_{\alpha}$. The denotations of $\neg,\vee$ and $\Pi_{(\alpha\shortrightarrow o)\shortrightarrow o}$ are always chosen as usual. A variable assignment $\phi$ maps variables $X_{\alpha}$ to elements in $D_{\alpha}$.

Definition 4** (Henkin model).**

An interpretation is a Henkin model (general model) if and only if there is a binary valuation function ${V}$, such that ${V}(\phi,s_{\alpha})\in D_{\alpha}$ for each variable assignment $\phi$ and term $s_{\alpha}$, and the following conditions are satisfied for all $\phi$, variables $x_{\alpha}$, constants $C_{\alpha}$, and terms $l_{\alpha\shortrightarrow\beta},r_{\alpha},s_{\beta}$ ($\alpha,\beta\in{T}$): ${V}(\phi,x_{\alpha})=\phi(x_{\alpha})$, ${V}(\phi,C_{\alpha})=I(C_{\alpha})$, ${V}(\phi,l_{\alpha\shortrightarrow\beta}\,r_{\alpha})=({V}(\phi,l_{\alpha\shortrightarrow\beta}){V}(\phi,r_{\alpha}))$, and ${V}(\phi,\lambda x_{\alpha}.s_{\beta})$ represents the function from $D_{\alpha}$ into $D_{\beta}$ whose value for each argument $z\in D_{\alpha}$ is ${V}(\phi[z/x_{\alpha}],s_{\beta})$, where $\phi[z/x_{\alpha}]$ is that assignment such that $\phi[z/x_{\alpha}](x_{\alpha})=z$ and $\phi[z/x_{\alpha}]y_{\beta}=\phi y_{\beta}$ when $y_{\beta}\not=x_{\alpha}$.

If an interpretation ${H}=\langle\{D_{\alpha}\}_{\alpha\in{T}},I\rangle$ is an Henkin model the function ${V}$ is uniquely determined and ${V}(\phi,s_{\alpha})\in D_{\alpha}$ is called the denotation of $s_{\alpha}$.

Definition 5** (Standard model).**

${H}=\langle\{D_{\alpha}\}_{\alpha\in{T}},I\rangle$* is called a standard model if and only if for all $\alpha$ and $\beta$, $D_{\alpha\shortrightarrow\beta}$ is the set of all functions from $D_{\alpha}$ into $D_{\beta}$. Obviously each standard model is also a Henkin model.*

Definition 6** (Validity).**

A formula $c$ of HOL is valid in a Henkin model ${H}$ if and only if ${V}(\phi,c)=T$ for all variable assignments $\phi$. In this case we write ${H}\models^{HOL}c$. $c$ is (Henkin) valid, denoted as $\models^{HOL}c$, if and only if ${H}\models^{HOL}c$ for all Henkin models ${H}$.

The following theorem verifies that the logical connectives behave as intended. The proof is straightforward.

Theorem 1**.**

Let ${V}$ be the valuation function of a Henkin model ${H}$. The following properties hold for all variable assignments $\phi$, terms $s_{o},t_{o},l_{\alpha},r_{\alpha}$, and variables $x_{\alpha},w_{\alpha}$: ${V}(\phi,\neg s_{o})=T$ if and only if ${V}(\phi,s_{o})=F$, ${V}(\phi,s_{o}\vee t_{o})=T$ if and only if ${V}(\phi,s_{o})=T$ or ${V}(\phi,t_{o})=T$, ${V}(\phi,\forall x_{\alpha}.s_{o})={V}(\phi,\Pi_{(\alpha\shortrightarrow o)\shortrightarrow o}\lambda x_{\alpha}.s_{o})=T$ if and only if for all $v\in D_{\alpha}$ holds ${V}(\phi[v/w_{\alpha}],(\lambda x_{\alpha}s_{o})\,w_{\alpha})=T$, and if $l_{\alpha}=_{\beta\eta}r_{\alpha}$ then ${V}(\phi,l_{\alpha})={V}(\phi,r_{\alpha})$.

A HOL formula $c$ that is Henkin-valid is obviously also valid in all standard models. Thus, when a Henkin-sound theorem prover for HOL finds a proof for $c$, then we know that $c$ is also theorem in standard semantics. More care has to be taken when model finders for HOL return models or countermodels, since theoretically these models could be non-standard. In practice this has not been an issue, since the available model finders for HOL so far return finite models only, and finite models in HOL are known to be standard [14]. Most importantly, however, the returned models in Isabelle/HOL can always be inspected by the user.

3 Theories of normative reasoning covered by the LogiKEy approach

Before explaining what theories of normative reasoning are covered by the SSE approach, we briefly survey the area of deontic logic. The logics described below are all candidates for LogiKEy layer L1.

3.1 Deontic logic

Deontic logic [51, 3, 5] is the field of logic that is concerned with normative concepts such as obligation, permission, and prohibition. Alternatively, a deontic logic is a formal system capturing the essential logical features of these concepts. Typically, a deontic logic uses $Op$ to mean that “it is obligatory that $p$”, or “it ought to be the case that $p$”, and $Pp$ to mean that “it is permitted, or permissible, that $p$”. Deontic logic can be used for reasoning about normative multiagent systems, i.e., about multiagent organizations with normative systems in which agents can decide whether to follow the explicitly represented norms, and the normative systems specify how, and to which extent, agents can modify the norms. Normative multiagent systems need to combine normative reasoning with agent interaction, and thus raise the challenge to relate the logic of normative systems to aspects of agency.

There are two main paradigms in deontic logic: the modal logic paradigm; the norm-based paradigm. This classification is not meant to be exhaustive or exclusive. Some frameworks, like adaptive deontic logic [52, 53], combine the two. We briefly describe the two paradigms in the next two subsections.

3.1.1 Modal logic paradigm

Traditional (or “standard”) deontic logic (SDL) is a normal propositional modal logic of type KD, which means that it extends the propositional tautologies with the axioms $K$: $O(p\rightarrow q)\rightarrow(Op\rightarrow Oq)$ and $D$: $\neg(Op\wedge O\neg p)$, and it is closed under the inference rules modus ponens $p,p\rightarrow q/q$ and generalization or necessitation $p/Op$. Prohibition and permission are defined by $Fp=O\neg p$ and $Pp=\neg O\neg p$. SDL is an unusually simple and elegant theory. An advantage of its modal-logical setting is that it can easily be extended with other modalities such as epistemic or temporal operators and modal accounts of action.

Dyadic deontic logic (DDL) introduces a conditional operator $O(p/q)$, to be read as “it ought to be the case that $p$, given $q$”. A number of DDLs have been proposed to deal with so-called contrary-to-duty (CTD) reasoning, cf. Carmo and Jones [21] for an overview on this area. In brief, the CTD problem is mostly about how to represent conditional obligation sentences dealing with norm violation, and an example is provided Sect. 6.1. Two landmark DDLs are the DDL proposed by Hansson [54], Åqvist [55, 56] and Kratzer [57], and the one proposed by Carmo and Jones [21, 58]. A notable feature of the DDL by Åqvist is that it also provides support for reasoning about so-called prima facie obligations [59]. A prima facie obligation is one that leaves room for exceptions. A limitation of the DDL by Carmo and Jones has been pointed out by Kjos-Hanssen [60].

To enable ethical agency a model of decision-making needs to be integrated in the deontic frames. Horty’s deontic STIT logic [61], which combines deontic logic with a modal logic of action, has been proposed as a starting point. The semantic condition for the STIT-ought is a utilitarian generalization of the SDL view that “it ought be that $A$” means that $A$ holds in all deontically optimal worlds.

3.1.2 Norm-based paradigm

The term “norm-based” deontic logic has been coined by Hansen [62] to refer to a family of frameworks analysing the deontic modalities not with reference to a set of possible worlds, some of them being more ideal than others, but with reference to a set of explicitly given norms. In such a framework, the central question is: given some input (e.g., a fact) and a set of explicitly given conditional norms (a normative system), what norms apply? Thus, the perspective is slightly different from the traditional setting, focusing on inference patterns [63].

Examples of norm-based deontic logics include the input/output (I/O) logic of Makinson & van der Torre [64], Horty’s theory of reasons [65], which is based on Reiter’s default logic, and Hansen’s logic of prioritized conditional obligations [66, 62].

By way of illustration, we document further I/O logic. The knowledge base takes the form of a set of rules of the form ($a$,$b$) to be read as “if $a$ then $b$”. The key feature of I/O logic is that it uses an operational semantics, based on the notion of detachment, rather than a truth-functional one in terms of truth-values and possible worlds. On the semantical side, the meaning of the deontic concepts is given in terms of a set of procedures, called I/O operations, yielding outputs (e.g., obligations) for inputs (facts). On the syntactical side, the proof-theory is formulated as a set of inference rules manipulating pairs of formulas rather than individual formulas. The framework supports functionalities that are often regarded as characteristic of the legal domain, and thus required to enable effective legal reasoning. Below, we list the two most elementary requirements that can be expected of a framework, if it is to deal with the legal domain; they are taken from Palmirani & colleagues [67].

Support for the modeling of constitutive rules, which define concepts or constitute activities that cannot exist without such rules (e.g., legal definitions such as “property”), and prescriptive rules, which regulate actions by making them obligatory, permitted, or prohibited. 2. 2.

Implementation of defeasibility [68, 69]; when the antecedent of a rule is satisfied by the facts of a case (or via other rules), the conclusion of the rule presumably holds, but is not necessarily true.

Other norm-based frameworks provide support for the aforementioned two functionalities. An example of such a framework is formal argumentation [70]. The question of how to embed argumentation frameworks into HOL is ongoing and future work [35].

3.2 Theories of normative reasoning implemented

The following theories of normative reasoning have been “implemented” by utilising the SSE approach.

SDL: All logics from the modal logic cube, including logic KD, i.e. SDL, have meanwhile been faithfully implemented in the SSE approach [39]. These implementations scale for first-order and even higher-order extensions.

DDL: the DDL by Åqvist [55, 56] and the DDL by Carmo and Jones [58]: Faithful SSEs of these logics in Isabelle/HOL are already available [8, 9], and most recently the ATP system Leo-III has been adapted to accept DDL as input [71, 72].

I/O logic [64]: The main challenge comes from the fact that the framework does not have a truth-functional semantics, but an operational one. First experiments with the SSE of the I/O-operator out1 (called simple-minded) and out2 (called basic) in Isabelle/HOL have been presented in the literature [10, 73].

I/O logic variants have recently been studied [74, 75] and some of these variants are related to certain non-normal modal logics, e.g., conditional logics with a selection function or a neighbourhood semantics. Note that the embedding of logics of the latter kind has already been studied in previous work [76, 77].

4 Sample LogiKEy embedding: Åqvist’s system E in HOL

In this section, to illustrate our approach, we describe our embedding of Åqvist [55]’s dyadic deontic logic in HOL. The system is called E.

We give this example, because all the development steps foreseen at layer L1 of LogiKEy (cf. Sect. 7) have been caried out for this system. In particular, the embedding has been shown to be faithfull—this is one of our key success criteria at layer L1. Moreover, this logic has been tested against available benchmarks, like those related to CTD reasoning. For sure, one does not need automated theorem provers to see that the system can handle this type of reasoning while SDL cannot. The treatment of CTD reasoning motived DDL in the first place. However, from pen and paper results alone one cannot conclude that an implementation of a logic will result in a practically useful system. Such an orthogonal question must be answered by empirical means, in particular, when first-order or higher-order extensions, or combinations with other logics, are required. Our SSE-based implementation of system E scales for such extensions; a first-order extension will later be tested with a simple CTD example structure in Sect. 6.1.

4.1 Target logic: system E

Definition 7**.**

The language of E is generated by the following BNF:

[TABLE]

$\square\phi$ is read as “$\phi$ is settled as true”, and $\bigcirc(\psi/\phi)$ as “$\psi$ is obligatory, given $\phi$”. $\bigcirc\phi$ (“$\phi$ is unconditionally obligatory”) is short for $\bigcirc(\phi/\top)$.

Traditionally so-called preference models are used as models for the language.

Definition 8**.**

A preference model $M=(W,\succeq,V)$ is a tuple where:

• •

$W$* is a (non-empty) set of possible worlds;*

• •

$\succeq$* is a binary relation over $W$ ordering the worlds according to their betterness or comparative goodness; $s\succeq t$ is read as “$s$ is at least as good as $t$”; $\succeq$ is called a preference or betterness relation;888“Preference relation” is a generic name used in different areas like the areas of conditional logic, rational choice theory, non-monotonic logic, and deontic logic. “Betterness relation” is the name used in deontic logic. This choice of name is dictated by the intuitive interpretation given to the preference relation.*

• •

$V$* is a valuation assigning to each propositional letter $p$ a set of worlds, namely the set of those worlds at which $p$ holds.*

For E, no specific properties are assumed of the preference or betterness relation $\succeq$. It is known that the assumptions of reflexivity and totalness (every worlds are pairwise comparable) do not “affect” the logic; cf. Theorem 2.

Intuitively the evaluation rule for $\bigcirc(\psi/\phi)$ puts $\bigcirc(\psi/\phi)$ true if and only if the best $\phi$-worlds, according to $\succeq$, are all $\psi$-worlds. Formally:

Definition 9** (Satisfaction).**

Given a preference model $M=(W,\succeq,V)$ and a world $s\in W$, we define the satisfaction relation $M,s\vDash\phi$ as usual, except for the following two new clauses:

• •

$M,s\vDash\Box\phi$* iff for all $t$ in $M$, $M,t\vDash\phi$*

• •

$M,s\vDash\bigcirc(\psi/\phi)$* iff $\mathrm{opt}_{\succeq}(||\phi||)\subseteq||\psi||$*

where $\|\phi\|$ is the set of worlds at which $\phi$ holds and $\mathrm{opt}_{\succeq}(||\phi||)$ is the subset of those that are optimal according to $\succeq$:

[TABLE]

Definition 10** (Validity).**

A formula $\phi$ is valid in the class $\mathcal{P}$ of all preference models (notation: $\models^{\mathcal{P}}\phi$) if and only if, for all preference models $M$ and all worlds $s$ in $M$, $M,s\models\phi$.

Definition 11**.**

E* is the proof system consisting of the following axiom schemata and rule schemata (the names are taken from Parent [78]):*

[TABLE]

The notions of theorem and consistency are defined as usual.

In the work of Åqvist, cf. [79, pp. 179–181] and [55, pp. 247–249] the question of whether E is complete with respect to its intended modeling has been left as an open problem; it has been recently been answered by Parent [56]. See Goble [80] for a similar axiomatization result of Hansson’s original models.

The second and third clauses in the statement of Theorem 2 mean that the assumptions of reflexivity and totalness do not have any impact on the logic. The fact that these two properties are idle remains largely unnoticed in the literature.

Theorem 2**.**

E* is sound and complete with respect to the following three classes of preference models:*

the class of all preference models; 2. 2.

the class of preference models in which the betterness relation is required to be reflexive; 3. 3.

the class of preference models in which the betterness relation is required to be total (for all $s$ and $t$, either $s\succeq t$ or $t\succeq s$).

Proof.

The proof can be found in Parent [56]. ∎

Theorem 3**.**

The theoremhood problem in E (“Is $\phi$ a theorem in E?”) is decidable.

Proof.

The proof can be found in Parent [81]. ∎

Stronger systems may be obtained by adding further constraints on $\succeq$, like transitivity and the so-called limit assumption, which rules out infinite sequences of strictly better worlds.

4.2 Embedding of E in HOL

The formulas of E are identified in our SSE with certain HOL terms (predicates) of type $i\shortrightarrow o$, where terms of type $i$ are assumed to denote possible worlds and $o$ denotes the (bivalent) set of Booleans. Type $i\shortrightarrow o$ is abbreviated as $\tau$ in the remainder. The HOL signature is assumed to contain the constant symbol $R_{i\shortrightarrow\tau}$. Moreover, for each propositional symbol $p^{j}$ of E, the HOL signature must contain the corresponding constant symbol $P^{j}_{\tau}$. Without loss of generality, we assume that besides those symbols and the primitive logical connectives of HOL, no other constant symbols are given in the signature of HOL.

Definition 12**.**

The mapping $\lfloor\cdot\rfloor$ translates a formula $\varphi$ of E into a formula $\lfloor\varphi\rfloor$ of HOL of type $\tau$. The mapping is defined recursively in the usual way [24], except for the following two new clauses:

[TABLE]

where $\Box_{\tau\shortrightarrow\tau}$ and $\bigcirc_{\tau\shortrightarrow\tau\shortrightarrow\tau}$ abbreviate the following formulas of HOL:

[TABLE]

The basic idea is to make the modal logic’s possible worlds structure explicit by introducing a distinguished predicate symbol $R$ to represent the preference or betterness relation $\succeq$, and to translate a formula directly according to its semantics. For instance $\bigcirc(\psi/\phi)$ translates into

[TABLE]

Definition 13** (Validity of an embedded formula).**

Global validity ($vld$) of an embedded formula $\phi$ of E in HOL is defined by the equation

[TABLE]

For example, checking the global validity of $\bigcirc(\psi/\phi)$ in E is hence reduced to checking the validity of the formula

[TABLE]

in HOL.

This definition is hidden from the user, who can construct now deontic logic formulas involving $\bigcirc(\psi/\phi)$ and use them to represent and prove theorems.

4.3 Faithfulness of the embedding

It can be shown that the embedding is faithful, in the sense given by Thm. 4. Remember that the establishment of such a result is our main success criterium at layer L1 in the LogiKEy methodology. Intuitively, Thm. 4 says that a formula $\phi$ in the language of ${\bf E}$ is valid in the class of all preference models if and only if its translation $\lfloor\phi\rfloor$ in the language of HOL is valid in the class of Henkin models in the sense of Def. 13.

Theorem 4** (Faithfulness of the embedding).**

[TABLE]

Proof.

The proof can be found in Benzmüller et al. [8]. The crux of the argument consists in relating preference models with Henkin models in a truth-preserving way. ∎

4.4 Encoding in Isabelle/HOL

The practical employment of the above SSE for E in Isabelle/HOL is straightforward and can be done in a separate theory file. This way, for a concrete application scenario, we can simply import the embedding without dealing with any technical details. The complete embedding is quite short (approx. 30 lines of code with line breaks) and is displayed in Fig. 6.

The embedding has been extended to include quantifiers as well. The possibilist quantifiers (cf. Sect. 2.1) are introduced in lines 13–17—this amounts to having a fixed domain of individuals rather than a world-relative domain (the actualist semantics). If needs be, actualist quantifiers can also be introduced in a few lines of code; see the study [24], where analogous definitions of both possibilist and actualist quantifiers are presented for higher-order conditional logic. The betterness relation $R$ is introduced as an uninterpreted constant symbol in line 20, and the conditional obligation operator is defined in line 26. Its definition mirrors the one given in Def. 12. The unconditional obligation operator is introduced in line 27. It is defined in terms of its dyadic counterpart in the usual way. Last, global and local validity (cf. Sect. 2.1) are introduced in lines 30–33. Lines 35–40 show sample queries. On line 35, consistency of the embedding is confirmed. Lines 37–40 illustrate how Isabelle/HOL can be used as a heuristic tool in correspondence theory. The focus is on the assumption of transitivity of the betterness relation. One would like to know what its syntactical counterpart is. Isabelle/HOL confirms that such an assumption has the effect of validating the axiom Lewis [82] called CV (line 39). Isabelle/HOL also confirms that transitivity is not equivalent to CV: the model finder Nitpick [43] integrated with Isabelle/HOL finds a model validating CV in which the betterness relation is not transitive (lines 42–44).

5 LogiKEy tool support

5.1 Support for different reasoning tasks

In a nutshell, a reasoner is a tool that can perform reasoning tasks in a given application domain. Reasoning thereby refers to the process of deriving or concluding information that is not explicitly encoded in the knowledge base. Which information is derivable and which is not is thereby dependent on the particular choice of logic. The reasoning tasks that are particularly relevant in our context, for example, include:

• •

Compliance checking: Is the current situation, respectively, an intended action by an IAS in a given context, compliant with a given regulation (a set of formally represented norms)?

• •

Non-compliance analysis: If non-compliance is the result of a compliance check, can the reasons be revealed and explained?

• •

Entailment checking: Does such-and-such obligation or legal interpretation follow from a given regulation?

• •

Non-entailment analysis: If entailment checking fails, can the reasons be revealed and explained?

• •

Consistency checking: Is a given regulation consistent? Is such-and-such norm, as part of a given regulation, consistent with this other set of norms, stemming from another regulation? Is such-and-such legal interpretation consistent with another one?

• •

Inconsistency analysis: If consistency checking fails, can a minimal set of conflicting norms be revealed and the inconsistency be explained?

We take consistency in its usual sense in classical logic. A set of formulas is consistent, if there exists a model that satisfies all of its members, and inconsistent otherwise. Thus, $\{p,q\}$ is consistent, but $\{p,\neg p\}$ is not. Likewise, $\{\bigcirc p,\bigcirc\neg p\}$ is consistent in a system of deontic logic accommodating the existence of conflicts, but $\{\bigcirc p,\neg{\bigcirc p}\}$ is not.

Consistency checking, non-compliance analysis and non-entailment analysis are well supported by model finders, respectively counter-model finders, while the other tasks generally require theorem proving technology. A powerful deontic reasoner should thus ideally provide both (counter-)model finding and theorem proving. Moreover, intuitive proof objects and adequate presentations of (counter-)models are desirable to enable user explanations.

5.2 Flexibility along different axes

While the above reasoning tasks are comparably easy to provide for many decidable propositional fragments of deontic logics, it becomes much less so for their quantified extensions. We are not aware of any system, besides the work presented in this article, that still meets all these requirements; cf. the related work in Sect. 8.

Our approach addresses challenges along different axes, which are motivated by the following observations:

Different logics: The quest for “a most suitable deontic logic” is still open, and will eventually remain so for quite some time. Therefore, a user should be able to choose the logic that suits his or her needs best. Our platform is flexible, and can “host” a wide range of deontic logics (cf. Sect. 3.2).

Expressivity levels: It is highly questionable whether normative knowledge and regulatory texts can often be abstracted and simplified to the point that pure propositional logic encodings are feasible and justified. For example, it can be doubted that the encoding of Gewirth’s “Principle of Generic Consistency”, which we outline in Sect. 6.2, can be mechanized also in a propositional setting without trivialising it to a point of vacuity. The need for quantified deontic logics is also evidenced by related work such as Govindarajulu and Bringsjord’s encoding of the “Doctrine of Double Effect” [83].

Logic combinations: In concrete applications normative aspects often meet with other challenges that can be addressed by suitable logic extensions, respectively, by combining a deontic logic with other suitable logics as required. An example is provided again by the encoding of Gewirth’s ethical theory as outlined in Sect. 6.2.

These issues should be addressed, utilising the LogiKEy methodology, in empirical studies in which the different choices of logics, different expressivity levels and different logic combinations are systematically compared and assessed within well selected application studies. However, for such empirical work to be feasible, implementations of the different deontic candidate logics, and its combinations with other logics, have to be provided first, both on the propositional level and ideally also on the first-order and higher-order level. Moreover, it is reasonable to ensure that these implementations remain comparable regarding the technological foundations they are based on, since this may improve the fairness and the significance of conceptual empirical evaluations.

Figure 4 well illustrates the different components and aspects that we consider relevant in our work. Different target logics (grey circles) and their combinations are provided in the higher-order meta-logic of the host system. In our case this one is either the proof assistant Isabelle/HOL or the higher-order ATP system Leo-III. In provided target logics different ethico-legal theories can then be encoded. Concrete examples are given in Sect. 6. This set-up enables a two-way fertilization. On the one hand, the studied theories are themselves assessed, e.g., for consistency, for entailed knowledge, etc. On the other hand the properties of the different target logics are investigated. For example, while one of the target logics might suffer from paradoxes in a concrete application context, another target logic might well be sufficiently stable against paradoxes in the same application context. An illustration of this aspect is given in Sect. 6.1. After arriving at consistent formalizations of an ethico-legal theory in a suitable logic or suitable combination of logics, empirical studies can be conducted.999 To this end the agent-based LeoPARD framework [84, 85], which is underlying the prover Leo-III [20], can be adapted and utilized, e.g., to embody upper ethical theories in virtual agents and to conduct empirical studies about the agents behaviour when reasoning with such upper principles in a simulated environment. The prover Leo-III is itself implemented as a proactive agent in the LeoPARD framework, which internally utilizes another copy/instance of the LeoPARD framework for the organization and orchestration of its distributed reasoning approach, where it collaborates, e.g., with other theorem provers that are modelled as proactive agents. In other words, Leo-III already is a pro-active agent within an agent-based framework, and it already comes with deontic logic reasoning support. The idea is now to populate multiple instances of such pro-active agents with selected normative theories within the LeoPARD framework, to initialize these agent societies with carefully selected tasks, and to subsequently study their interaction behaviour within a controlled environment.

6 LogiKEy case studies

In this section we shift our attention to the encoding of ethico-legal theories at LogiKEy layer L2. We outline and selectively discuss two respective case studies.

6.1 Data protection

In our first case study the legal theory of interest is the General Data Protection Regulation (GDPR, Regulation EU 2016/679). It is a regulation by which the European Parliament, the Council of the European Union and the European Commission intend to strengthen and unify data protection for all individuals within the European Union. The regulation became enforceable from 25 May 2018.

First-order logic has been identified so far as a good level of abstraction (in the case study in 6.2, in contrast, higher-order logic is used). Given respective first-order extensions of deontic logics, the interest then is to practically assess their correctness and reasoning performance in context, and to compare the outcomes of such tests with our expectations. Below we illustrate how such practical assessments can be conducted within the interactive user-interface of Isabelle/HOL. As an illustrating example we present a concrete CTD structure that we revealed in the context of the GDPR; for readers not yet familiar with CTD structures this example may also be useful from an educational viewpoint.

The proper representation of CTD structures is a well-known problem in the study of deontic logics. CTD structures refer to situations in which there is a primary obligation and, additionally, what we might call a secondary, contrary-to-duty obligation, which comes into effect when the primary obligation is violated.101010The problem was first pointed out by Chisholm [86] in relation with SDL. The paradox arises when we try to symbolize certain intuitively consistent sets of ordinary language sentences, sets that include at least one CTD obligation sentence, by means of ordinary counterparts available in various monadic deontic logics, such as SDL and similar systems. The formal representations often turn out to be inconsistent, in the sense that it is possible to deduce contradictions from them, or else they might violate some other intuitively plausible condition, for example that the sentences in the formalization should be independent of each other. It is not the purpose of this article to discuss in any greater depth the paradox. The interested reader should consult, e.g., Carmo and Jones [21].

Here is the CTD structure we revealed in the context of the GDPR:

Personal data shall be processed lawfully (Art. 5). For example, the data subject must have given consent to the processing of his or her personal data for one or more specific purposes (Art. 6/1.a).

If the personal data have been processed unlawfully (none of the requirements for a lawful processing applies), the controller has the obligation to erase the personal data in question without delay (Art. 17.d, right to be forgotten).

When combined with the following a typical CTD-structure is exhibited.

It is obligatory, e.g., as part of a respective agreement between a customer and a company, to keep the personal data (as relevant to the agreement) provided that it is processed lawfully.

Some data in the context of such an agreement has been processed unlawfully.

The latter information pieces are not part of the GDPR. (3) is a norm coming from another regulation, with which the GDPR has to co-exists. (4) is a factual information—it is exactly the kind of world situations the GDPR wants to regulate.

Figure 7 illustrates the problem raised by CTD scenarios, when the inference engine is based on SDL. The knowledge base is encoded in lines 7–25. The relevant obligations and the assumed situation as described by (1)–(4) above are formalized in lines 18–25. Subsequently, three different kinds of queries are answered by the reasoning tools integrated with Isabelle/HOL. The first query asks whether the encoded knowledge base is consistent, and Nitpick answers negatively to this question in line 28. The failed attempt to compute a model is highlighted in pink. The second query asks whether falsum is derivable, and Isabelle/HOL’s prover metis returns a proof within a few milliseconds in line 29. Notice that the proof depends on the seriality axiom D of SDL, which is imported from SDL’s encoding in file SDL.thy–that is not shown here. The query in line 36 asks whether an arbitrarily weird and unethical conclusion such as the obligation to kill Mary follows, and the prover answers positively to this query.

These results are clearly not desirable, and confirm the need to use a logic other than SDL for application scenarios in which norm violation play a key role.

Fig. 8 shows that our SSE based implementation of system E is in contrast not suffering from this effect. The prescriptive rules of the GDPR scenario are modelled in lines 17–22:

⬇

A1: $\forall$d $\bigcirc(\mathsf{process}\_\mathsf{lawfully}\;\mathsf{d}/\mathsf{is}\_\mathsf{protected}\_\mathsf{by}\_\mathsf{GDPR}\;\mathsf{d})$

A2: $\forall$d $\bigcirc(\mathsf{erase}\;\mathsf{d}/\mathsf{is}\_\mathsf{protected}\_\mathsf{by}\_\mathsf{GDPR}\;\mathsf{d}\wedge\neg\mathsf{process}\_\mathsf{lawfully}\;\mathsf{d})$

A3: $\forall$d $\bigcirc(\neg\mathsf{erase}\;\mathsf{d}/\mathsf{is}\_\mathsf{protected}\_\mathsf{by}\_\mathsf{GDPR}\;\mathsf{d}\wedge\mathsf{process}\_\mathsf{lawfully}\;\mathsf{d})$

The current situation, in which we have that Peter’s personal data $\mathsf{d1}$ are not processed lawfully, is defined in line 24:

⬇

Situation:  $\neg\mathsf{process}\_\mathsf{lawfully}\;\mathsf{d1}$

The three same queries as before are run, but this time with success. In line 28 we are told by Nitpick that the knowledge base has a model. The computed model can be inspected in full detail a separate window. In line 29 we are told that falsum is no longer derivable and the theorem provers integrated with sledghammer terminate with a time-out. In line 30 we are told that the obligation to kill Mary no longer follows.

These practical experiments with theorem provers and model finders demonstrate that a machine can indeed reason about norm violation in a first-order extension of DDL at run-time, resp. on the fly. Future research will study the practical deployment of the LogiKEy flexible reasoning technology, for example, for ethico-legal governance of autonomous cars, smart homes, social robots, etc. Given these ambitious goals, it is relevant to confirm early-on that the LogiKEy solution, without further ado, can already handle simple examples as discussed here.111111For example, Meder, in his MSc thesis [11], worked out an SSE for a variant of STIT-logic put forth by Lorini [87], called T-STIT, for temporal STIT. It was found out that model and (counter-)model finding wasn’t responsive for analogous experiments. The reason, however, was quickly revealed: the T-STIT-logic, by nature, requires infinite models, while the (counter-)model finding tools in Isabelle/HOL so far explore finite model structures only. This, of course, provides only a relevant first assessment step. The development of respective libraries of increasingly complex benchmarks, see also Sect. 6.2, is therefore an important objective in our future work.

6.2 Gewirth’s Principle of Generic

Consistency

In a second case study our framework has been adapted and utilized for the exemplary mechanization and assessment [12, 13] of Alan Gewirth’s Principle of Generic Consistency (PGC) [31, 88] on the computer; the PGC is an ethical theory that can be understood as an emendation of the well known golden rule. The formalization of the PGC, which is summarized below, demonstrates that intuitive encodings of ambitious ethical theories and their mechanization, resp. automation, on the computer are no longer antipodes.

Some further information on the PGC is given in Fig. 9, including a depiction of the modeling decisions taken for its formalization. The self-contained Isabelle/HOL sources of the formalization are available in the Archive of Formal Proofs [34],121212See also the Data in brief article [30] associated with this article. and an excerpt of the derivation and verification of the main inference steps of the argument is presented in Fig. 10.

The argument used by Gewirth to derive the PGC is by no means trivial and has stirred much controversy in legal and moral philosophy during the last decades. It has also been discussed in political philosophy as an argument for the a priori necessity of human rights. Perhaps more relevant for us, the PGC has lately been proposed as a means to bound the impact of artificial general intelligence [90].

Gewirth’s PGC is taken here as an illustrative showcase to exemplarily assess its logical validity with our normative reasoning machinery, and the success of Fuenmayor’s and Benzmüller’s work [12, 13] provides evidence for the claims made in this article. It is the first time that the PGC has been formalized and assessed on the computer at such a level of detail, i.e., without trivializing it by abstraction means, and while upholding intuitive formula representations and user-interaction means. As a side-effect, the ATP systems integrated with Isabelle/HOL have helped in this work to reveal and fix some (minor) issues in Gewirth’s argument.

To encode the PGC an extended embedding of the DDL by Carmo and Jones in HOL was employed. Conditional, ideal and actual obligation has been combined, among others, with further modalities, with Kaplan’s notion of context-dependent logical validity, and with both first-order and higher-order quantifiers.131313Kaplan’s context-sensitive logic of demonstratives covers the dimension of agency, among others. Future work includes the study of alternative modelings, utilising, e.g., the modal logics of agency or STIT logic. STIT logic, however, gives rise to interesting problems, including infinite models as already noted. The infinite character is fixed in the axioms.

What can be seen in Fig. 10 is that readable formula presentations are supported, which in turn enable quite intuitive user-interactions in combination with proof automation means. It is demonstrated that the interactive assessment of Gewirth’s argument is supported at an adequate level of granularity: the proof steps as presented in Fig. 10 correspond directly to actual steps in Gewirth’s argument and further details in the verification process can be delegated to automated reasoning tools provided in Isabelle/HOL.

Proof automation can be pushed further, but this has not been the focus so far in this work. The result of this work is a formally verified derivation of the statement “Every prospective purposive agent has a claim right to their free will and well-being” from Gewirth’s elementary premises, axioms and definitions in the theorem prover Isabelle/HOL (at LogiKEy layer L2, cf. Fig. 2). The formalization of this ethical theory in combination with the mechanization and automation of its underlying non-trivial, logic combination (at LogiKEy layer L1) enables further experiments with the theory and provides an entry for devising applications of it (at LogiKEy layer L3). One possibility in this regard is the population of this theory within virtual agents, so that the behaviour of each agent is ultimately constraint, if no other regulatory rules apply, by this very general moral principle; cf. Footnote 9.

7 Logic & knowledge design and engineering methodology

Now that we have explained and illustrated various ingredients and aspects of LogiKEy, we will, in this section, present and discuss the LogiKEy logic & knowledge design and engineering methodology methodology in more detail. Remember that LogiKEy distinguishes between the following three layers; they were visualized earlier in Fig. 2.

1. L1

Logics and logic combinations. Logics and logic combinations are modelled, automated and assessed at layer L1. The automation of CTD compliant normative reasoning is thereby of particular interest, where logical explosion is avoided even in situations when an intelligent autonomous system (IAS) accidentally or deliberately violates some of its obligations. We thus prefer a proper intra-logical handling of the CTD challenge in our work over tackling this challenge, e.g., with extra-logical and ad hoc means. Sect. 3 presented respective examples of CTD compliant logics—the dyadic deontic logic (DDL) of Carmo and Jones [21] and Åqvist’s system E [55, 56]—and Sect. 4 explained how system E is modelled and automated adopting the LogiKEy methodology. 2. L2

Ethico-legal domain theories. At layer L2 concrete ethico-legal theories are modelled, automated and assessed — exploiting the logic and logic combinations from layer L1. Question answering, consistency and compliance checking support is provided. Our particular interest is in ethico-legal theories suited to govern the behaviour of IASs. Examples for layer L2 developments were presented in Sect. 6, and tool support, for L2 and the other layers, was discussed in Sect. 5. 3. L3

Applications. Layer L3 addresses the deployment of the ethical and legal domain reasoning competencies, e.g., for regulating the behaviour of IASs. This requires the implantation of L1- and L2-reasoning capabilities within a suitably designed governance component for the IAS to be regulated.

Concrete engineering steps for layers L1, L2 and L3 are presented below, and pointers to directly related work and illustrating examples are provided. The LogiKEy methodology has been developed, refined and tested in prior research projects and also in lecture courses at Freie Universität Berlin and at University of Luxembourg. We have thus gained experience that LogiKEy well supports both research and education [91] at the depicted layers.

While each layer in the methodology can serve as an entry point, we here start our systematic exhibition at layer L1. In concrete research and education projects, one may alternatively start from layers L2 or L3; the formalization of Gewirth’s PGC, for example, started at layer L2. Entry at layers L3 or L2 will increasingly become the default, when our library of reusable logic encodings at layer L1 grows, so that extensive engineering work at layer L1 can largely be avoided in future applications.

7.1 Layer L1 – Logics and logic

combinations

Logic: Select a logic or logic combination

Logic examples include DDL or system E, cf. Sect. 3. The need for a non-trivial logic combination was, e.g., identified in the case study on Gewirth’s PGC [12]; cf. Sect. 6.2 and Fig. 9. As explained in detail by Fuenmayor and Benzmüller [12], in this work a higher-order extension of DDL was combined with relevant parts of Kaplan’s logic of demonstratives (LD) [89, 92]. Moreover, a combination of multi-epistemic logic with an operator for common knowledge was used in an automation of the Wise Men Puzzle [24, 93].

Semantics: Select a semantics for the chosen logic or logic

combinations

This step is preparing the automation of the logic or logic combination, using the SSE approach, in the next step. Suitable semantics definitions for DDL and system E are given in the mentioned original articles. To arrive at a semantics for the logic combination used in the PGC formalization, DDL’s original semantics was extended and combined, utilising a product construction [6, §1.2.2], with Kaplan’s semantics for LD. In the work on the Wise Men Puzzle, a logic fusion [6, §1.2.1] was used, and the semantics for multi-epistemic logic and common knowledge were adopted from Sergot [94].

Automate: Automate the selected logics and logic

combinations in HOL

In this step a selected logic or logic combination is shallowly embedded by directly encoding its semantics in meta-logic HOL. This is practically supported in theorem provers and proof assistant systems for HOL, such as Isabelle/HOL or Leo-III. SSEs thus constitute our preferred solution to the automation challenge, since they enable the reuse of already existing reasoning machinery.141414However, also deep logic embeddings in HOL can be utilized, and even combinations of both techniques are supported. The abstraction layers used by Kirchner, Benzmüller and Zalta [37], for example, support a deep embedding of a proof calculus for higher-order hyper-intensional (relational) logic S5 in HOL on top of an SSE for the same logic in HOL; both reasoning layers can then been exploited for proof automation and mutual verification; cf. also Footnote 5 and Sect. 8.

Assess: Empirically assess the SSEs with model finders and

theorem provers

The consistency of an SSE can be verified with model finders, and ATP systems can be employed to show that the original axioms and proof rules of an embedded logic can be derived from its semantics. Respective examples have been presented in the literature [13, 37]. If problems are revealed in this assessment, modifications in previous steps maybe required.

Faithfulness: Prove the faithfulness of the SSEs

Part of this challenge is computationally addressed already in the previous step. In addition, explicit soundness and completeness proofs should be provided using pen and paper methods. An example is Thm. 4 in Sect. 4, which proves the faithfulness of the SSE of system E in HOL. If faithfulness cannot be established, modifications in the first three steps maybe required.

Implications: Explore the implications of the embedded

logics and logic combinations

What theorems are implied by an SSE? Are the expectations matched? For the SSE of the combination higher-order DDL with Kaplan’s LD in HOL it has, e.g., been checked [13], whether model finders still report countermodels to propositional and first-order variants of the Chisholm paradox [86]. If the investigated implications do not match the expectations, modifications in the first three steps maybe required.

Benchmarks: Test the logic automation against benchmarks

Benchmark tests not only rank LogiKEy proof automations against competitor approaches, they also provide further evidence for the practical soundness and robustness of the implemented technology; this is most relevant since pen and paper faithfulness proofs provide no guarantee that an implementation is free of bugs.151515Respective comparisons of SSE provers for first-order modal logics with competitor systems have been presented in the literature [32, 95]. Since we are not aware of any implementation of first-order or higher-order DDLs besides our own work, we cannot yet conduct analogous evaluation studies for our SSE-based DDL provers.

Contribute: Contribute to the built-up and extension of

benchmark suites

7.2 Layer L2 – Domain Theories

Select an ethico-legal domain theory of interest

An example is Gewirth’s PGC from Sect. 6.2. Another example is the German road traffic act, which we have started to work on in student projects as part of our lecture courses. Alternatively, or in addition, one might be interested in designing, from scratch, new sets of ethical rules to govern the behaviour of autonomous cars.

Analyse the ethico-legal domain theory

Mutually related aspects are addressed in this step, and requirements for the logics and logic combinations imported from layer L1 are identified.

Determine a suitable level of abstraction. Can relevant notions and concepts be suitably abstracted, e.g., to a purely propositional level (as often done in toy examples in AI), or would that cause an oversimplification regarding the intended applications at layer L3? 2. 2.

Identify basic notions and concepts. What are the most essential concepts addressed and utilized in a given domain theory. Which basic entities need to be explicitly referred to, and which properties, relations and functions for such entities must be explicitly modelled? For example, notions identified as relevant for Gewirth’s PGC, cf. Fig. 9, include the relations ActsOnPurpose, NeedsForPurpose and InterferesWith, the predicates Good (for Goodness) and FWB (free will and well-being), and the defined terms RightTo (has right to) and PPA (is a prospective purposive agent). As a result of this analysis, a signature is obtained together with a set of associated foundational axioms and definitions.

In this step dependencies on very generic notions, such as mereological terms, may be revealed whose precise meanings are left implicit. For the formalization of such notions one may consult other sources, including existing upper ontologies.161616Upper ontologies formally define very generic terms that are shared across several domains. Import from external upper ontologies requires some conceptual and logical fit which often is not given. 3. 3.

Identify notions of quantification. Domain theories may contain universal and/or existential statements that cannot or should not be abstracted away. Careful assessment of the precise characteristics of each of the identified quantifiers is then advisable. In particular, when quantifiers interact with linguistic modalities, see below, the question arises whether, e.g., the Barcan formulas [96] should hold or not. Different kinds of quantifiers may thus have to be provided at layer L1. 4. 4.

Identify linguistic modalities. Ethico-legal domain theories are challenged, in particular, by deontic modalities (e.g., ”an entity is permitted/obliged to …”), and they may occur in combination with other modalities. In Gewirth’s PGC, for example, deontic and alethic modalities are relevant. Notions of time or space are further examples that frequently need to be addressed. Combinations of modalities may thus have to be provided at layer L1.

Determine a suitable logic or logic combination

The previous step identifies essential logical requirements for the formalization task at hand. Based on these requirements a suitable base logic or logic combination must be determined or devised and imported from layer L1; if not yet provided, further work at layer L1 is required.

Formalize the ethico-legal domain theory

During the formalization process regular sanity checks, e.g., for in-/consistency or logical entailment, with ATP systems and model finders are advisable, cf. Sect. 5.1. This serves two different purposes: early detection of misconceptions and errors in the formalization process, and early testing of the proof automation performance. If the reasoning performance is weak early on, then countermeasures maybe taken, for example, by considering alternative choices in the previous steps.171717Remember Footnote 11, where respective issues for T-STIT-logic where identified by such experiments.

Explore theory implications and check whether expectations are matched

If the computationally explored and assessed implications of the formalized domain theory are not matching the expectations, modifications in one of the previous steps are required.181818Respective experiments have been conducted, e.g., in the context of the formalisation of Gödel’s ontological argument. In these experiments it has been confirmed with automated reasoning tools that monotheism and the modal collapse (expressing “there are no contingent truths”, “there is no free will”) were implied by Gödel’s theory; cf. [97]. Both implications might not be in-line with our expectations or intentions, and the modal collapse has in fact motivated further emendations of Gödel’s theory and of the utilized foundational logic.

Contribute: Contribute to the built-up of benchmark suites

for domain theories

7.3 Layer L3 – Applications

Layer L3 deploys the ethico-legal domain theories from layer L2 in practical applications, e.g., to regulate the behaviour of an IAS.

Select an application scenario and define the objectives

Already mentioned examples include the ethico-legal governance of autonomous cars and ethico-legal reasoner in the smart home example.

Ethical governor component

A suitable explicit ethical governor architecture must be selected and provided. This step connects with recent research area on governing architectures for intelligent systems [98, 99, 100].

Populate the governor component with the ethico-legal domain theory and reasoner

Select the ethico-legal domain theory to be employed; if not yet formalized and automated, first consult layer L2. Otherwise integrate the ethico-legal domain reasoner obtained from layer L2 with the governor component and perform offline tests. Does it respond to example queries as expected and with reasonable performance? In particular, can it check for compliance of a considered action in an IAS wrt. the formalized ethico-legal domain theory?

Properly test, assess and demonstrate the system in

practice

7.4 Note on open-texture and concept explication

A goal of LogiKEy at layer L2 is to support, among others, the systematic exploration, formalization and automation of new regulatory theories for IASs. Ideally, such a development is conducted by an expert team comprised of logicians, legal and ethical experts and practitioners representing the addressed application domain. Alternatively, such a theory formalization process may start from existing legislation. A known challenge in the latter case concerns the open-texture of informal legal texts; e.g., relevant concepts may probably be specified rather vaguely and deliberately left open for interpretation in context. In prior work the open-texture challenge occurred also in other contexts, e.g., in the analysis philosophical arguments. In a recent reconstruction and verification of Lowe’s ontological argument [101], for example, underspecified notions such as necessary being and concrete being had to be suitably interpreted in context to finally arrive at a verified formalisation of the argument; cf. Fuenmayor and Benzmüller [36], where a respective computer-supported, iterative interpretation process is presented and explained. The LogiKEy methodology does not eliminate the open-texture challenge. However, it provides suitable means to address it in an interaction between human experts and computational tools. The idea is to computationally explore suitable explications or emendations of vague concepts for a given application context. The logical plurality, flexibility and expressivity supported in LogiKEy thereby constitutes a distinctive virtue that is, as far as we are aware of, unmatched in related work. Moreover, ongoing work on computational hermeneutics [102] aims at reducing the need for user interaction in future applications by automating the exploration of choice points in concept explication and beyond.

8 Related work

Relevant own related work has already been mentioned in the previous sections; the referenced works contain technical details and evidence that we cannot address in full depth in this article. Further references to own work and that of others are provided below. Many of those contain illustrating examples and further details that may well benefit researchers or students interested in adopting the LogiKEy methodology in their own work. They also provide useful information on various intellectual roots of the research presented in this article.

8.1 Machine ethics and deontic logic

The questions how transparency, explainability and verifiability can best be achieved in future intelligent systems and whether bottom-up or top-down architectures should be preferred are discussed in a range of related articles; cf., e.g., [1, 103, 104, 105, 106, 107, 108, 109] and the references therein. For example, Dennis et al. [109] make a compelling case for the use of so-called formal verification—a well-established technique for proving correctness of computer systems—in the area of machine ethics. The idea is to use formal methods to check whether an autonomous system (e.g., an unmanned civilian aircraft) is compliant with some specific ethico-legal rules (e.g., the Rules of the Air) when making decisions. An ethical rule is represented as a formula of the form “$\mathrm{do(a)}\Rightarrow_{c}\neg E\phi$”, denoting that doing action a counts as a violation of ethical principle $\phi$. However, they do not specify in full the syntax and semantics of their operator $E$. It may be valuable to further explore the relationship between this work and the approach outlined in the present article. As the authors observe, on p. 6 of their article, the $E$ modal operator resembles the obligation operator $\bigcirc$ used in deontic logic.

Further related work includes a range of implemented theorem proving systems. A lean but powerful connection-based theorem prover for first-order modal logics, covering also SDL, has been developed by Otten [110]. A tableaux-based propositional reasoner is employed in the work of Furbach and Schon [110, 27] and first-order resolution methods for modal logics have been contributed by Schmidt and Hustadt [111]. Further related work includes a reasoner for propositional defeasible modal logic by Governatori and his team [26]. Their reasoner supports defeasible reasoning, but it is less flexible than ours, because it does not allow the user to easily switch between different systems of normative reasoning and explore their properties. A reasoner for expressive contextual deontic reasoning was proposed by Bringsjord et al. [28]. Pereira and Saptawijaya [29, 112, 113] present a solution that implements deontic and counterfactual reasoning in Prolog.

We are not aware of any attempts to automate, within a single framework, such a wide portfolio of CTD resistant propositional, first-order and higher-order deontic logics as we report it in this article. Note that in addition to the features of the above related systems our solution also supports intuitive user-interaction and most flexible logic combinations.

The SSE approach has also been implemented in the Leo-III theorem prover, so that the prover now provides native language support for a wide range of modal logics and for DDL [71, 32]. A recent, independent study [114] shows that Leo-III, due to its wide range of directly supported logics, has become the most powerful and most widely applicable ATP system existent to date.191919The assessment has included various variants of classical first-order and higher-order logic benchmark problems. First-order and higher-order deontic logics and other non-classical logics were still excluded though. Their inclusion would clearly further benefit the Leo-III prover.

The flexibility of the SSE approach has been exploited and demonstrated in particular in the case study on Gewirth’s PGC that we have presented in Sect. 6.2. Related work on the mechanization of ambitious ethical theories includes the already mentioned automation of the “Doctrine of Double Effect” by Govindarajulu and Bringsjord [83].

8.2 Universal logical reasoning

Related experiments, at LogiKEy layers L1 and L2, with the SSE approach have been conducted in metaphysics [97, 115]. An initial focus thereby has been on computer-supported assessments of rational arguments, in particular, of modern, modal logic variants of the ontological argument for the existence of God. In the course of these experiments, in which the SSE approach was applied for automating different variants of higher-order quantified modal logics, the theorem prover LEO-II even detected an previously unnoticed inconsistency in Gödel’s [116] modal variant of the ontological argument, while the soundness of the emended variant by Scott [117] was confirmed and all argument steps were verified. Further modern variants of the ontological argument have subsequently been studied with the approach, and theorem provers have even contributed to the clarification of an unsettled philosophical dispute [118]. The good performance of the SSE approach in previous work has been a core motivation for the new application direction addressed here. In previous work, Benzmüller and colleagues also studied actualist quantifiers [76, 77], and it should be possible to transfer these ideas to our setting.

Another advantage of the SSE approach, when implemented within powerful proof assistants such as Isabelle/HOL, is that proof construction, interactive or automated, can be supported at different levels of abstraction. For this note that proof protocols/objects may generally serve two different purposes: (a) they may provide an independently verifiable explanation in a typically well-defined logical calculus, or (b) they may provide an intuitive explanation to the user why the problem in question has been answered positively or negatively. Many reasoning tools, if they are offering proof objects at all, do generate only objects of type (a). The SSE approach, however, has already demonstrated its capabilities to provide both types of responses simultaneously in even most challenging logic settings. For example, a quite powerful, abstract level theorem prover for hyper-intensional higher-order modal logic has been provided by Kirchner and colleagues [38, 37]. He encoded, using abstraction layers, a proof calculus for this very complex logic as proof tactics and he demonstrated how these abstract level proof tactics can again be automated using respective tools in Isabelle/HOL. Kirchner then successfully applied this reasoning infrastructure to reveal, assess and intuitively communicate a non-trivial paradox in Zalta’s “Principia Logico-Metaphysica” [119].

Drawing on the results and experiences from previous work, the ambition of our ongoing project is to further extend the already existing portfolio of deontic logics in Isabelle/HOL towards a most powerful, flexible and scalable deontic logic reasoning infrastructure. A core motivation thereby is to support empirical studies in various application scenarios, and to assess and compare the suitability, adequacy and performance of individual deontic logic solutions for the engineering of ethically and legally regulated agents and explainable intelligent systems. It is relevant to mention that proof automation in Isabelle/HOL, and also in related higher-order ATP systems such as Leo-III [20], is currently improving at good pace. These developments are fostered in particular by recently funded research and infrastructure projects.202020Prominent example projects include Matryoshka (http://matryoshka.gforge.inria.fr) and ALEXANDRIA (http://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/).

8.3 Discussion

We propose higher-order logic as a uniform and highly expressive formal framework to represent and experiment with normative theories of ethico-legal reasoning. To some researchers, this may seem paradoxical for two reasons. First of all, we do no longer aim for a unique and standard deontic logic which can be used for all applications, but we do propose to use higher-order logic as a unique and formal framework to represent normative theories. So what exactly is the difference between a unique deontic logic and a unique formal framework? The second apparent paradox is that we propose higher-order logic for tool support, whereas it is well-known that higher-order logic has theoretical drawbacks and is undecidable.

These two apparent paradoxes can be explained away by our methodology of representing normative theories in higher-order logic. There are many ways in which a normative theory can be represented in higher-order logic, and only a few of them will be such that the formal methods of the tool support can be suitably applied to them. Therefore, the representation of deontic logics in higher-order logic is an art, and each new representation has to come with a proof that the embedding is faithful. These proofs play a similar role in our formal framework as soundness and completeness proofs play in most of the traditional work of deontic logic.

9 Further research

In future work, the range of normative theories must be extended, and the currently represented theories must be further optimized. In particular, a wider range of explicit ethical theories must be studied and formalized. We have made historical and current developments in normative reasoning practically accessible for the use in machine ethics. We showed how our approach can support research in normative reasoning itself. The use of computer-assisted exploration and assessment of new deontic logics provides immediate feedback from systems to property checks. This is particularly valuable for unifying and combining different logics and for experimental studies. For example, since our approach supports meta-logical investigations, conjectured relationships between I/O logics and conditional logics can be formally assessed in future work.

Moreover, our approach can also be used for other relevant purposes. In education, for example, the different logics discussed in this article can now be integrated in computer-supported classroom education. First reassuring results have been obtained in lecture courses at University of Luxembourg (Intelligent Agents II) and Freie Universität Berlin (Universal Logical Reasoning and Computational Metaphysics). Students start exploring existing deontic logics and other non-classical logics without the need for a deep a priori understanding of them. They can use the logics in small or larger examples, modify them, assess their modifications, etc.

In agent simulation, we plan the embodiment/implementation of explicit ethical theories in simulated agents. We can then investigate properties for single agents, but beyond that also study agent interaction and the behaviour of the agent society as a whole. To this end the agent-based LeoPARD framework [84], which is underlying the Leo-III prover, will be adapted and utilized in future work.

10 Conclusion

It is the availability of powerful systems such as Isabelle/HOL or Leo-III for tool support that allows our approach to revolutionize the field of formal ethics. Though the use of higher-order logic may come as a paradigm shift to the field of ethical reasoning, it is an insight which is already well established in the area of formal deduction. Whereas it is far from straightforward to represent deontic logics in higher-order logic, once a deontic logic has been represented, it becomes much easier to make small changes to them and see the effect of these changes—and this is exactly how our approach supports the design of normative theories of ethico-legal reasoning. It is in the ease in which the user can work with and adapt existing theories, how the design of normative theories is made accessible to non-specialist users and developers.

To validate our approach we have embedded the main strands of current deontic logic within higher-order logic, and we have experimented with the approach over the past two years.

Our LogiKEy normative reasoning framework and infrastructure supports empirical studies on ethico-legal theories in which the underlying logic formalisms itself can be flexibly varied, assessed and compared in context. This infrastructure can fruitfully support the development of much needed logic based approaches towards ethical agency. The solution we have presented supports a wide range of specific deontic logic variants, and it also scales for their first-order and higher-order extensions.

The use of tool support for ethico-legal reasoning is not only fruitful to develop new normative theories, it is now being employed also in teaching, and we plan to use it as a formal framework for simulation. Another promising application is the use of our approach for the study of deontic modality in natural language processing. In linguistics the use of higher-order logic is already adopted for the semantics of natural language, and we believe that our framework can also support studies of the pragmatic aspects of the use of deontic modality.

Acknowledgments:

We thank the anonymous reviewers for their valuable feedback and for various comments, which helped to significantly improve this paper. We also thank Ali Farjami, David Fuenmayor, Tobias Gleißner, Alexander Steen, Valeria Zahoransky and several further colleagues for their contributions to this project.