It is not straightforward to reason about specific legal concepts such as epistemic rights and duties, which are crucial in AI systems that have to make autonomous decisions based on who knows what, who is entitled to know, and under what conditions information should be shared or withheld. Such issues are central to responsible AI, data governance, and regulatory compliance. A concrete application arises is in the context of the GDPR, where a data subject has a right to know whether and for what purpose her personal data is being processed, creating a duty to tell for the controller when asked. On the other hand, if the software used for the processing is proprietary, the data subject does not have the right to know its exact mechanisms, so her asking to know them does not create a corresponding duty for the data controller. In this paper, a shallow semantical embedding (SSE) of the Dynamic Logic of the Right to Know (LRK) in Higher-Order Logic is presented. The embedding is proven faithful, and it is encoded and experimented with in the Isabelle/HOL proof assistant. The SSE is then used to reason with the GDPR example encoded in LRK. The embedding of LRK differs from existing ones in how it represents the dynamic updating of the model: instead of performing changes on the domain of possible worlds, the provided SSE maintains the accessibility and neighborhood relations within the context of a formula. Updates are then handled by updating the relations, while the domain of possible worlds stays the same. The work presented in this paper contributes to the LogiKEy knowledge engineering methodology and framework, which enables experimentation with logics and logic combinations, with general and domain knowledge, and with concrete use cases.

This paper presents a formal analysis of discretionary judicial decision making through its normative characterization, focusing on the concept’s central deontic feature, the inherent freedom, and its boundaries. We use answer set programming to grasp the deontic concepts and their interplay in a judge making a discretionary decision: the nuanced permissions showing the judge’s initial freedom but finally leading up to the decision itself, and the obligations, violation of which results in the decision being wrong. The here-presented formal framework hence captures judicial discretion in a comprehensive way with symbolic AI, which initiative can pave the way for broadening the application scope of computational law.

This paper explores how to fulfill the right to explanation and support the right to challenge in automated decision-making systems by integrating symbolic methods with Large Language Models (LLMs). In cases involving automated decisions based on conflicting arguments, we first model the situation using an abstract argumentation framework. We then apply grounded semantics and discussion games to guide the explanation of the decision and support the right to challenge. Specifically, we prompt OpenAI’s flagship model (o1) to perform these reasoning steps and generate corresponding natural-language explanations. Finally, we ask the model to identify which argument would need to be modified to alter the decision, based on the formal reasoning behind the explanation. To assess the quality of the explanations, we use several state-of-the-art LLMs as evaluators. We compare three types of explanations produced by o1 with a set of criteria: those based on grounded semantics, discussion games, and a baseline explanation (in which o1 generates an explanation without any formal symbolic constraints). The results indicate that explanations based on discussion games are rated higher than those based on grounded semantics, which in turn outperform the baseline explanations. We also discuss the "right to challenge" aspect, showing that explanations based on discussion games effectively identify which arguments can be challenged to alter the decision. Overall, our findings suggest that formally guided LLMs can better fulfill the right to explanation and support the fulfillment of the right to challenge. This supports the view that integrating sub-symbolic, data-driven generative AI with symbolic, knowledge-driven AI is a fruitful way to achieve transparent AI systems that align with our societies’ legal requirements regarding digitalization.

We formalize the notions of “permitted and obligatory announcements” in the context of information security, such as privacy policy compliance. In a sender-receiver setting, we define the sender’s permitted and obligatory announcements in terms of the receiver’s ideal epistemic states (i.e., the epistemic states that comply with the given security policies). We propose two logics, LPOA and DLPOA, to reason about permitted and obligatory announcements in static and dynamic contexts, respectively. These two logics are completely axiomatized, and we also study generalizations in which the receiver’s knowledge is characterized by non-S5 logics. Our paper makes two main contributions to the formalization of permitted and obligatory announcements: First, we clarify the interplay between the sender’s permitted and obligatory announcements and the receiver’s knowledge. Second, we distinguish between weakly and strongly permitted announcements.

