A bi-intuitionistic modal logic: foundations and automation (Q299186)

In the paper, a bi-intuitionistic logic BISKT with modal tense operators is constructed. This logic finds its foundations in a general algebraic framework of pre-orders and relations on downward-closed sets as well as on graphs. Then, BISKT can be defined as a bi-intuitionistic stable tense logic with a semantics in which formulas are interpreted as downward-closed sets, including subgraphs as a special case. The language of BISKT includes two adjoint pairs of modal tense operators: \(\square\), \(\blacklozenge\), \(\lozenge\), \(\blacksquare\). These operators obtain their interpretation on subgraphs by taking the nodes to be time points, the edges to be open intervals, and \(R\) to relate each open interval to all instants that either end the interval or end some later interval. As the authors explain, the times when, e.g., \(\lozenge p\) holds are then the open intervals for which \(p\) holds at some later instant, together with both endpoints of those intervals, and the times when \(\blacksquare q\) holds are all the closed intervals where \(q\) holds at all times and has always held. Remarkably, an alternative semantics for BISKT can be obtained by its embedding into the traditional propositional tense logic \(Kt(H,R)\) defined over two accessibility relations \(H\) and \(R\) and their converse relations. Since it is well-known that \(Kt(H,R)\) is decidable and has the effective finite model property, it follows that BISKT has the effective finite model property and is decidable as well. Moreover, it can be shown that satisfiability in BISKT is PSPACE-complete. The paper also presents a terminating labeled tableau calculus for BISKT, which is shown to be sound and complete.