Abstract
As a remedy for the bad computational behaviour of first-order temporal logic (FOTL), it has recently been proposed to restrict the application of temporal operators to formulas with at most one free variable thereby obtaining so-called monodic fragments of FOTL. In this paper, we are concerned with constructing tableau algorithms for monodic fragments based on decidable fragments of first-order logic like the two-variable fragment or the guarded fragment. We present a general framework that shows how existing decision procedures for first-order fragments can be used for constructing a tableau algorithm for the corresponding monodic fragment of FOTL. Some example instantiations of the framework are presented.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Degtyarev, A., and M. Fisher, 'Towards first-order temporal resolution', in F. Baader, G. Brewka, and T. Eiter, (eds.), Advances in Artificial Intelligence (KI'2001), volume 2174 of LNAI, pp. 18–32, Springer-Verlag, 2001.
Degtyarev, A., M. Fisher, and A. Lisitsa, 'Equality and monodic first-order temporal logic', Studia Logica, 72(2):147–156, 2002.
Degtyarev, A., M. Fisher, and B. Konev, 'Monodic temporal resolution', Submitted, 2003. Available as Technical report ULCS-03-001 from http://www.csc.liv.ac.uk/research/techreports.
Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Reidel, Dordrecht, 1983.
Fitting, M., and R. Mendelson First-Order Modal Logic, Kluwer Academic Publishers, Dordrecht, 1998.
Gabbay, D., I. Hodkinson, and M. Reynolds, Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 1, Oxford University Press, 1994.
Gabbay, D., A. Kurucz, F. Wolter, and M. Zakharyaschev, Many-Dimensional Modal Logics: Theory and Applications, Elsevier, 2003.
Goranko, V., and S. Passy., 'Using the universal modality: Gains and questions', Journal of Logic and Computation, 2:5–30, 1992.
GorÉ, R., 'Tableau algorithms for modal and temporal logic', in D'Agostino et al., (eds.), Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht, 1999.
Hodkinson, I., 'Monodic packed fragment with equality is decidable', Studia Logica, 72(2):185–197, 2002.
Hodkinson, I., F. Wolter, and M. Zakharyaschev, 'Decidable fragments of first-order temporal logics', Annals of Pure and Applied Logic, 106:85–134, 2000.
Hodkinson, I., F. Wolter, and M. Zakharyaschev, 'Monodic fragments of firstorder temporal logics: 2000-2001 A.D.', in Logic for Programming, Artificial Intelligence and Reasoning, volume 2250 of LNAI, pp. 1–23, Springer-Verlag, 2001.
Hughes, G. E., and M. J. Cresswell, A New Introduction to Modal Logic, Methuen, London, 1996.
Kripke, S.A., 'Semantical considerations on modal logic', Acta Philosophica Fennica, 16:83–94, 1963.
Lutz, C., H. Sturm, F. Wolter, and M. Zakharyaschev, 'Tableaux for temporal description logic with constant domain', in R. GorÉ, A. Leitsch, and T. Nipkow, (eds.), Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR'01), volume 2083 of LNAI, pp. 121–136. Springer-Verlag, 2001.
Lutz, C., H. Sturm, F. Wolter, and M. Zakharyaschev, 'A tableau decision algorithm for modalized A L C with constant domains', Studia Logica, 72(2):199–232, 2002.
Schild, K., 'Combining terminological logics with tense logic', in Miguel Filgueiras and Luís Damas, (eds.), Progress in Artificial Intelligence - 6th Portuguese Conference on Artificial Intelligence, EPIA'93, volume 727 of LNAI, pp. 105–120. Springer-Verlag, 1993.
Sturm, H., and F. Wolter, 'A tableau calculus for temporal description logic: The expanding domain case', Journal of Logic and Computation, 2002.
Wajsberg, M., 'Ein erweiterter Klassenkalkül', Monatsh Math. Phys., 40:113–126, 1933
Wolper, P., 'The tableau method for temporal logic: An overview', Logique et Analyse, 28:119–152, 1985.
Wolter, F., and M. Zakharyaschev, 'Satisfiability problem in description logics with modal operators', in A. Cohn, L. Schubert, and S. Shapiro, (eds.), KR'98: Principles of Knowledge Representation and Reasoning, pp. 512–523. Morgan Kaufmann Publishers, 1998.
Wolter, F., and M. Zakharyaschev, 'Multi-dimensional description logics', in D. Thomas, (ed.), Proceedings of the 16th International Joint Conference on Artificial Intelligence (IJCAI-99), pp. 104–109. Morgan Kaufmann Publishers, 1999.
Wolter, F., and M. Zakharyaschev, 'Dynamic description logic', in K. Segerberg, M. de Rijke, H. Wansing, and M. Zakharyaschev, (eds.), Advances in Modal Logic, Volume 2, pp. 431–445. CSLI Publications, 2000.
Wolter, F., and M. Zakharyaschev, 'Temporalizing description logics', in D. Gabbay and M. de Rijke, (eds.), Frontiers of Combining Systems II, pp. 379–401. Studies Press/Wiley, 2000.
Wolter, F., and M. Zakharyaschev, 'Decidable fragments of first-order modal logics', Journal of Symbolic Logic, 66:1415–1438, 2001.
Wolter, F., and M. Zakharyaschev, 'Axiomatizing the monodic fragment of firstorder temporal logic', Annals of Pure and Applied Logic, 118(1-2):133–145, 2002.
Wolter, F., and M. Zakharyaschev, 'Qualitative spatio-temporal representation and reasoning: a computational perspective,’ in Exploring Artificial Intelligence in the New Millenium, pp. 175-215, Morgan Kaufmann Publishers, 2002.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Kontchakov, R., Lutz, C., Wolter, F. et al. Temporalising Tableaux. Studia Logica 76, 91–134 (2004). https://doi.org/10.1023/B:STUD.0000027468.28935.6d
Issue Date:
DOI: https://doi.org/10.1023/B:STUD.0000027468.28935.6d