Tableau development for a bi-intuitionistic tense logic

John G. Stell; Renate A. Schmidt; David Rydeheard

doi:10.1007/978-3-319-06251-8_25

Tableau development for a bi-intuitionistic tense logic

John G. Stell, Renate A. Schmidt, David Rydeheard

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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. © 2014 Springer International Publishing.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Publisher	Springer Nature
Pages	412-428
Number of pages	16
Volume	8428
ISBN (Print)	9783319062501
DOIs	https://doi.org/10.1007/978-3-319-06251-8_25
Publication status	Published - 2014
Event	14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014 - Marienstatt Duration: 1 Jul 2014 → … http://dx.doi.org/10.1007/978-3-319-06251-8_25

Conference

Conference	14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014
City	Marienstatt
Period	1/07/14 → …
Internet address	http://dx.doi.org/10.1007/978-3-319-06251-8_25

Access to Document

10.1007/978-3-319-06251-8_25

Cite this

@inproceedings{cd7d78e24bda45fabe25bcd68cf0b354,

title = "Tableau development for a bi-intuitionistic tense logic",

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. {\textcopyright} 2014 Springer International Publishing.",

author = "Stell, {John G.} and Schmidt, {Renate A.} and David Rydeheard",

year = "2014",

doi = "10.1007/978-3-319-06251-8_25",

language = "English",

isbn = "9783319062501",

volume = "8428",

pages = "412--428",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

publisher = "Springer Nature",

address = "United States",

note = "14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014 ; Conference date: 01-07-2014",

url = "http://dx.doi.org/10.1007/978-3-319-06251-8_25",

}

Stell, JG, Schmidt, RA & Rydeheard, D 2014, Tableau development for a bi-intuitionistic tense logic. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 8428, Springer Nature, pp. 412-428, 14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014, Marienstatt, 1/07/14. https://doi.org/10.1007/978-3-319-06251-8_25

Tableau development for a bi-intuitionistic tense logic. / Stell, John G.; Schmidt, Renate A.; Rydeheard, David.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 8428 Springer Nature, 2014. p. 412-428.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Tableau development for a bi-intuitionistic tense logic

AU - Stell, John G.

AU - Schmidt, Renate A.

AU - Rydeheard, David

PY - 2014

Y1 - 2014

N2 - 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. © 2014 Springer International Publishing.

AB - 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. © 2014 Springer International Publishing.

U2 - 10.1007/978-3-319-06251-8_25

DO - 10.1007/978-3-319-06251-8_25

M3 - Conference contribution

SN - 9783319062501

VL - 8428

SP - 412

EP - 428

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

T2 - 14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014

Y2 - 1 July 2014

ER -

Tableau development for a bi-intuitionistic tense logic

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this