{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T20:54:04Z","timestamp":1684529644114},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2007,10,6]],"date-time":"2007-10-06T00:00:00Z","timestamp":1191628800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2008,8]]},"DOI":"10.1007\/s00224-007-9059-9","type":"journal-article","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T15:21:49Z","timestamp":1191597709000},"page":"254-271","source":"Crossref","is-referenced-by-count":4,"title":["Branching Time Logics $\\mathcal {BTL}^{\\mathrm {U,S}}_{\\mathrm {N},\\mathrm {N}^{-1}}(\\mathcal {Z})_{\\alpha }$ with Operations Until and Since Based on Bundles of Integer Numbers, Logical Consecutions, Deciding Algorithms"],"prefix":"10.1007","volume":"43","author":[{"given":"V.","family":"Rybakov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,10,6]]},"reference":[{"key":"9059_CR1","series-title":"Applied Logic Series","volume-title":"Advances in Temporal Logic","author":"H. Barringer","year":"1999","unstructured":"Barringer, H., Fisher, M., Gabbay, D., Gough, G.: Advances in Temporal Logic. Applied Logic Series, vol. 16. Kluwer Academic, Dordrecht (1999)"},{"key":"9059_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Conference on Computer Aided Verification (CAV)","author":"R. Bloem","year":"1999","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Conference on Computer Aided Verification (CAV), Trento, Italy. Lecture Notes in Computer Science, vol. 1633. Springer, Berlin (1999)"},{"key":"9059_CR3","first-page":"35","volume-title":"Lecture Notes in Computer Science","author":"F. Carsten","year":"2003","unstructured":"Carsten, F.: Constructing B\u00fcchi automaton from linear temporal logic using simulation relations for alternating B\u00fcchi automata. In: Lecture Notes in Computer Science, vol. 2759, pp. 35\u201348. Springer, Berlin (2003)"},{"key":"9059_CR4","doi-asserted-by":"crossref","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.: Improved automata generation for linear temporal logic. In: (CAV\u201999), International Conference on Computer-Aided Verification, Trento, Italy (1999)","DOI":"10.1007\/3-540-48683-6_23"},{"key":"9059_CR5","first-page":"996","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logics. In: van Leenwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 996\u20131072. Elsevier Science, Amsterdam (1990)"},{"issue":"3","key":"9059_CR6","doi-asserted-by":"crossref","first-page":"113","DOI":"10.2307\/2271891","volume":"40","author":"H. Friedman","year":"1975","unstructured":"Friedman, H.: One hundred and two problems in mathematical logic. J. Symb. Log. 40(3), 113\u2013130 (1975)","journal-title":"J. Symb. Log."},{"key":"9059_CR7","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-94-009-8384-7_3","volume-title":"Aspects of Phil. Logic","author":"D. Gabbay","year":"1981","unstructured":"Gabbay, D.: An irreflexivity lemma with applications to axiomatizations of conditions of linear frames. In: Monnich, V. (ed.) Aspects of Phil. Logic, pp. 67\u201389. Reidel, Dordrecht (1981)"},{"key":"9059_CR8","series-title":"Lecture Notes in Computer Science","first-page":"409","volume-title":"Proceedings of the 1st Conference on Temporal Logic in Specification","author":"D. Gabbay","year":"1987","unstructured":"Gabbay, D.: The declarative past and imperative future: executable temporal logic for interactive systems. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Proceedings of the 1st Conference on Temporal Logic in Specification. Lecture Notes in Computer Science, vol. 398, pp. 409\u2013448. Springer, Berlin (1987)"},{"key":"9059_CR9","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1093\/logcom\/1.2.229","volume":"1","author":"D.M. Gabbay","year":"1990","unstructured":"Gabbay, D.M., Hodkinson, I.M.: An axiomatisation of the temporal logic with Until and Since over the real numbers. J. Log. Comput. 1, 229\u2013260 (1990)","journal-title":"J. Log. Comput."},{"key":"9059_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0013976","volume-title":"Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1","author":"D.M. Gabbay","year":"1994","unstructured":"Gabbay, D.M., Hodkinson, I.M., Reynolds, M.A.: Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1. Clarendon, Oxford (1994)"},{"issue":"2","key":"9059_CR11","doi-asserted-by":"crossref","first-page":"859","DOI":"10.2307\/2586506","volume":"64","author":"S. Ghilardi","year":"1999","unstructured":"Ghilardi, S.: Unification in intuitionistic logic. J. Symb. Log. 64(2), 859\u2013880 (1999)","journal-title":"J. Symb. Log."},{"key":"9059_CR12","series-title":"CSLI Lecture Notes","volume-title":"Logics of Time and Computation","author":"R. Goldblatt","year":"1992","unstructured":"Goldblatt, R.: Logics of Time and Computation. CSLI Lecture Notes, vol. 7. Stanford University Press, Stanford (1992)"},{"issue":"5\/6","key":"9059_CR13","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/S1570-8683(03)00008-9","volume":"1","author":"R. Goldblatt","year":"2003","unstructured":"Goldblatt, R.: Mathematical modal logic: a view of its evolution. J. Appl. Log. 1(5\/6), 309\u2013392 (2003)","journal-title":"J. Appl. Log."},{"issue":"1","key":"9059_CR14","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1093\/logcom\/2.1.5","volume":"2","author":"V. Goranko","year":"1992","unstructured":"Goranko, V., Passy, S.: Using the universal modality: gains and questions. J. Log. Comput. 2(1), 5\u201330 (1992)","journal-title":"J. Log. Comput."},{"key":"9059_CR15","doi-asserted-by":"crossref","first-page":"27","DOI":"10.2307\/2964334","volume":"25","author":"R. Harrop","year":"1960","unstructured":"Harrop, R.: Concerning formulas of the types A\u2192B \u2228 C, A\u2192\u2203 xB(x) in intuitionistic formal system. J. Symb. Log. 25, 27\u201332 (1960)","journal-title":"J. Symb. Log."},{"key":"9059_CR16","doi-asserted-by":"crossref","first-page":"281","DOI":"10.2307\/2694922","volume":"66","author":"R. Iemhoff","year":"2001","unstructured":"Iemhoff, R.: On the admissible rules of intuitionistic propositional logic. J. Symb. Log. 66, 281\u2013294 (2001)","journal-title":"J. Symb. Log."},{"key":"9059_CR17","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1093\/logcom\/exi029","volume":"15","author":"E. Jer\u00e1bek","year":"2005","unstructured":"Jer\u00e1bek, E.: Admissible rules of modal logics. J. Log. Comput. 15, 411\u2013431 (2005)","journal-title":"J. Log. Comput."},{"issue":"3","key":"9059_CR18","doi-asserted-by":"crossref","first-page":"756","DOI":"10.1017\/S002248120002973X","volume":"52","author":"B.M. Kapron","year":"1987","unstructured":"Kapron, B.M.: Modal sequents and definability. J. Symb. Log. 52(3), 756\u2013765 (1987)","journal-title":"J. Symb. Log."},{"issue":"1","key":"9059_CR19","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1002\/malq.200410009","volume":"51","author":"M. Lange","year":"2005","unstructured":"Lange, M.: A quick axiomatisation of LTL with past. Math. Log. Q. 51(1), 83\u201388 (2005)","journal-title":"Math. Log. Q."},{"key":"9059_CR20","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS\u201902), Copenhagen, Denmark, pp. 383\u2013392 (2002)","DOI":"10.1109\/LICS.2002.1029846"},{"issue":"1","key":"9059_CR21","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","volume":"8","author":"O. Lichtenstein","year":"2000","unstructured":"Lichtenstein, O., Pnueli, A.: Propositional temporal logics: decidability and completeness. Log. J. IGPL 8(1), 55\u201385 (2000)","journal-title":"Log. J. IGPL"},{"key":"9059_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-01539-1","volume-title":"Einf\u00fchrung in die Operative Logik und Mathematik","author":"P. Lorenzen","year":"1955","unstructured":"Lorenzen, P.: Einf\u00fchrung in die Operative Logik und Mathematik. Springer, Berlin (1955)"},{"key":"9059_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin (1992)"},{"key":"9059_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/3-540-45022-X_37","volume-title":"Proceedings of the 27th Int. Colloq. Aut. Lang. Prog. (ICALP 2000)","author":"Z. Manna","year":"2000","unstructured":"Manna, Z., Sipma, H.: Alternating the temporal picture for safety. In: Proceedings of the 27th Int. Colloq. Aut. Lang. Prog. (ICALP 2000). Lecture Notes in Computer Science, vol. 1853, pp. 429\u2013450. Springer, Berlin (2000)"},{"issue":"4","key":"9059_CR25","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1007\/BF01084082","volume":"6","author":"G.E. Mints","year":"1976","unstructured":"Mints, G.E.: Derivability of admissible rules. J. Soviet Math. 6(4), 417\u2013421 (1976)","journal-title":"J. Soviet Math."},{"key":"9059_CR26","first-page":"46","volume-title":"Proceedings of the 18th Annual Symposium on Foundations of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE, New York (1977)"},{"issue":"5","key":"9059_CR27","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/BF01982031","volume":"23","author":"V.V. Rybakov","year":"1984","unstructured":"Rybakov, V.V.: A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic. Alg. Log. 23(5), 369\u2013384 (1984) (Engl. translation)","journal-title":"Alg. Log."},{"key":"9059_CR28","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/BF01978706","volume":"24","author":"V.V. Rybakov","year":"1985","unstructured":"Rybakov, V.V.: The bases for admissible rules of logics S4 and int. Alg. Log. 24, 55\u201368 (1985) (English translation)","journal-title":"Alg. Log."},{"issue":"3","key":"9059_CR29","doi-asserted-by":"crossref","first-page":"912","DOI":"10.2307\/2275439","volume":"57","author":"V.V. Rybakov","year":"1992","unstructured":"Rybakov, V.V.: Rules of inference with parameters for intuitionistic logic. J. Symb. Log. 57(3), 912\u2013923 (1992)","journal-title":"J. Symb. Log."},{"issue":"1","key":"9059_CR30","doi-asserted-by":"crossref","first-page":"266","DOI":"10.2307\/2275521","volume":"60","author":"V.V. Rybakov","year":"1995","unstructured":"Rybakov, V.V.: Hereditarily structurally complete modal logics. J. Symb. Log. 60(1), 266\u2013288 (1995)","journal-title":"J. Symb. Log."},{"key":"9059_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BFb0022279","volume-title":"Proceedings of the Conference CSL\u201994","author":"V.V. Rybakov","year":"1995","unstructured":"Rybakov, V.V.: Modal logics preserving admissible for S4 inference rules. In: Proceedings of the Conference CSL\u201994. Lecture Notes in Computer Science, vol. 993, pp. 512\u2013526. Springer, Berlin (1995)"},{"key":"9059_CR32","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Admissible Logical Inference Rules","author":"V.V. Rybakov","year":"1997","unstructured":"Rybakov, V.V.: Admissible Logical Inference Rules. Studies in Logic and the Foundations of Mathematics, vol. 136. Elsevier Science\/North-Holland, New York\/Amsterdam (1997)"},{"key":"9059_CR33","first-page":"333","volume-title":"Lecture Notes in Computer Science","author":"V.V. Rybakov","year":"1997","unstructured":"Rybakov, V.V.: Quasi-characteristic inference rules. In: Adian, S., Nerode, A. (eds.) Lecture Notes in Computer Science, vol. 1234, pp. 333\u2013342. Springer, Berlin (1997)"},{"issue":"4","key":"9059_CR34","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1002\/malq.19990450409","volume":"45","author":"V.V. Rybakov","year":"1999","unstructured":"Rybakov, V.V., Kiyatkin, V.R., Oner, T.: On finite model property for admissible rules. Math. Log. Q. 45(4), 505\u2013520 (1999)","journal-title":"Math. Log. Q."},{"issue":"2","key":"9059_CR35","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1002\/(SICI)1521-3870(200005)46:2<207::AID-MALQ207>3.0.CO;2-E","volume":"46","author":"V.V. Rybakov","year":"2000","unstructured":"Rybakov, V.V., Terziler, M., Rimazki, V.: Basis in semi-reduced form for the admissible rules of the intuitionistic logic IPC. Math. Log. Q. 46(2), 207\u2013218 (2000)","journal-title":"Math. Log. Q."},{"issue":"4","key":"9059_CR36","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1002\/1521-3870(200111)47:4<441::AID-MALQ441>3.0.CO;2-J","volume":"47","author":"V.V. Rybakov","year":"2001","unstructured":"Rybakov, V.V.: Construction of an explicit basis for rules admissible in modal system S4. Math. Log. Q. 47(4), 441\u2013451 (2001)","journal-title":"Math. Log. Q."},{"issue":"5","key":"9059_CR37","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1093\/logcom\/exi025","volume":"15","author":"V.V. Rybakov","year":"2005","unstructured":"Rybakov, V.V.: Logical consecutions in intransitive temporal linear logic of finite intervals. J. Log. Comput. 15(5), 633\u2013657 (2005)","journal-title":"J. Log. Comput."},{"issue":"4","key":"9059_CR38","doi-asserted-by":"crossref","first-page":"1137","DOI":"10.2178\/jsl\/1129642119","volume":"70","author":"V.V. Rybakov","year":"2005","unstructured":"Rybakov, V.V.: Logical consecutions in discrete linear temporal logic. J. Symb. Log. 70(4), 1137\u20131149 (2005)","journal-title":"J. Symb. Log."},{"issue":"3","key":"9059_CR39","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"issue":"1","key":"9059_CR40","doi-asserted-by":"crossref","first-page":"00","DOI":"10.2307\/2272558","volume":"37","author":"S.K. Thomason","year":"1972","unstructured":"Thomason, S.K.: Semantic analysis of tense logic. J. Symb. Log. 37(1), 00\u201300 (1972)","journal-title":"J. Symb. Log."},{"key":"9059_CR41","series-title":"Synthese Library","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-010-9868-7","volume-title":"The Logic of Time","author":"J. Benthem van","year":"1983","unstructured":"van Benthem, J.: The Logic of Time. Synthese Library, vol. 156. Reidel, Dordrecht (1983)"},{"key":"9059_CR42","unstructured":"Vardi, M.: An automata-theoretic approach to linear temporal logic. In: Proceedings of the Banff Workshop on Knowledge Acquisition (Banff\u201994) (1994)"},{"key":"9059_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"Proceedings of the 25th International Colloquium on Automata, Languages, and Programming","author":"M. Vardi","year":"1998","unstructured":"Vardi, M.: Reasoning about the past with two-way automata. In: Proceedings of the 25th International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science, vol. 1443, pp. 628\u2013641. Springer, Berlin (1998)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9059-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-007-9059-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9059-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T11:51:34Z","timestamp":1558698694000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-007-9059-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,6]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,8]]}},"alternative-id":["9059"],"URL":"https:\/\/doi.org\/10.1007\/s00224-007-9059-9","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10,6]]}}}