We introduce a new type of proof formalism for multiagent modal logics with S5-type modalities, viewed here as a logic of multiagent epistemic reasoning, and use this formalism to give a constructive proof that multiagent S5 enjoys a strong form of Craig interpolation with respect to both propositional variables and agents, the latter in the form of agent-indexed knowledge modalities. Our new proof formalism combines the features of hypersequents to represent S5 modalities with nested sequents to represent the T-like modality alternations. Combining these features is necessary to obtain computationally effective interpolation for agents rather than merely propositional variables, and we further show that our new proof formalism is sound and complete, cut-free, strongly terminating, and yields decidability and the finite model property for multiagent S5.
In this paper, we enhance the many-sorted hybrid logic with an algebraic structure over nominals. In this way, a world or a state might be referred by a nominal term and the set of worlds has an algebraic structure. We define algebraic structures for the proposed logic, as pairs of algebras and Boolean algebras with operators and we prove frame and algebraic completeness theorems. As an example of this system, we define an epistemic logic with actions for specifying and analysing security protocols.
In this paper we are interested in the dual composition of two relations. The dual composition is defined to be the composition of relations on the dual order structure of a distributive allegory if it exists. We investigate this operation and the corresponding algebraic/categorical structures. In particular, we show that its existence guarantees that complemented relations are closed under composition, and we investigate when the dual composition of two univalent relations is again univalent.
We study uniform continuity for functions on coinductive data. The familiar 1-Lipschitz case yields the standard notion of causality from synchronous systems. We generalise this to fan-causality, where the output observed at depth n may depend on input available at a depth specified in terms of n by a monotone, unbounded map on natural numbers. This captures computations whose look-ahead varies with observation depth, including bounded fixed look-ahead as a limiting case. Final coalgebras constructed as a limit of finite iterations of a functor carry a canonical metric. We show that fan-causal maps on such final coalgebras correspond precisely to uniformly continuous maps with respect to this metric. We then construct a symmetric monoidal category whose morphisms are in bijection with fan-causal maps. This yields a compositional foundation for convenient specifications and reasoning tools for general uniformly continuous maps on final coalgebras.
