We propose a separation logic where resources are histories (sequences) of epistemic actions so that resource update means concatenation of histories and resource decomposition means splitting of histories. This separation logic, called AMHSL, allows us to reason about the past: does what is true now depend on what was true in the past, before certain actions were executed? We show that the multiplicative connectives can be eliminated from a logical language with also epistemic and action model modalities, if the horizon (...) of epistemic actions is bounded. (shrink)

The aim of the paper is to present two natural deduction systems for Intuitionistic Sentential Calculus with Identity ( ISCI ); a syntactically motivated \(\mathsf {ND}^1_{\mathsf {ISCI}}\) and a semantically motivated \(\mathsf {ND}^2_{\mathsf {ISCI}}\). The formulation of \(\mathsf {ND}^1_{\mathsf {ISCI}}\) is based on the axiomatic formulation of ISCI. Its rules cannot be straightforwardly classified as introduction or elimination rules; ISCI -specific rules are based on axioms characterizing the identity connective. The system does not enjoy the standard subformula property, but due (...) to the normalization procedure non-subformulas can label only leaves of proofs. In \(\mathsf {ND}^2_{\mathsf {ISCI}}\), we propose only two general identity-related rules, in reference to the treatment of the identity connective in First-Order Logic. (shrink)

In this paper we present an extension of (bunched) separation logic, Boolean BI, with epistemic and dynamic epistemic modalities. This logic, called action model separation logic ( \(\mathrm {AMSL}\) ), can be seen as a generalization of public announcement separation logic in which we replace public announcements with action models. Then we not only model public information change (public announcements) but also non-public forms of information change, such as private announcements. In this context the semantics for the connectives \(*\) and (...) \(\mathrel {-*}\) from separation logic are epistemic versions of their usual semantics. This is because formulas are interpreted in states, not in resources, and agents may be uncertain between different states representing the same resource. We present the logic \(\mathrm {AMSL}\) and its semantics, with a detailed case study that highlights its interest for modeling. We also prove the elimination of the dynamics modalities and discuss some alternative epistemic semantics for the separation connectives. (shrink)