Article ID Journal Published Year Pages File Type
10333720 Journal of Logical and Algebraic Methods in Programming 2016 20 Pages PDF
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.
Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, , ,