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.
This research was supported by UK EPSRC research grant EP/H043748/1.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
MetTeL website, http://www.mettel-prover.org
Aiello, M., van Benthem, J.: A Modal Walk Through Space. Journal of Applied Non-Classical Logics 12, 319–363 (2002)
Aiello, M., Ottens, B.: The Mathematical Morpho-Logical View on Reasoning about Space. In: Veloso, M.M. (ed.) IJCAI 2007, pp. 205–211. AAAI Press (2007)
Andréka, H., Németi, I., van Benthem, J.: Modal Languages and Bounded Fragments of Predicate Logic. Journal of Philosophical Logic 27, 217–274 (1998)
Bénabou, J.: Distributors at Work (2000), http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf
Bloch, I.: Modal Logics Based on Mathematical Morphology for Qualitative Spatial Reasoning. Journal of Applied Non-Classical Logics 12, 399–423 (2002)
Bloch, I., Heijmans, H.J.A.M., Ronse, C.: Mathematical Morphology. In: Aiello, M., Pratt-Hartmann, I., van Benthem, J. (eds.) Handbook of Spatial Logics, pp. 857–944. Springer (2007)
Goré, R., Postniece, L., Tiu, A.: Cut-elimination and Proof Search for Bi-Intuitionistic Tense Logic. arXiv e-Print 1006.4793v2 (2010)
Grädel, E.: On the restraining power of guards. Journal of Symbolic Logic 64, 1719–1742 (1999)
Heijmans, H., Vincent, L.: Graph Morphology in Image Analysis. In: Dougherty, E.R. (ed.) Mathematical Morphology in Image Processing, pp. 171–203. Marcel Dekker (1993)
Rauszer, C.: A formalization of the propositional calculus of H-B logic. Studia Logica 33, 23–34 (1974)
Reyes, G.E., Zolfaghari, H.: Bi-Heyting Algebras, Toposes and Modalities. Journal of Philosophical Logic 25, 25–43 (1996)
Schmidt, R.A., Hustadt, U.: The Axiomatic Translation Principle for Modal Logic. ACM Transactions on Computational Logic 8, 1–55 (2007)
Schmidt, R.A., Tishkovsky, D.: A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 194–209. Springer, Heidelberg (2008)
Schmidt, R.A., Tishkovsky, D.: Automated Synthesis of Tableau Calculi. Logical Methods in Computer Science 7, 1–32 (2011)
Schmidt, R.A., Tishkovsky, D.: Using Tableau to Decide Description Logics with Full Role Negation and Identity. To appear in ACM Transactions on Computational Logic (2013)
Serra, J.: Image Analysis and Mathematical Morphology. Academic Press (1982)
Stell, J.G.: Relations on Hypergraphs. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol. 7560, pp. 326–341. Springer, Heidelberg (2012)
Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: The Tableau Prover Generator MetTeL2. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS, vol. 7519, pp. 492–495. Springer, Heidelberg (2012)
Tishkovsky, D., Schmidt, R.A.: Refinement in the Tableau Synthesis Framework. arXiv e-Print 1305.3131v1 (2013)
Wansing, H.: Constructive negation, implication, and co-implication. Journal of Applied Non-Classical Logics 18, 341–364 (2008)
Zakharyaschev, M., Wolter, F., Chagrov, A.: Advanced Modal Logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 3, pp. 83–266. Kluwer (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Stell, J.G., Schmidt, R.A., Rydeheard, D. (2014). Tableau Development for a Bi-intuitionistic Tense Logic. In: Höfner, P., Jipsen, P., Kahl, W., Müller, M.E. (eds) Relational and Algebraic Methods in Computer Science. RAMICS 2014. Lecture Notes in Computer Science, vol 8428. Springer, Cham. https://doi.org/10.1007/978-3-319-06251-8_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-06251-8_25
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06250-1
Online ISBN: 978-3-319-06251-8
eBook Packages: Computer ScienceComputer Science (R0)