@INPROCEEDINGS{StellSchmidtRydeheard14a,
AUTHOR = {Stell, J. G. and Schmidt, R. A. and Rydeheard, D.},
YEAR = {2014},
TITLE = {Tableau Development for a Bi-Intuitionistic Tense Logic},
EDITOR = {Jipsen, P. and Kahl, W.},
BOOKTITLE = {Relational and Algebraic Methods in Computer Science (RAMiCS 14)},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {8428},
PUBLISHER = {Springer},
PAGES = {412--428},
DOI = {10.1007/978-3-319-06251-8_25},
URL = {http://www.cs.man.ac.uk/~schmidt/publications/StellSchmidtRydeheard14a.html},
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.
},
}