In agent theory, epistemic trust is used to infer beliefs, for example by filtering out the information the agent receives from untrustworthy agents. Moreover, trust itself can be inferred from other information. We introduce a simple information filtering architecture that clearly distinguishes the relation between the two kinds of inference. We provide a logical analysis of the architecture, based on a new family of input/output logics. We then explore information filtering and belief manipulation within this formal framework. Our key finding is that with this architecture, some of the widely debated logical rules for trust inference are redundant with respect to information-filtering mechanisms and some others are redundant with respect to belief manipulation.

Inspired by revealed preference in economics, we study revealed epistemic trust: an agent’s (dis)trust in an information source is typically hidden, while her accept/reject behavior leaves observable traces. We model such traces by an acceptance function that maps each reported set of formulas to the subset the agent accepts. We develop two complementary models: a white-list mode, where acceptance is supported by trusted information in the report, and a black-list mode, where acceptance avoids distrusted patterns via a cautious remainder-set/full-meet construction. For both modes, we provide postulate-based representation theorems and show how canonical "revealed" trust and distrust cores can be reconstructed from the acceptance function itself.

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.

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.

Abstract We introduce a logic of knowledge in a framework in which knowledge is treated as a kind of belief. The framework is based on a standard KD45 characterization of belief, and the characterization of knowledge undergoes the classical tripartite analysis that knowledge is justified true belief, which has a natural link to the studies of logics of evidence and justification. The interpretation of knowledge avoids the unwanted properties of logical omniscience, independent of the choice of the base logic of belief. We axiomatize the logic, prove its soundness and completeness and study the computational complexity results of the model checking and satisfiability problems. We extend the logic to a multi-agent setting and introduce a variant in which belief is characterized in a weaker system to avoid the problem of logical omniscience.