Hostname: page-component-78c5997874-t5tsf Total loading time: 0 Render date: 2024-11-09T13:04:07.843Z Has data issue: false hasContentIssue false
  • English
  • Français

Logical consecutions in discrete linear temporal logic

Published online by Cambridge University Press:  12 March 2014

V. V. Rybakov
V. V. Rybakov*
Affiliation:
Department of Computing and Mathematics, Manchester Metropolitan University, John Dalton Building, Chester Street, Manchester M1 5GD, UK, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We investigate logical consequence in temporal logics in terms of logical consecutions, i.e., inference rules. First, we discuss the question: what does it mean for a logical consecution to be ‘correct’ in a propositional logic. We consider both valid and admissible consecutions in linear temporal logics and discuss the distinction between these two notions. The linear temporal logic LDTL, consisting of all formulas valid in the frame 〈L ≤, ≥〉 of all integer numbers, is the prime object of our investigation. We describe consecutions admissible in LDTL in a semantic way—via consecutions valid in special temporal Kripke/Hintikka models. Then we state that any temporal inference rule has a reduced normal form which is given in terms of uniform formulas of temporal degree 1. Using these facts and enhanced semantic techniques we construct an algorithm, which recognizes consecutions admissible in LDTL. Also, we note that using the same technique it follows that the linear temporal logic L(N) of all natural numbers is also decidable w.r.t. inference rules. So, we prove that both logics LDTL and L(N) are decidable w.r.t. admissible consecutions. In particular, as a consequence, they both are decidable (known fact), and the given deciding algorithms are explicit.

Keywords

temporal logiclinear temporal logiclogical consequenceinferenceinference rulesconsecutionsadmissible rules
Type
Research Article
Information
The Journal of Symbolic Logic , Volume 70 , Issue 4 , December 2005 , pp. 1137 - 1149
Copyright
Copyright © Association for Symbolic Logic 2005

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Bloem, R., Ravi, K., and Somenzi, F., Efficient decision procedures for model checking of linear time logic properties, Conference on Computer Aided Verification (CAV) (Terento, Italy), LNCS, vol. 1633, Springer-Verlag, 1999.Google Scholar
[2]Chagrov, A. and Zakharyaschev, M., Modal logic, Oxford Logic Guides, vol. 35, Clarendon Press, Oxford, 1997.CrossRefGoogle Scholar
[3]Citkin, A. I., On admissible rules of intuitionistic propositional logic, Math. USSR Sbornik, vol. 31 (1977), no. 2, pp. 279–288.CrossRefGoogle Scholar
[4]Clarke, E., Grumberg, O., and Hamaguchi, K. P., Another look at LTL model checking, Conference on Computer Aided Verification (CAV) (Stanford, California), LNCS, vol. 818, Springer-Verlag, 1994.Google Scholar
[5]Curry, H. B., Foundations of mathematical logic, Dover Publications, New-York, 1977.Google Scholar
[6]Friedman, H., One hundred and two problems in mathematical logic, this Journal, vol. 40 (1975), no. 3, pp. 113–130.Google Scholar
[7]Gabbay, D., Model theory for tense logics, U.S. Air Forse Office of Science Research, contract no. F61052-68-C-0036, report no. 1, 04 1969.Google Scholar
[8]Gabbay, D., Kurucz, A., Wolter, F., and Zakharyaschev, M., Many-dimensional modal logics: Theory and applications, Elsevier Science Pub Co., 2003.Google Scholar
[9]Ghilardi, S., Unification in intuitionistic logic, this Journal, vol. 64 (1999), no. 2, pp. 859–880.Google Scholar
[10]Goldblatt, R., Logics of time and computation, second ed., CSLI Lecture Notes, vol. 7, 1992.Google Scholar
[11]Harrop, R., Concerning formulas of the types A → B ∨ C, A ∨ ∃xB(x) in intuitionistic formal system, this Journal, vol. 25 (1960), pp. 27–32.Google Scholar
[12]Iemhoff, R., A(nother) characterization of intuitionistic propositional logic, Annals of Pure and Applied Logic, vol. 113 (2001), no. 1-3, pp. 161–173.CrossRefGoogle Scholar
[13]Iemhoff, R., On the admissible rules of intuitionistic propositional logic, this Journal, vol. 66 (2001), pp. 281–294.Google Scholar
[14]Lorenzen, P., Einführung in die operative Logik und Mathematik, Springer-Verlag, 1955.CrossRefGoogle Scholar
[15]Marx, M. and Venema, Y., Multi-dimensional modal logics, Kluwer Academic Publishers, 1997.CrossRefGoogle Scholar
[16]Mints, G. E., Derivability of admissible rules, Journal of Soviet Mathematics, vol. 6 (1976), no. 4, pp. 417–421.CrossRefGoogle Scholar
[17]Pnueli, A., The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, IEEE, 1997, pp. 46–57.Google Scholar
[18]Prior, A., Time and modaliy, Oxford, 1957.Google Scholar
[19]Prior, A., Past, present and future, Oxford, 1967.CrossRefGoogle Scholar
[20]Rybakov, V. V., A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic, Algebra and Logic, vol. 23 (1984), no. 5, pp. 369–384, English Translation.CrossRefGoogle Scholar
[21]Rybakov, V. V., The bases for admissible rules of logics 54 and Int, Algebra and Logic, vol. 24 (1985), pp. 55–68, English translation.CrossRefGoogle Scholar
[22]Rybakov, V. V., Rules of inference with parameters for intuitionistic logic, this Journal, vol. 57 (1992), no. 3, pp. 912–923.Google Scholar
[23]Rybakov, V. V., Heriditarily structurally complete modal logics, this Journal, vol. 60 (1995), no. 1, pp. 266–288.Google Scholar
[24]Rybakov, V. V., Admissible logical inference rules, Studies in Logic and the Foundations of Mathematics, vol. 136, North-Holland, 1997.Google Scholar
[25]Rybakov, V. V., Construction of an explicit basis for rules admissible in modal system S4, Mathematical Logic Quarterly, vol. 47 (2001), no. 4, pp. 441–451.3.0.CO;2-J>CrossRefGoogle Scholar
[26]Rybakov, V. V., Refined common knowledge logics or logics of common information, Archive for Mathematical Logic, vol. 42 (2003), pp. 179–200.CrossRefGoogle Scholar
[27]Rybakov, V. V., Kiyatkin, V. R., and Oner, T., On finite model property for admissible rules, Mathematical Logic Quarterly, vol. 45 (1999), no. 4, pp. 505–520.CrossRefGoogle Scholar
[28]Rybakov, V. V., Terziler, M., and Rimazki, V. V., Basis in semi-reduced form for the admissible rules of the intuitionistic logic IPC, Mathematical Logic Quarterly, vol. 46 (2000), no. 2, pp. 207–218.3.0.CO;2-E>CrossRefGoogle Scholar
[29]Segerberg, K., Modal logics with linear alternative relations, Theoria, vol. 36 (1970), pp. 301–322.CrossRefGoogle Scholar
[30]Thomason, S. K., Semantic analysis of tense logic, this Journal, vol. 37 (1972), no. 1.Google Scholar
[31]van Benthem, J., The logic of time, Synthese Library, vol. 156, Reidel, 1983.CrossRefGoogle Scholar