Abstract Logical investigations of the notion of secrecy are typically concentrated on tools for deducing whether private information is well hidden from unauthorized, direct, or indirect access attempts. This paper proposes a multi-agent, normal multi-modal logic to capture salient features of secrecy’s intentions. Specifically, we focus on the intentions, beliefs and knowledge of secret keepers and, more generally, of all the actors involved in secret-keeping scenarios. In particular, we investigate intentions underlying the keeping of a true secret, namely a secret concerning information known (and so true) by the secret keeper. The resulting characterization of intending to keep a true secret provides valuable insights into conditions ensuring or undermining secrecy depending on agents’ attitudes and links between secrets and their surrounding context. We present the proposed logical system’s soundness, completeness and decidability results. Furthermore, we outline some theorems with potential applications to several fields, e.g. computer science and the social sciences.

Trust is an extremely helpful construct when reasoning under uncertainty. Thus, being able to logically formalize the concept in a suitable language is important. However, doing so is problematic for three reasons. First, in order to keep track of the contextual nature of trust, situation trackers are required inside the language. Second, in order to produce trust estimations, agents rely on evidence personally gathered or reported by other agents; this requires elements in the language that can track which agents are used as referrals and how much weight is placed on their opinions. Finally, trust is subjective in nature, thus, personal thresholds are needed to track the trust-propensity of different evaluators. In this paper we propose an interpretation of a probabilistic modal language à la Hennessy-Milner in order to capture a context-aware quantitative notion of trust based on evidence. We also provide an axiomatization for the language and prove soundness, completeness, and decidability results.

Abstract Using an approach, inspired by our modernisation of Lemoine’s Geometrography, this paper proposes a new readability criterion for formal proofs produced by automated theorem provers for geometry. We analyse two criteria to measure the readability of a proof: the criterion given by Chou et al. and the one given by Wiedijk. After discussing the limitations of these two criteria, we introduce a novel approach, which provides a new criterion. We conclude discussing some future work.