{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:07:54Z","timestamp":1761620874433},"reference-count":12,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1994,10,1]],"date-time":"1994-10-01T00:00:00Z","timestamp":780969600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1994,10]]},"DOI":"10.1007\/bf00881951","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:25:12Z","timestamp":1104002712000},"page":"391-407","source":"Crossref","is-referenced-by-count":15,"title":["The saturated tableaux for linear miniscoped horn-like temporal logic"],"prefix":"10.1007","volume":"13","author":[{"given":"Regimantas","family":"Pliu\u0161kevi\u010dius","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF00881951_CR1","unstructured":"Fisher, M.:A Resolution Method for Temporal Logic, Proc. IJCAI, Sydney, 1991"},{"key":"BF00881951_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1990","unstructured":"Fitting, M.:First-Order Logic and Automated Theorem Proving, Springer-Verlag, Berlin, 1990."},{"key":"BF00881951_CR3","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"J. H. Gallier","year":"1986","unstructured":"Gallier, J. H.:Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, New York, 1986."},{"key":"BF00881951_CR4","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1002\/malq.19870330506","volume":"33","author":"H. Kawai","year":"1987","unstructured":"Kawai, H.: Sequential calculus for a first order infinitary temporal logic,Zeitshr. f\u00fcr Math. Logic und Grundlagen der Math. 33 (1987), 423\u2013432.","journal-title":"Zeitshr. f\u00fcr Math. Logic und Grundlagen der Math."},{"key":"BF00881951_CR5","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1007\/BFb0029643","volume-title":"Mathematical Foundations of Computer Science 1990","author":"R. Pliu\u0161kevi\u010dius","year":"1990","unstructured":"Pliu\u0161kevi\u010dius, R.: Investigation of finitary calculi for temporal logic by means of infinitary calculi, in B. Rovan (ed.),Mathematical Foundations of Computer Science 1990, Lecture Notes in Comput. Sci., 452, Springer-Verlag, Berlin, 1990, pp. 464\u2013469."},{"key":"BF00881951_CR6","doi-asserted-by":"crossref","unstructured":"Pliu\u0161kevi\u010dius, R.: On saturated calculi for a linear temporal logic, in A. Borzyszkowski and S. Sokolowski (eds),Mathematical Foundations of Computer Science 1993, Lecture Notes in Comput. Sci., 711, Springer-Verlag, 1993, pp. 640\u2013649.","DOI":"10.1007\/3-540-57182-5_55"},{"key":"BF00881951_CR7","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BFb0022577","volume-title":"Computational Logic and Proof Theory","author":"R. Pliu\u0161kevi\u010dius","year":"1993","unstructured":"Pliu\u0161kevi\u010dius, R.: On the saturation principle for a linear temporal logic, in G. Gottlob, A. Leitsch and D. Mundici (eds),Computational Logic and Proof Theory, Lecture Notes in Comput. Sci., 713, Springer-Verlag, Berlin, 1993, pp. 289\u2013300."},{"key":"BF00881951_CR8","doi-asserted-by":"crossref","unstructured":"Pratt, V. R.: A practical decision method for propositional dynamic logic,ACM Symp. on Theory of Computing, 1978, 326\u2013337.","DOI":"10.1145\/800133.804362"},{"key":"BF00881951_CR9","first-page":"138","volume-title":"Handbook of Philosophical Logics, vol. 1","author":"G. Sundholm","year":"1983","unstructured":"Sundholm, G.: Systems of deduction, in D. Gabbay and F. Guenthner (eds),Handbook of Philosophical Logics, vol. 1, D. Reidel, Dordrecht, 1983, pp. 138\u2013188."},{"key":"BF00881951_CR10","unstructured":"Valiev, M.: On temporal logic of von Wright (in Russian),The second Soviet-Finland Colloquium on Logic, Moscow, 1979, pp. 7\u201311."},{"key":"BF00881951_CR11","first-page":"119","volume":"28","author":"P. Wolper","year":"1985","unstructured":"Wolper, P.: The tableaux method for temporal logic: an overview,Log. et anal. 28 (1985), 119\u2013136.","journal-title":"Log. et anal."},{"key":"BF00881951_CR12","volume-title":"Modal Logic: The Lewis-Modal Systems","author":"J. J. Zeman","year":"1973","unstructured":"Zeman, J. J.:Modal Logic: The Lewis-Modal Systems, Oxford University Press, Oxford, 1973."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881951.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881951\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881951","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:30:00Z","timestamp":1586043000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881951"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,10]]},"references-count":12,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994,10]]}},"alternative-id":["BF00881951"],"URL":"https:\/\/doi.org\/10.1007\/bf00881951","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,10]]}}}