Abstract Recently, several logics modelling evidence have been proposed in the literature. These logics often also feature beliefs. We call the process or function that maps evidence to beliefs consolidation. In this paper, we use a four-valued modal logic of evidence as a basis. In the models for this logic, agents are represented by nodes, peer connections by edges and the private evidence that each agent has by a four-valued valuation. From this basis, we propose methods of consolidating the beliefs of the agents, taking into account both their private evidence as well as their peers’ opinions. To this end, beliefs are computed iteratively. The final consolidated beliefs are the ones in the point of stabilization of the model. However, it turns out that some consolidation policies will not stabilize for certain models. Finding the conditions for stabilization is one of the main problems studied here, along with other properties of such consolidations. Our main contributions are twofold: we offer a new dynamic perspective on the process of forming evidence-based beliefs, in the context of evidence logics, and we set up and address some mathematically challenging problems, which are related to graph theory and practical subject areas such as belief/opinion diffusion and contagion in multi-agent networks.

In this contribution we present arbitrary arrow update model logic (AAUML). This is a dynamic epistemic logic or update logic. In update logics, static/basic modalities are interpreted on a given relational model whereas dynamic/update modalities induce transformations (updates) of relational models. In AAUML the update modalities formalize the execution of arrow update models, and there is also a modality for quantification over arrow update models. Arrow update models are an alternative to the well-known action models. We provide an axiomatization of AAUML. The axiomatization is a rewrite system allowing to eliminate arrow update modalities from any given formula, while preserving truth. Thus, AAUML is decidable and equally expressive as the base multi-agent modal logic. Our main result is to establish arrow update synthesis: if there is an arrow update model after which φ, we can construct (synthesize) that model from φ. We also point out some pregnant differences in update expressivity between arrow update logics, action model logics, and refinement modal logic.

Proving that one language is more succinct than an-other becomes harder when the underlying seman-tics is stronger. We propose to use Formula-Size Games (as put forward by Adler and Immerman, 2003), games that are played on two sets of mod-els, and that directly link the length of play with the size of the formula. Using FSGs, we prove three succinctness results form-dimensional modal logic: (1) In system Km, a notion of ‘everybody knows ’ makes the resulting language exponentially more succinct form> 1 (2) In S5m, the same lan-guage becomes more succinct for m> 3 and (3) Public Announcement Logic is exponentially more succinct than S5m, if m> 3. The latter settles an open problem raised by Lutz, 2006. 1

This paper presents a logic for reasoning about information change in multi-agent settings based on epistemic arrow deletion in Kripke models.

We provide a strongly complete infinitary proof system for hybrid logic. This proof system can be extended with countably many sequents. Thus, although these logics may be non-compact, strong completeness proofs are provided for infinitary hybrid versions of non-compact logics like ancestral logic and Segerberg's modal logic with the bounded chain condition. This extends the completeness result for hybrid logics by Gargov, Passy, and Tinchev.