{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,14]],"date-time":"2026-10-14T22:47:05Z","timestamp":1792018025927,"version":"4.4.0"},"publisher-location":"Berlin\/Heidelberg","reference-count":22,"publisher":"Springer-Verlag","isbn-type":[{"value":"354051659X","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0026305","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T10:35:17Z","timestamp":1132396517000},"page":"240-253","source":"Crossref","is-referenced-by-count":19,"title":["Gentzen-Systems for propositional temporal logics"],"prefix":"10.1007","author":[{"given":"Barbara","family":"Paech","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","first-page":"1","volume":"193","author":"M. Abadi","year":"1985","unstructured":"M. Abadi,Z. Manna Non-clausal temporal deduction (Logics of Programs, Springer-Verlag LNCS 193, pp1\u201315, 1985)","journal-title":"LNCS"},{"key":"14_CR2","first-page":"402","volume":"25","author":"M. Ben-Ari","year":"1982","unstructured":"M. Ben-Ari,J.Y. Halpern,A. Pnueli Deterministic propositional dynamic logic: Finite models, complexity and completeness (JCSS 25,pp 402\u2013417, 1982)","journal-title":"JCSS"},{"key":"14_CR3","first-page":"1","volume-title":"On a decision method in restricted second order arithmetic","author":"J.R. B\u00fcchi","year":"1962","unstructured":"J.R. B\u00fcchi On a decision method in restricted second order arithmetic (Logic,Methodology and Philosophy of Science 1960, Stanford Univ.Press, Stanford,Calif.,pp 1\u201311, 1962)"},{"key":"14_CR4","first-page":"113","volume":"170","author":"A. Cavalli","year":"1984","unstructured":"A. Cavalli,L. Farinas del Cerro A decision method for linear temporal logic (7th Int. Conf. on Automated Deduction, Springer-Verlag LNCS 170, pp 113\u2013127, 1984)","journal-title":"LNCS"},{"key":"14_CR5","unstructured":"R.L.Constable et al. Implementing Mathematics with the Nuprl Proof Development System (Prentice-Hall,1986)"},{"key":"14_CR6","first-page":"1","volume":"30","author":"E.A. Emerson","year":"1985","unstructured":"E.A. Emerson,J.Y. Halpern Decision procedures and expressiveness in the temporal logic of branching time (JCSS 30, pp 1\u201324, 1985)","journal-title":"JCSS"},{"key":"14_CR7","first-page":"177","volume":"39","author":"G. Gentzen","year":"1933","unstructured":"G. Gentzen Untersuchungen \u00fcber das logische Schlie\u00dfen I (Mathematische Zeitschrift 39, pp 177\u2013210, 1933)","journal-title":"Mathematische Zeitschrift"},{"key":"14_CR8","first-page":"144","volume":"25","author":"D. Harel","year":"1982","unstructured":"D. Harel,D. Kozen,R. Parikh Process Logic: Expressiveness, decidability and completeness (JCSS 25, pp 144\u2013170, 1982)","journal-title":"JCSS"},{"key":"14_CR9","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0304-3975(85)90225-7","volume":"38","author":"D. Harel","year":"1985","unstructured":"D. Harel,D. Peleg Process Logic with regular formulas (TCS 38, pp 307\u2013322, 1985)","journal-title":"TCS"},{"key":"14_CR10","unstructured":"J.E.Hopcroft,J.D.Ullman Introduction to automata theory, languages and computation (Addison-Wesley, 1979)"},{"key":"14_CR11","volume-title":"Tense Logic and the theory of linear order","author":"J.A.W. Kamp","year":"1968","unstructured":"J.A.W. Kamp Tense Logic and the theory of linear order (PhD thesis Univ.of Calif., LA,1968)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"F.Kr\u00f6ger Temporal Logic of Programs (Springer-Verlag, 1987)","DOI":"10.1007\/978-3-642-71549-5"},{"key":"14_CR13","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/S0019-9958(77)90443-0","volume":"33","author":"R. Ladner","year":"1977","unstructured":"R. Ladner Application of Model theoretic games to discrete linear orders and finite automata (Information and Control 33, pp 281\u2013303, 1977) \u03a9","journal-title":"Information and Control"},{"key":"14_CR14","unstructured":"D. Miller, A. Felty An integration of resolution and natural deduction theorem proving (Nat.Conf.on AI, Philadelphia,PA, 1986)"},{"key":"14_CR15","volume-title":"Executing temporal logic programs","author":"B. Moszkowski","year":"1986","unstructured":"B. Moszkowski Executing temporal logic programs (Cambridge, Univ.Press, 1986)"},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/BF00268322","volume":"12","author":"H. Nishimura","year":"1979","unstructured":"H. Nishimura Sequential method in propositional dynamic logic (Acta Informatica 12, pp 377\u2013400, 1979)","journal-title":"Acta Informatica"},{"key":"14_CR17","unstructured":"B.Paech Gentzen-Systems for propositional temporal logics (LMU M\u00fcnchen, Institut f\u00fcr Informatik, Bericht 88\/01, 1988)"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"V.R.Pratt Semantical considerations on Floyd-Hoare logic (17th IEEE Symp. on Foundations of Computer Science,pp 109\u2013121, 1976)","DOI":"10.1109\/SFCS.1976.27"},{"key":"14_CR19","unstructured":"R.Rosner, A.Pnueli A Choppy Logic (Logic in Computer Science,pp 306\u2013314, 1986)"},{"key":"14_CR20","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1016\/S0019-9958(79)90629-6","volume":"42","author":"W. Thomas","year":"1979","unstructured":"W. Thomas Star-free regular sets of \u03c9-sequences (Information and Control 42, pp 148\u2013156, 1979)","journal-title":"Information and Control"},{"key":"14_CR21","first-page":"482","volume":"74","author":"M.K. Valiev","year":"1979","unstructured":"M.K. Valiev On axiomatization of deterministic propositional dynamic logic (Springer-Verlag LNCS 74, pp 482\u2013491, 1979)","journal-title":"LNCS"},{"key":"14_CR22","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper Temporal logic can be more expressive (Information and Control 56, pp 72\u201399, 1983)","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","CSL '88"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0026305.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:56:03Z","timestamp":1607550963000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0026305"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354051659X"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0026305","relation":{},"subject":[]}}