2025 • In Lynce, Ines (Ed.) ECAI 2025 - 28th European Conference on Artificial Intelligence, including 14th Conference on Prestigious Applications of Intelligent Systems, PAIS 2025 - Proceedings
AI systems; Autonomous decision; Condition; Data subjects; Decision-based; Dynamic logic; Embeddings; Legal concepts; Possible worlds; Right-to-know; Artificial Intelligence
Abstract :
[en] 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.
PASETTO, Luca ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
Benzmüller, Christoph; Otto-Friedrich-Universität Bamberg, Germany ; Freie Universität Berlin, Germany
LI, Xu ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
MARKOVICH, Réka ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)
External co-authors :
yes
Language :
English
Title :
Reasoning with Epistemic Rights and Duties: Automating a Dynamic Logic of the Right to Know in LogiKEy
Publication date :
21 October 2025
Event name :
ECAI 2025: 28th European Conference on Artificial Intelligence
Event place :
Bologna, Ita
Event date :
25-10-2025 => 30-10-2025
Audience :
International
Main work title :
ECAI 2025 - 28th European Conference on Artificial Intelligence, including 14th Conference on Prestigious Applications of Intelligent Systems, PAIS 2025 - Proceedings
This work was supported by the Luxembourg National Research Fund (FNR) through the project Logical methods for Deontic Explanations (INTER/DFG/23/17415164/LODEX) and the project Deontic Logic for Epistemic Rights (OPEN O20/14776480). We also thank the anonymous reviewers for their fruitful feedback.
C. Areces, P. Fontaine, and S. Merz. Modal satisfiability via SMT solving. In R. Hennicker and R. de Nicola, editors, Software, Services, and Systems, volume 8950 of LNCS, pages 30-45. Springer, 2015.
G. Aucher, G. Boella, and L. van der Torre. A dynamic logic for privacy compliance. Artificial Intelligence and Law, 19(2):187, 2011.
F. Baader and S. Ghilardi. Unification in modal and description logics. Logic Journal of the IGPL, 19(6):705-730, 2010.
P. Balbiani and P. Seban. Reasoning about permitted announcements. Journal of Philosophical Logic, 40(4):445-472, 2011.
C. Benzmuller. Cut-elimination for quantified conditional logic. Journal of Philosophical Logic, 46(3):333-353, 2017.
C. Benzmuller. Universal (meta-)logical reasoning: Recent successes. Science of Computer Programming, 172:48-62, 2019.
C. Benzmuller. Universal (meta-)logical reasoning: The wise men puzzle (Isabelle/HOL Dataset). Data in Brief, 24(103823):1-5, 2019.
C. Benzmuller and P. Andrews. Church's Type Theory. In E. N. Zalta and U. Nodelman, editors, The Stanford Encyclopedia of Philosophy. Stanford University, Spring 2024 edition, 2024.
C. Benzmuller and D. Miller. Automation of higher-order logic. In D. M. Gabbay et al., editors, Handbook of the History of Logic, Volume 9-Computational Logic, pages 215-254. North Holland, 2014.
C. Benzmuller and L. C. Paulson. Quantified multimodal logics in simple type theory. Logica Universalis, 7(1):7-20, 2013.
C. Benzmuller and S. Reiche. Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy. Journal of Logic and Computation, 33(6):1243-1269, 2023.
C. Benzmuller, C. Brown, and M. Kohlhase. Higher-order semantics and extensionality. Journal of Symbolic Logic, 69(4):1027-1088, 2004.
C. Benzmuller, A. Farjami, and X. Parent. Aqvist's dyadic deontic logic E in HOL. FLAP, 6(5):733-755, 2019.
C. Benzmuller, A. Farjami, D. Fuenmayor, et al. LogiKEy workbench: Deontic logics, logic combinations and expressive ethical and legal reasoning (Isabelle/HOL dataset). Data in Brief, 33(106409):1-10, 2020.
C. Benzmuller, X. Parent, and L. van der Torre. Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. Artificial Intelligence, 287:103348, 2020.
C. Benzmuller, A. Farjami, and X. Parent. Dyadic deontic logic in HOL: Faithful embedding and meta-Theoretical experiments. In S. Rahman et al., editors, New Developments in Legal Reasoning and Logic: From Ancient Law to Modern Legal Systems, volume 23 of Logic, Argumentation & Reasoning. Springer Nature, 2022.
C. Benzmuller, D. Fuenmayor, and B. Lomfeld. Modelling valueoriented legal reasoning in LogiKEy. Logics, 2(1):31-78, 2024.
C. Benzmuller et al. I/O logic in HOL. FLAP, 6(5):715-732, 2019.
C. Benzmuller. Faithful logic embeddings in HOL-deep and shallow. In CADE-30, volume 15943 of LNCS, pages 280-302. Springer, 2025.
J. Blanchette, S. Bohme, and L. Paulson. Extending Sledgehammer with SMT solvers. Journal of Automated Reasoning, 51:116-130, 2011.
A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5(2):56-68, 1940.
I. A. Ciardelli and F. Roelofsen. Inquisitive dynamic epistemic logic. Synthese, 192:1643-1687, 2015.
M. Cristani et al. The architecture of a reasoning system for defeasible deontic logic. Procedia Comput. Sci., 225:4214-4224, 2023.
D. Doligez, J. Kriener, L. Lamport, et al. Coalescing for reasoning in first-order modal logics. In C. Benzmuller et al., editors, ARQNL 2014, volume 33 of EPiC Series in Computing, pages 1-16. EasyChair, 2014.
H. Dong and O. Roy. Dynamic logic of legal competences. J. Log. Lang. Inf., 30(4):701-724, 2021.
European Parliament and Council of the European Union. Regulation (EU) 2016/679 (GDPR), 2016.
J. Gerbrandy andW. Groeneveld. Reasoning about information change. Journal of Logic, Language and Information, 6:147-169, 1997.
S. Gerke, T. Minssen, and G. Cohen. Ethical and legal challenges of artificial intelligence-driven healthcare. In A. Bohr et al., editors, Artificial Intelligence in Healthcare, pages 295-336. Academic Press, 2020.
J. Gibbons and N. Wu. Folding domain-specific languages: Deep and shallow embeddings (functional pearl). In J. Jeuring and M. M. T. Chakravarty, editors, ICFP 2014, pages 339-347. ACM, 2014.
T. Gleisner, A. Steen, and C. Benzmuller. Theorem provers for every normal modal logic. In T. Eiter et al., editors, Proc. of LPAR-21, volume 46 of EPiC Series in Computing, pages 14-30. EasyChair, 2017.
K. Godel. Uber formal unentscheidbare Satze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38(1):173-198, 1931.
J. Groenendijk and M. Stokhof. Chapter 19-questions. In J. van Benthem and A. ter Meulen, editors, Handbook of Logic and Language, pages 1055-1124. North-Holland, Amsterdam, 1997.
L. Henkin. Completeness in the theory of types. The Journal of Symbolic Logic, 15(2):81-91, 1950.
W. N. Hohfeld. Fundamental legal conceptions applied in judicial reasoning. In W. W. Cook, editor, Fundamental Legal Conceptions Applied in Judicial Reasoning and Other Legal Essays, pages 23-64. New Haven: Yale University Press, 1923.
U. Hustadt et al. Model construction for modal clauses. In Automated Reasoning, volume 14740 of LNCS, pages 3-23. Springer, 2024.
A. J. I. Jones and M. Sergot. A formal characterisation of institutionalised power. Log. J. IGPL, 4(3):427-443, 1996.
S. Kanger and H. Kanger. Rights and parliamentarism. Theoria, 32(2): 85-115, 1966.
B. Kooi and B. Renne. Arrow update logic. The Review of Symbolic Logic, 4(4):536-559, 2011.
H.-P. Lam and G. Governatori. The making of SPINdle. In G. Governatori et al., editors, Rule Representation, Interchange and Reasoning on the Web, number 5858 in LNCS, pages 315-322. Springer, 2009.
N. Leone and F. Ricca. Answer set programming: A tour from the basics to advanced development tools and industrial applications. In Reasoning Web, volume 9203 of LNCS, pages 308-326. Springer, 2015.
N. Leone, G. Pfeifer, et al. The DLV system for knowledge representation and reasoning. ACM Trans. Comput. Log., 7(3):499-562, 2006.
X. Li and R. Markovich. A dynamic logic of the right to know. FLAP, 12(2):221-250, 2025.
X. Li, D. Gabbay, and R. Markovich. Dynamic Deontic Logic for Permitted Announcements. In Proc. of the 19th Intl. Conf. on Principles of Knowledge Representation and Reasoning, pages 226-235, 2022.
L. Lindahl. Position and change: A study in law and logic. Synthese Library. Springer Dordrecht, 1 edition, 1977.
D. Makinson. On the formal representation of rights relations. Journal of Philosophical Logic, 15(4):403-425, 1986.
R. Markovich. Understanding Hohfeld and Formalizing Legal Rights: The Hohfeldian Conceptions and Their Conditional Consequences. Studia Logica, 108, 2020.
C. Nalon and C. Dixon. Clausal resolution for normal modal logics. Journal of Algorithms, 62(3):117-134, 2007.
C. Nalon, U. Hustadt, and C. Dixon. A resolution-based theorem prover for knkn: Architecture, refinements, strategies and experiments. Journal of Automated Reasoning, 64, 2018.
C. Nalon, C. Dixon, and U. Hustadt. Modal resolution: Proofs, layers, and refinements. ACM Trans. Comput. Logic, 20(4), 2019.
T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin, Heidelberg, 2002.
X. Parent and C. Benzmuller. Automated verification of deontic correspondences in Isabelle/HOL-first results. In Proc. of ARQNL 2022, volume 3326, pages 92-108. CEUR-WS.org, 2023.
X. Parent and C. Benzmuller. Conditional normative reasoning as a fragment of HOL. J. Appl. Non-Class. Log., 34:561-592, 2024.
L. Pasetto and C. Benzmuller. Implementing the Fatio protocol for multi-agent argumentation in LogiKEy. In Proc. of ARQNL 2024, volume CEUR-3875, pages 38-47. CEUR-WS.org, 2024.
F. Pfenning and C. Elliott. Higher-order abstract syntax. In R. L. Wexelblat, editor, Proc. of the ACM SIGPLAN'88 Conf. on Progr. Language Design and Implementation (PLDI), pages 199-208. ACM, 1988.
L. Robaldo et al. Compliance checking on first-order knowledge with conflicting and compensatory norms: A comparison among currently available technologies. Artif. Intell. Law, 32(2):505-555, 2023.
K. Satoh, K. Asai, T. Kogawa, et al. Proleg: An implementation of the presupposed ultimate fact theory of Japanese civil code by PROLOG technology. In T. Onada et al., editors, New Frontiers in Artificial Intelligence, pages 153-164. Springer Berlin Heidelberg, 2011.
R. Sebastiani and M. Vescovi. Automated reasoning in modal and description logics via sat encoding: The case study of k(m)/alcsatisfiability. J. Artif. Intell. Res., 35:343-389, 2009.
G. Sileno and M. Pascucci. Disentangling deontic positions and abilities: A modal analysis. In F. Calimeri et al., editors, Proc. of the 35th Edition of the Italian Conf. on Comp. Logic (CILC), pages 36-50, 2020.
UNESCO. Recommendation on the ethics of ai. https://unesdoc.unesco. org/ark:/48223/pf0000381137, 2022. Accessed: 2025-05-06.
J. van Benthem and , S. Minic?a. Toward a dynamic logic of questions. Journal of Philosophical Logic, 41(4):633-669, 2012.
J. van Benthem et al. Symbolic model checking for dynamic epistemic logic-S5 and beyond. J.Log.Comp., 28(2):367-402, 2018.
L. Watson. The Right to Know: Epistemic Rights and Why We Need Them. Routledge Focus on Philosophy. Routledge, 1 edition, 2021.
