@ARTICLE{StellSchmidtRydeheard16,
AUTHOR = {Stell, J. G. and Schmidt, R. A. and Rydeheard, D.},
YEAR = {2016},
TITLE = {A Bi-Intuitionistic Modal Logic: Foundations and Automation},
JOURNAL = {Journal of Logical and Algebraic Methods in Programming},
VOLUME = {85},
NUMBER = {4},
PAGES = {500--519},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/StellSchmidtRydeheard16.html},
DOI = {http://dx.doi.org/10.1016/j.jlamp.2015.11.003},
ABSTRACT = {The paper introduces a bi-intuitionistic modal logic, called BISKT, with two adjoint pairs of tense operators.
The semantics of BISKT is defined using 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.
We present a comprehensive study of the logic, giving decidability,
complexity and correspondence results.
We also show the logic has the effective finite model property.
We present a sound, complete and terminating tableau calculus for the
logic and use the MetTeL system to explore implementations of
different versions of the calculus.
An experimental evaluation gave good results for satisfiable problems
using predecessor blocking.
}
}