×

zbMATH — the first resource for mathematics

Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition. (English) Zbl 1209.03011
Summary: The paper develops a technique for computing inference rules admissible in temporal logic \(\text{T}_{\text{S}4}\). The problem whether there exists an algorithm recognizing inference rules admissible in \(\text{T}_{\text{S}4}\) is a long-standing open problem. The logic \(\text{T}_{\text{S}4}\) has neither the extension property nor the co-cover property which previously were central instruments for constructing decision algorithms for admissibility in modal logics (e.g., reflexive and transitive modal logic \(\text{S}4\)). Our paper uses a linear-compression property, a zigzag-ray property and a zigzag stretching property which hold for \(\text{T}_{\text{S}4}\). The main result of the paper is a sufficient condition for admissibility of inference rules in \(\text{T}_{\text{S}4}\). It is shown that all rules which are valid in special finite models (with an effective upper bound on size) must be admissible in \(\text{T}_{\text{S}4}\).

MSC:
03B44 Temporal logic
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Areces, G.; Blackburn, P.; Marx, M., The computational complexity of hybrid temporal logics, Logic journal of IGPL, 8, 653-679, (2000) · Zbl 0959.03011
[2] Barringer, H.; Fisher, M.; Gabbay, D.; Gough, G., ()
[3] Bloem, R.; Ravi, K.; Somenzi, F., Efficient decision procedures for model checking of linear time logic properties, () · Zbl 1046.68579
[4] Bull, R.A., An algebraic study of tense logics with linear time, The journal of symbolic logic, 33, 27-38, (1968) · Zbl 0155.01403
[5] Bull, R.A., Note on a paper in tense logic, The journal of symbolic logic, 34, 215-218, (1969) · Zbl 0179.31307
[6] Fritz, Carsten, Constructing Büchi automaton from linear temporal logic using simulation relations for alternating Büchi automata, (), 35-48 · Zbl 1279.68152
[7] M. Daniele, F. Giunchiglia, M. Vardi, Improved automata generation for linear temporal logic, in: book: CAV’99, International Conference on Computer-Aided Verification, Trento, Italy, 1999. · Zbl 1046.68588
[8] Friedman, H., One hundred and two problems in mathematical logic, Journal of symbolic logic, 40, 3, 113-130, (1975) · Zbl 0318.02002
[9] Gabbay, D., The declarative past and imperative future: executable temporal logic for interactive systems, (), 409-448
[10] Gabbay, D.M.; Hodkinson, I.M.; Reynolds, M.A., ()
[11] Gabbay, D.M.; Hodkinson, I.M., An axiomatisation of the temporal logic with until and Since over the real numbers, Journal of logic and computation, 1, 229-260, (1990) · Zbl 0744.03018
[12] Ghilardi, S., Unification in intuitionistic logic, Journal of symbolic logic, 64, 2, 859-880, (1999) · Zbl 0930.03009
[13] Ghilardi, S., Best solving modal equations, Annals of pure and applied logic, 102, 183-198, (2000) · Zbl 0949.03010
[14] Ghilardi, S.; Sacchetti, L., Filtering unification and most general unifiers in modal logic, Journal of symbolic logic, 69, 3, 879-906, (2004) · Zbl 1069.03011
[15] Goldblatt, R., Logics of time and computation, () · Zbl 0635.03024
[16] Goldblatt, R., Mathematical modal logic: a view of its evolution, Journal of applied logic, 1, 5-6, 309-392, (2003) · Zbl 1041.03015
[17] Harrop, R., Concerning formulas of the types \(A \rightarrow B \vee C\), \(A \rightarrow \exists x B(x)\) in intuitionistic formal system, Journal of symbolic logic, 25, 27-32, (1960) · Zbl 0098.24201
[18] Iemhoff, R., On the admissible rules of intuitionistic propositional logic, Journal of symbolic logic, 66, 281-294, (2001) · Zbl 0986.03013
[19] Iemhoff; Metcalfe, G., Proof theory for admissible rules, Annals of pure and applied logic, 159, 1-2, 171-186, (2009) · Zbl 1174.03024
[20] Jerábek, E., Admissible rules of modal logics, Journal of logic computation, 15, 411-431, (2005) · Zbl 1077.03011
[21] Jerábek, E., Complexity of admissible rules, Archive for mathematical logic, 46, 2, 73-92, (2007) · Zbl 1115.03010
[22] F. Laroussinie, N. Markey, Ph. Schnoebelen, Temporal logic with forgettable past, in: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS’02, Copenhagen, Denmark, 2002, pp. 383-392.
[23] Lichtenstein, O.; Pnueli, A., Propositional temporal logics: decidability and completeness, Logic journal of the IGPL, 8, 1, 55-85, (2000) · Zbl 1033.03009
[24] Litak, T.; Wolter, F., All finitely axiomatizable tense logics of linear time flows are conp-complete, Studia logica, 81, 2, 153-165, (2005) · Zbl 1096.03014
[25] Lorenzen, P., Einführung in die operative logik und Mathematik, (1955), Springer-Verlag Berlin-Göttingen, Heidelberg · Zbl 0066.24802
[26] Manna, Z.; Pnueli, A., The temporal logic of reactive and concurrent systems: specification, (1992), Springer-Verlag
[27] Manna, Z.; Sipma, H., Alternating the temporal picture for safety, (), 429-450 · Zbl 0973.68141
[28] Mints, G.E., Derivability of admissible rules, Journal of soviet mathematics, 6, 4, 417-421, (1976) · Zbl 0375.02014
[29] Pnueli, A., The temporal logic of programs, (), 46-57
[30] Roziere, P., Admissible and derivable rules, (), 129-136 · Zbl 0797.03001
[31] Rybakov, V.V., A criterion for admissibility of rules in the modal system \(S 4\) and the intuitionistic logic, Algebra and logic, 23, 5, 369-384, (1984), (English Translation) · Zbl 0598.03013
[32] Rybakov, V.V., The bases for admissible rules of logics S4 and int., Algebra and logic, 24, 55-68, (1985), (English translation) · Zbl 0598.03014
[33] Rybakov, V.V., Equations in free Topoboolean algebra, Algebra and logic, 25, 2, 172-204, (1986), (in Russian) · Zbl 0624.03007
[34] Rybakov, V.V., Logical equations and admissible rules with parameters in modal logics of provability, Studia logica, XLIX, 2, 215-239, (1990) · Zbl 0729.03012
[35] Rybakov, V.V., Rules of inference with parameters for intuitionistic logic, Journal of symbolic logic, 57, 3, 912-923, (1992) · Zbl 0788.03007
[36] Rybakov, V.V., Admissible logical inference rules, () · Zbl 0729.03012
[37] Rybakov, V.V.; Kiyatkin, V.R.; Oner, T., On finite model property for admissible rules, Mathematical logic quarterly, 45, 4, 505-520, (1999) · Zbl 0938.03033
[38] Rybakov, V.V., Construction of an explicit basis for rules admissible in modal system \(S 4\), Mathematical logic quarterly, 47, 4, 441-451, (2001) · Zbl 0992.03027
[39] Rybakov, V.V., Logical consecutions in discrete linear temporal logic, Journal of symbolic logic, 70, 4, 1137-1149, (2005) · Zbl 1110.03010
[40] Rybakov, V.V., Logical consecutions in intransitive temporal linear logic of finite intervals, Journal of logic computation, 15, 5, 633-657, (2005) · Zbl 1091.03002
[41] Rybakov, V.V., Linear temporal logic with until and before on integer numbers, deciding algorithms, (), 322-334 · Zbl 1185.03022
[42] Rybakov, V., Until-Since temporal logic based on parallel time with common past. deciding algorithms, (), 486-497 · Zbl 1132.03324
[43] Rybakov, V., Logics with universal modality and admissible consecutions, Journal of applied non-classical logics, 17, 3, 381-394, (2007) · Zbl 1186.03048
[44] Rybakov, V., Branching time logics \(B T L_{N, N^{- 1}}^{U, S}\) with operations until and Since based on bundles of integer numbers, logical consecutons, deciding algorithms, (), 254-271 · Zbl 1148.03011
[45] Rybakov, V., Multi-modal and temporal logics with universal formula—reduction of admissibility to validity and unification, Journal of logic computation, 18, 4, 509-519, (2008) · Zbl 1149.03017
[46] Rybakov, V., Linear temporal logic with until and next, logical consecutions, Annals of pure and applied logic, 155, 1, 32-45, (2008) · Zbl 1147.03008
[47] Sistla, A.P.; Clarke, E.M., The complexity of propositional linear temporal logic, Journal of the ACM, 32, 3, 733-749, (1985) · Zbl 0632.68034
[48] van Benthem, J., ()
[49] M. Vardi, An automata-theoretic approach to linear temporal logic, in: Proceedings of the Banff Workshop on Knowledge Acquisition, Banff’94, 1994.
[50] Vardi, M., Reasoning about the past with two-way automata, (), 628-641 · Zbl 0909.03019
[51] Wolter, F.; Zakharyaschev, M., Undecidability of the unification and admissibility problems for modal and description logics, ACM transactions of computational logic (TOCL), 9, 4, 25:1-25.20, (2008) · Zbl 1367.03026
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.