Discrete linear temporal logic with current time point clusters, deciding algorithms
DOI:
https://doi.org/10.12775/LLP.2008.009Keywords
temporal logics, linear temporal logics, algorithms, Kripke structures, multi-modal logics, decidability, admissible inference rulesAbstract
The paper studies the logic TL(N\Box+-wC) – logic of discrete linear time with current time point clusters. Its language uses modalities \Diamond+ (possible in future) and \Diamond- (possible in past) and special temporal operations, – \Box+w (weakly necessary in future) and \Box-w (weakly necessary in past). We proceed by developing an algorithm recognizing theorems of TL(N\Box+-wC), so we prove that TL(N\Box+-wC) is decidable. The algorithm is based on reduction of formulas to inference rules and converting the rules in special reduced normal form, and, then, on checking validity of such rules in models of singleexponential size in the rules. Also we consider the admissibility problem for TL(N\Box+-wC) and show how to reduce the problem for admissibility to the decidability of TL(N\Box+-wC) itself using definable universal modalities.References
Areces G., P. Blackburn, and M. Marx, “The computational complexity of hybrid temporal logics”, Logic Journal of IGPL 8 (2000), 653–679.
Bull, R.A., “An algebraic study of tense logics with linear time”, The Journal of Symbolic Logic 33 (1968), 27–38.
Bull, R.A., “Note on a paper in tense logic”, The Journal of Symbolic Logic 34 (1969), 215–218.
Chagrov, A., “A decidable logic with undecidable admissibility problem for inference rulres”, Algebra and Logic 31 (1992), 53–55.
Gabbay, D.M., I.M. Hodkinson, and M.A. Reynolds, “Temporal logic”, Mathematical Foundations and Computational Aspects, vol. 1, Clarendon Press, Oxford, 1994.
Gabbay, D.M., and I.M. Hodkinson, “An axiomatisation of the temporal logic with Until and Since over the real numbers”, Journal of Logic and Computation 1 (1990), 229–260.
Ghilardi, S., “Unification in intuitionistic logic”, Journal of Symbolic Logic 64, 2 (1999), 859–880.
Ghilardi, S., “Best solving modal equations”, Annals of Pure and Applied Logic 102 (2000), 183–198.
V. Rybakov [9] Ghilardi, S., and L. Sacchetti, “Filtering unification and most general unifiers in modal logic”, Journal of Symbolic Logic 69, 3 (2004), 879–906.
Goldblatt, R., “Logics of time and computation”, CSLI Lecture Notes, no. 7, 1992.
Goldblatt, R., “Mathematical modal logic: A view of its evolution”, J. Applied Logic 1, 5–6 (2003), 309–392.
Golovanov, M.I., A.V. Kosheleva, and V.V. Rybakov, “Logic of visibility, perception, and knowledge and admissible inference rules”, Logic Journal of the IGPL 13, 2 (2005), 201–209.
Goranko, V., and S. Passy, “Using the universal modality, Gains and questions”, Journal of Logic Computation 2, 1 (1992), 5–30.
Harrop, R., “Concerning formulas of the types A › B ? C, A › ?xB(x) in intuitionistic formal system”, J. of Symbolic Logic 25 (1960), 27–32.
Iemhoff, R., “On the admissible rules of intuitionistic propositional logic”, J. of Symbolic Logic 66 (2001), 281–294.
Jerábek, E., “Admissible rules of modal logics”, J. of Logic Computation 15 (2005), 411–431.
Kapron, B.M., “Modal sequents and definability”, J. of Symbolic Logic 52 (1987), 3, 756–765.
Hintikka, J., and F. Vandamme, Logic of Discovery and Logic of Discourse, Springer, 1986.
Litak, T., and F. Wolter, “All finitely axiomatizable tense logics of linear time flows are coNP-complete”, Studia Logica 81, 2 (2005), 153–165.
Lorenzen, P., Einführung in die operative Logik und Mathematik, Berlin–Göttingen, Heidelberg, Springer-Verlag, 1955.
Mints, G.E., “Derivability of admissible rules”, J. of Soviet Mathematics 6, 4 (1976), 417–421.
Roziere, P., “Admissible and derivable rules”, Math. Structures in Computer Science 3 (1993), 129–136.
Rybakov, V.V., “A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic”, Algebra and Logic 23, 5 (1984), 369–384 (Engl. Translation).
Rybakov, V.V., Admissible Logical Inference Rules, series “Studies in Logic and the Foundations of Mathematics”, vol. 136, Elsevier Sci. Publ., North-Holland, 1997.
Rybakov, V.V., “Construction of an explicit basis for rules admissible in modal system S4”, Mathematical Logic Quarterly 47, 4 (2001), 441–451.
Rybakov, V.V., “Logical consecutions in tntransitive temporal linear logic of finite intervals”, Journal of Logic Computation 15, 5 (2005), 633–657.
Rybakov, V.V., “Logical consecutions in discrete linear temporal logic”, Journal of Symbolic Logic 70, 4 (2005), 1137–1149.
Rybakov, V.V., “Linear temporal logic with Until and Before on integer numbers, deciding algorithms”, pp. 322–334 in Computer Science – Theory and Applications, Lecture Notes in Computer Science, Springer, vol. 3967, 2006.
Rybakov, V.V., “Branching time logic TL(NBox+-wC)alpha with operations Until and Since based on bundles of integer numbers”, Logical Consecutions, Deciding Algorithms, 2006 (submitted).
Segerberg, K., “Modal logics with linear alternative relations”, Theoria 36 (1970), 301–322.
van Benthem, J., The Logic of Time, Reidel, Dordrecht, Synthese Library, vol. 156, 1983.
van Benthem, J., and J.A. Bergstra, “Logic of transition systems”, Journal of Logic, Language and Information 3, 4 (1994), 247–283.
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 172
Number of citations: 0
