Jean-René Courtault, Hans van Ditmarsch and Didier Galmiche: An Epistemic Separation Logic

We define an Epistemic Separation Logic, called ESL, that allows us to consider epistemic possible worlds as resources that can be shared or separated, in the spirit of separation logics. After studying the semantics and illustrating the use of this logic for modelling, we provide a tableau calculus with labels and constraints that is proved sound and complete and also a countermodel generation method.