Tableau development for a bi-intuitionistic tense logic

Abstract

The paper introduces a bi-intuitionistic logic with two modal operators and their tense versions. The semantics is defined by Kripke models in which the set of worlds carries a pre-order relation as well as an accessibility relation, and the two relations are linked by a stability condition. A special case of these models arises from graphs in which the worlds are interpreted as nodes and edges of graphs, and formulae represent subgraphs. The pre-order is the incidence structure of the graphs. These examples provide an account of time including both time points and intervals, with the accessibility relation providing the order on the time structure. The logic we present is decidable and has the effective finite model property. We present a tableau calculus for the logic which is sound, complete and terminating. The MetTel system has been used to generate a prover from this tableau calculus. © 2014 Springer International Publishing.