Judicial discretion is a central question in both the theory and the practice of law, but it received very little explicit attention from AI&Law yet. What is more, it is often considered as the limitation of what can be formalized in law, which might have serious implications for the future of computational law. In this paper, we introduce a deontic logic extended with nuanced permissions pursuing to grasp the characteristics, normative framework of and reasoning process in the discretionary decision-making of the judge. We illustrate the modeling capacity of the Discretionary Judicial Decision Logic (DJDL) by formalizing examples from an area of law where discretion plays an openly crucial role: family law, more precisely child custody cases.

This paper presents a formal model of specific reasoning patterns in conflict of laws (CoL). CoL arises when multiple countries have jurisdiction due to the diverse nationalities of the involved factors. When initiating legal action in one country, the question of which country’s substantial law to apply emerges, possibly involving the CoL regulations of other countries (in cases of transmission and renvoi). Moreover, parties contemplating legal action in a case falling under CoL often engage in a deliberation process known as forum shopping: determining which country’s CoL regulations would result in the most favorable outcome for them. Our model integrates deontic logic (specifically Input/Output logic) with proof theory and formal argumentation techniques to model both types of reasoning.

The advent of Distributed Ledger Technologies (DLTs) has paved the way for a new paradigm of traceability in all information systems areas. In the context of decision-making processes, however, DLTs are generally used only to trace the end results. In this work we argue that a reasoning system can be put in place for making these decisions, in order to enhance auditability, transparency, and finally to provide explainability. We propose the Intelligent Human-input-based Blockchain Oracle (IHiBO), a cross-chain oracle that enables the execution and traceability of formal argumentation and negotiation processes, involving the intervention of human experts. We take as reference the decision-making processes of fund managements, as trust is of crucial importance in such ``trust services''. The architecture and implementation of IHiBO are based on leveraging two-layer DLTs, smart contracts, argumentation and negotiation in a multi-agent setup. Finally, we provide some experimental results that support our discussion, namely that in the use-case we have considered our methodology can increase trust from principals to trusted services.

Bill 25 proposed by the Texas Senate in 2017 was created to eliminate the so-called ‘wrongful birth’ cause of action. This plan raised some questions about the ‘right to know’ and indirectly about rights in general. We provide a preliminary logical analysis investigating these questions by using deontic and epistemic logics within the theory of normative positions. This work contributes to the logic-based legal knowledge representation tradition, and to the formal conceptual analysis of legal rights studying the cause of action’s role in the debated relation between the Hohfeldian categories ‘claim-right’ and ‘power’.

The theory of formal argumentation distinguishes and unifies various notions of attack, support and preference among arguments, and principles are used to classify the semantics of various kinds of argumentation frameworks. In this paper, we consider the case in which we know that an argument is supporting another one, but we do not know yet which kind of support it is. Most common in the literature is to classify support as deductive, necessary, or evidentiary. Alternatively, support is characterized using principles. We discuss the interpretation of support using a legal divorce action. Technical results and proofs can be found in an accompanying technical report.

peer reviewed

Legal texts consist of hierarchically ordered and labeled (numbered) structural units (sections, subsections, paragraphs, etc.). Using the ordered layout and the labels the different parts of structural units can be easily localized and clearly referred. Nearly one-third of the structural units in the statutes we have examined are list items that can be considered as elliptical. In such cases the list items---each with unique identifying label (number)---are not complete propositions. We have trained the computer to recognize these lists and the different units and elements in them, and to create complete sentences from these. We will introduce some logical considerations that have to be reckoned with if we intend to use these complete sentences to create logical assignments to the legal regulation's content: we show how this technique influences the logical description of norms.

Using the notion of correlativity in the Hohfeldian system of rights we not just gain a better understanding of legal relations, but we can identify and differentiate existing and non-existing rights and duties. One has to see clearly, though, who the agents are in these correlative pairs and dissociate them from the State. Using SDL with an iterable and agent-indexed STIT operator we can outline the characteristics of the relations while clearly separating these roles.