Actuality, tableaux, and two-dimensional modal logics
The paper's goal is to provide sound and complete tableau systems for a range of first-order modal logics, of suitable syntactic expressivity, that are two-dimensional in the sense that they are equipped with a Kripke semantics in which valuations are parametrized by pairs of possible worlds, one of which is the world in which the formula is being assessed while the other is a world that is treated as actual.
scientific article; zbMATH DE number 6960408
scientific article