×

zbMATH — the first resource for mathematics

Logical consecutions in discrete linear temporal logic. (English) Zbl 1110.03010
In this paper the author investigates the notion of logical consequence in temporal logic in terms of inference rules. The study of logical inference is usually based upon the choice of a particular set of axioms and inference rules (axiomatic system), since this notion is not an invariant. Nevertheless, there is a way to define an invariant notion of logical inference, called “admissible rules” or “consecutions”. Such rules are defined by the set of theorems of a given logic (where a logic is conceived as the set of all formulas valid in specified models) using the notion of uniform substitution. Admissible rules have been investigated for several modal and superintuitionistic logics (see, for example, [G. E. Mints, “Derivability of admissible rules.” J. Sov. Math. 6, 417–421 (1976); translation from Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 32, 85–89 (1973; Zbl 0358.02031)], [V. V. Rybakov, “A criterion for admissibility of rules in the modal system S4 and intuitionistic logic” Algebra Logic 23, 369–384 (1984); translation from Algebra Logika 23, No. 5, 546–572 (1984; Zbl 0598.03013)], [S. Ghilardi, “Unification in intuitionistic logic”, J. Symb. Log. 64, No. 2, 859–880 (1999; Zbl 0930.03009)]).
In the present paper, linear temporal logic, LDTL, is studied. LDTL can be conceived as all the formulas valid in the frame \((\mathbb Z, \leq, \geq)\) of all integer numbers. An algorithm is constructed that recognizes consecutions admissible in LDTL. Further, the same technique is applied to the linear temporal logic \(\mathcal L(\mathbb N)\) of all natural numbers. So, both logics LDTL and \(\mathcal L(\mathbb N)\) are decidable w.r.t. admissible rules.

MSC:
03B44 Temporal logic
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] DOI: 10.1007/BF01978706 · Zbl 0598.03014 · doi:10.1007/BF01978706
[2] Heriditarily structurally complete modal logics 60 pp 266– (1995)
[3] Unification in intuitionistic logic 64 pp 859– (1999) · Zbl 0930.03009
[4] Many-dimensional modal logics: Theory and applications (2003) · Zbl 1051.03001
[5] One hundred and two problems in mathematical logic 40 pp 113– (1975)
[6] Foundations of mathematical logic (1977) · Zbl 0396.03001
[7] Conference on Computer Aided Verification (CAV) 818 (1994)
[8] DOI: 10.1070/SM1977v031n02ABEH002303 · Zbl 0386.03011 · doi:10.1070/SM1977v031n02ABEH002303
[9] Modal logic 35 (1997) · Zbl 0871.03007
[10] Conference on Computer Aided Verification (CAV) 1633 (1999)
[11] Rules of inference with parameters for intuitionistic logic 57 pp 912– (1992)
[12] The logic of time 156 (1983)
[13] Semantic analysis of tense logic 37 (1972)
[14] Past, present and future (1967) · Zbl 0169.29802
[15] Time and modaliy (1957)
[16] Proceedings of the 18th Annual Symposium on Foundations of Computer Science pp 46– (1997)
[17] DOI: 10.1007/BF01084082 · Zbl 0375.02014 · doi:10.1007/BF01084082
[18] Multi-dimensional modal logics (1997)
[19] Einführung in die operative Logik und Mathematik (1955) · Zbl 0066.24802
[20] On the admissible rules of intuitionistic propositional logic 66 pp 281– (2001)
[21] DOI: 10.1016/S0168-0072(01)00056-2 · Zbl 0988.03045 · doi:10.1016/S0168-0072(01)00056-2
[22] Concerning formulas of the types A B C, A xB(x) in intuitionistic formal system 25 pp 27– (1960)
[23] Logics of time and computation 7 (1992)
[24] Theoria 36 pp 301– (1970)
[25] DOI: 10.1002/(SICI)1521-3870(200005)46:2&lt;207::AID-MALQ207&gt;3.0.CO;2-E · Zbl 0955.03037 · doi:10.1002/(SICI)1521-3870(200005)46:2<207::AID-MALQ207>3.0.CO;2-E
[26] DOI: 10.1002/malq.19990450409 · Zbl 0938.03033 · doi:10.1002/malq.19990450409
[27] DOI: 10.1007/s001530100134 · Zbl 1030.03015 · doi:10.1007/s001530100134
[28] DOI: 10.1002/1521-3870(200111)47:4&lt;441::AID-MALQ441&gt;3.0.CO;2-J · Zbl 0992.03027 · doi:10.1002/1521-3870(200111)47:4<441::AID-MALQ441>3.0.CO;2-J
[29] Admissible logical inference rules 136 (1997)
[30] DOI: 10.1007/BF01982031 · Zbl 0598.03013 · doi:10.1007/BF01982031
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.