We extend belief revision theory from propositional logic to the modal logic S5. Our first contribution takes the form of three new postulates (M1-M3) that go beyond the AGM ones and capture the idea of minimal change in the presence of modalities. Concerning the construction of modal revision operations, we work with set pseudo-distances, i.e., distances between sets of points that may violate the triangle-inequality. Our second contribution is the identification of three axioms (A3-A5) that go beyond the standard axioms of metrics. Loosely speaking, our main result states the following: if a pseudo-distance satisfies certain axioms, then the induced revision operation satisfies (M1-M3). We investigate three pseudo-distances from the literature (Dhaus, Dinj, Dsum), and the three induced revision operations (*Haus, *Inj, *Sum). Using our main result, we show that only *Sum satisfies (M1-M3) all together. As a last contribution, we revisit a major criticism of AGM operations, namely that the revisions of (p ∧ q) and (p ∧ (p → q)) are identical. We show that the problem disappears if instead of material implication we use the modal operator of strict implication that can be defined in S5.

We present a computationally grounded semantics for counterfactual conditionals in which i) the state in a model is decomposed into two elements: a propositional valuation and a causal base in propositional form that represents the causal information available at the state; and ii) the comparative similarity relation between states is computed from the states' two components. We show that, by means of our semantics, we can elegantly formalize the notion of actual cause without recurring to the primitive notion of intervention. Furthermore, we provide a succinct formulation of the model checking problem for a language of counterfactual conditionals in our semantics. We show that this problem is PSPACE-complete and provide a reduction of it into QBF that can be used for automatic verification of causal properties.

Conditional logics are usually interpreted in terms of closest world and minimal change. It relies on a measure of distance between worlds which is defined abstractly, i.e. as an element of the model. The typical example of a concrete measure in literature is the Hamming distance. We show that given countably infinite atomic propositions in the language, Hamming distance is not merely an example, but grounded for two arguably most important conditional logics, Lewis' VC and VCU. That means, a formula is satisfied in a VC (resp. VCU) model, if and only if it is satisfied in a VC (resp. VCU) model whose distance between worlds is Hammingian.