TY - JOUR
T1 - A Bi-Intuitionistic Modal Logic: Foundations and Automation
AU - Stell, J G
AU - Schmidt, Renate
AU - Rydeheard, David
N1 - This research was supported by UK EPSRC research grant EP/H043748/1.
PY - 2016/6
Y1 - 2016/6
N2 - 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.
AB - 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.
U2 - 10.1016/j.jlamp.2015.11.003
DO - 10.1016/j.jlamp.2015.11.003
M3 - Article
SN - 2352-2216
VL - 85
SP - 500
EP - 519
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
IS - 4
ER -