{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:27:31Z","timestamp":1764782851520},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2004,6,14]],"date-time":"2004-06-14T00:00:00Z","timestamp":1087171200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2004,11]]},"DOI":"10.1007\/s00153-004-0237-z","type":"journal-article","created":{"date-parts":[[2004,6,22]],"date-time":"2004-06-22T11:30:49Z","timestamp":1087903849000},"page":"965-990","source":"Crossref","is-referenced-by-count":14,"title":["An approach to infinitary temporal proof theory"],"prefix":"10.1007","volume":"43","author":[{"given":"Stefano","family":"Baratella","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Masini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,6,14]]},"reference":[{"key":"237_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(95)00045-X","volume":"151","author":"Ambler","year":"1995","unstructured":"Ambler, S., Kwiatkowska, M., Measor, N.: Duality and the completeness of modal \u03bc\u2013calculus. Theor. Comp. Sci. 151, 3\u201327 (1995)","journal-title":"Theor. Comp. Sci."},{"key":"237_CR2","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/S0168-0072(03)00021-6","volume":"123","author":"Baratella","year":"2003","unstructured":"Baratella, S., Masini, A.: A proof-theoretic investigation of a logic of positions. Ann. Pure Appl. Logic 123, 135\u2013162 (2003)","journal-title":"Ann. Pure Appl. Logic"},{"key":"237_CR3","doi-asserted-by":"crossref","unstructured":"Basin, D., Matthews, S., Vigan\u00f2, L.: Labelled modal logics: quantifiers. J. Logic, Lang. Inf. 7\u20133, 237\u2013263 (1998)","DOI":"10.1023\/A:1008278803780"},{"key":"237_CR4","doi-asserted-by":"crossref","unstructured":"Cerrito, S., Cialdea Mayer, M.: Bounded model search in linear temporal logic and its application to planning. In: H. De Swart (ed.) Automated Resoning with Analytic Tableaux and Related Methods, Lec. Notes in Artificial Intelligence, 1937, (Springer, Berlin, 1998), pp. 141\u2013152","DOI":"10.1007\/3-540-69778-0_18"},{"key":"237_CR5","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: J. van Leeuwen (ed.), Handbook of theoretical computer science. Vol. B: formal models and semantics (Elsevier, Amsterdam, 1990), pp. 995\u20131072","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"237_CR6","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs as fixpoints. In: Proc. 7th Int. Colloq. Aut. Lang. Prog., Lec. Notes in Comp. Sci. 85, (Springer, Berlin, 1981), pp. 169\u2013181"},{"key":"237_CR7","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal logic: mathematical foundations and computational aspects. Vol. 1. (Oxford University Press, Oxford, 1994)","DOI":"10.1007\/BFb0013976"},{"key":"237_CR8","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proc. 7th ACM Symposium on Principles of Programming Languages (ACM Press, 1980), pp. 163\u2013173","DOI":"10.1145\/567446.567462"},{"key":"237_CR9","doi-asserted-by":"crossref","unstructured":"Garson, J.W.: Quantification in modal logic. In: D.M. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, Vol II (Reidel, Dordrecht, 1984), pp. 249\u2013307","DOI":"10.1007\/978-94-009-6259-0_5"},{"key":"237_CR10","unstructured":"Girard, J.-Y.: Proof theory and logical complexity, vol. I (Bibliopolis, Napoli, 1987)"},{"key":"237_CR11","doi-asserted-by":"crossref","first-page":"735","DOI":"10.1093\/jigpal\/6.5.735","volume":"6","author":"Guerrini","year":"1998","unstructured":"Guerrini, S., Martini, S., Masini, A.: An analysis of (linear) exponentials based on extended sequents. Logic J. IGPL, 6, 735\u2013753 (1998)","journal-title":"Logic J. IGPL,"},{"key":"237_CR12","doi-asserted-by":"crossref","unstructured":"Harel, D.: Dynamic Logic. In: Handbook of Philosophical Logic. Vol. II. Extensions of classical logic. D. Gabbay and F. Guenthner (eds.), Synthese Library 165, (D. Reidel Publishing Co., 1984), pp. 497\u2013604","DOI":"10.1007\/978-94-009-6259-0_10"},{"key":"237_CR13","unstructured":"Kamp, J.: Tense logic and the theory of linear order. Ph.D Thesis, UCLA, USA 1968"},{"key":"237_CR14","doi-asserted-by":"crossref","unstructured":"Martini, S., Masini, A.: A computational interpretation of modal proofs. In: H. Wansing (ed.), Proof theory of modal logic, (Kluwer, 1996), pp. 213\u2013241","DOI":"10.1007\/978-94-017-2798-3_12"},{"key":"237_CR15","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0168-0072(92)90029-Y","volume":"58","author":"Masini","year":"1992","unstructured":"Masini, A.: 2-sequent calculus: a proof theory of modalities. Ann. Pure Appl. Logic 58, 229\u2013246 (1992)","journal-title":"Ann. Pure Appl. Logic"},{"key":"237_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. 18th Annual Symposium on Foundations of Computer Science (Providence, R.I., 1977), IEEE Comput. Sci., Long Beach, Calif, 1977, pp. 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"237_CR17","doi-asserted-by":"crossref","unstructured":"Reynolds, M.: An axiomatization of full computation tree logic. J. Symbolic Logic, 66\u20133, 1011\u20131057 (2001)","DOI":"10.2307\/2695091"},{"key":"237_CR18","doi-asserted-by":"crossref","unstructured":"Sch\u00fctte, K.: Proof theory, Translated from the revised German edition by J. N. Crossley. Grundlehren der Mathematischen Wissenschaften, Band 225. (Springer\u2013Verlag, Berlin\u2013New York, 1977)","DOI":"10.1007\/978-3-642-66473-1"},{"key":"237_CR19","doi-asserted-by":"crossref","unstructured":"Segerberg, K.: A model existence theorem in infinitary propositional modal logic. J. Philos. Log. 23\u20134, 337\u2013367 (1994)","DOI":"10.1007\/BF01048686"},{"key":"237_CR20","doi-asserted-by":"crossref","unstructured":"Sisla, A., Clarke, E.: The complexity of propositional linear temporal logic. J. ACM 32\u20133, 733\u2013749 (1985)","DOI":"10.1145\/3828.3837"},{"key":"237_CR21","doi-asserted-by":"crossref","unstructured":"Szalas, A.: A complete axiomatic characterization of first-order temporal logic of linear time. Theoret. Comput. Sci. 54\u20132-3, 199\u2013214 (1987)","DOI":"10.1016\/0304-3975(87)90129-0"},{"key":"237_CR22","doi-asserted-by":"crossref","first-page":"81","DOI":"10.3233\/FI-1996-2616","volume":"26","author":"Szalas","year":"1996","unstructured":"Szalas, A.: On natural deduction in first-order fixpoint logics. Fundamenta Informatic\u00e6 26, 81\u201394 (1996)","journal-title":"Fundamenta Informatic\u00e6"},{"key":"237_CR23","unstructured":"Takeuti, G.: Proof theory (North-Holland, Amsterdam, 1975)"},{"key":"237_CR24","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logic of programs. J. Comput. Sys. Sci. 32, 183\u2013221 (1986)","journal-title":"J. Comput. Sys. Sci."}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-004-0237-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00153-004-0237-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-004-0237-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,28]],"date-time":"2023-04-28T21:57:55Z","timestamp":1682719075000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00153-004-0237-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,6,14]]},"references-count":24,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2004,11]]}},"alternative-id":["237"],"URL":"https:\/\/doi.org\/10.1007\/s00153-004-0237-z","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,6,14]]}}}