Pasetto, LucaLucaPasettoBenzmüller, ChristophChristophBenzmüller0000-0002-3392-3093Markovich, RékaRékaMarkovich2026-05-272026-05-272026https://fis.uni-bamberg.de/handle/uniba/115278Neurotechnology and AI are expanding how systems can access and influence mental states, raising concerns about mental privacy. Yet the legal status of a right to mental privacy remains unsettled: it is often treated as a special case of the right to privacy, while others argue it is grounded in freedom of thought, which protects against coercion to disclose or adopt beliefs. Despite the regulatory and technological stakes, it is unclear how these epistemic rights formally interact or how autonomous systems can reason about them. We address this by introducing a Logic for Mental Privacy (LMP) that integrates multi-modal formalizations of the right to privacy and freedom of thought as epistemic claim-rights. We mechanize LMP in Isabelle/HOL via shallow semantical embeddings in Higher-Order Logic within the LogiKEy framework, and use automated reasoning to study its normative consequences. A case study shows how access to cognitive data can steer belief formation while remaining compliant with duties on explicitly protected content, yielding an indirect compromise of freedom of thought and exposing a normative gap around mental privacy. Overall, we show how legal knowledge representation and automated reasoning can inform debates on neurotechnology governance and support the design and analysis of normative multiagent systems.engNormative Multiagent SystemsLegal Knowledge RepresentationAutomated ReasoningModal LogicHigher-Order LogicLogiKEyMental PrivacyFreedom of ThoughtNormative PositionsFormalizing Mental Privacy in LogiKEyconferenceobject10.65109/ptsf2244