{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:30:23Z","timestamp":1764783023437},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540749141"},{"type":"electronic","value":"9783540749158"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74915-8_36","type":"book-chapter","created":{"date-parts":[[2007,8,24]],"date-time":"2007-08-24T05:13:35Z","timestamp":1187932415000},"page":"481-495","source":"Crossref","is-referenced-by-count":8,"title":["A Cut-Free and Invariant-Free Sequent Calculus for PLTL"],"prefix":"10.1007","author":[{"given":"Joxe","family":"Gaintzarain","sequence":"first","affiliation":[]},{"given":"Montserrat","family":"Hermo","sequence":"additional","affiliation":[]},{"given":"Paqui","family":"Lucio","sequence":"additional","affiliation":[]},{"given":"Marisa","family":"Navarro","sequence":"additional","affiliation":[]},{"given":"Fernando","family":"Orejas","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"36_CR1","unstructured":"Fisher, M.: A resolution method for temporal logic. In: IJCAI, pp. 99\u2013104 (1991)"},{"key":"36_CR2","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/567446.567462","volume-title":"POPL 1980","author":"D. Gabbay","year":"1980","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL 1980. Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, New York, NY, USA, pp. 163\u2013173. ACM Press, New York (1980)"},{"key":"36_CR3","volume-title":"Mathematische Zeitschrift","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G.: Untersuchungen \u00c4uber das logische schliessen (English translation in The collected papers of Gerhard Gentzen, pp. 68\u2013131). In: Szabo, M.E. (ed.) Mathematische Zeitschrift, vol.\u00a039, North-Holland, Amsterdam (1969)"},{"key":"36_CR4","unstructured":"Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. PhD. Thesis, University of California, Los Angeles (1968)"},{"key":"36_CR5","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Propositional temporal logics: Decidability and completeness. Logic Journal of the IGPL\u00a08(1) (2000)","DOI":"10.1093\/jigpal\/8.1.55"},{"key":"36_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/BFb0026305","volume-title":"CSL\u201988","author":"B. Paech","year":"1989","unstructured":"Paech, B.: Gentzen-systems for propositional temporal logics. In: B\u00f6rger, E., Kleine B\u00fcning, H., Richter, M.M. (eds.) CSL 1988. LNCS, vol.\u00a0385, pp. 240\u2013253. Springer, Heidelberg (1989)"},{"issue":"1-2","key":"36_CR7","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1006\/inco.1999.2832","volume":"157","author":"F. Pfenning","year":"2000","unstructured":"Pfenning, F.: Structural cut elimination: I. intuitionistic and classical logic. Inf. Comput.\u00a0157(1-2), 84\u2013141 (2000)","journal-title":"Inf. Comput."},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"Pliuskevicius, R.: Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus. Baltic Computer Science, 504\u2013528 (1991)","DOI":"10.1007\/BFb0019366"},{"key":"36_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S1574-6526(05)80011-2","volume-title":"Handbook of Temporal Reasoning in Artificial Intelligence","author":"M. Reynolds","year":"2005","unstructured":"Reynolds, M., Dixon, C.: Theorem-proving for discrete temporal logic. In: Handbook of Temporal Reasoning in Artificial Intelligence, pp. 279\u2013314. Elsevier, Amsterdam (2005)"},{"issue":"3","key":"36_CR10","doi-asserted-by":"publisher","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 logics. J. ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"36_CR11","doi-asserted-by":"crossref","unstructured":"Szalas, A.: Temporal logic of programs: A standard approach. In: Time and Logic. A Computational Approach, pp. 1\u201350. UCL Press Ltd (1995)","DOI":"10.4324\/9780429321047-1"},{"issue":"1\u20132","key":"36_CR12","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Information and Control\u00a056(1\u20132), 72\u201399 (1983)","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74915-8_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:24:58Z","timestamp":1605763498000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74915-8_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540749141","9783540749158"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74915-8_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}