{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T13:46:42Z","timestamp":1751982402487},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677970"},{"type":"electronic","value":"9783540449577"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44957-4_35","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T01:24:41Z","timestamp":1180661081000},"page":"523-537","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["On an \u03c9-Decidable Deductive Procedure for Non-Horn Sequents of a Restricted FTL"],"prefix":"10.1007","author":[{"given":"Regimantas","family":"Pliu\u0161kevi\u010dius","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"key":"35_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(89)90138-2","volume":"64","author":"M. Abadi","year":"1989","unstructured":"Abadi M.: The power of temporal proofs. Theoretical Comp. Sci. 64 (1989) 35\u201384.","journal-title":"Theoretical Comp. Sci."},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"Fisher M.: A normal form for temporal logics and its applications in theorem proving and execution. Journal of Logic and Computation 7(4) (1997).","DOI":"10.1093\/logcom\/7.4.429"},{"issue":"1","key":"35_CR3","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1142\/S0218843097000057","volume":"6","author":"M. Fisher","year":"1997","unstructured":"Fisher M., Wooldridge M.: On the formal specification and verification of multi-agent systems. Intern. Journal of Cooperative Information Systems 6(1) (1997) 37\u201365.","journal-title":"Intern. Journal of Cooperative Information Systems"},{"key":"35_CR4","unstructured":"Hodkinson I., Wolter F., Zakharyaschev M.: Decidable fragments of first-order temporal logics. (To appear in: Annals of Pure and Applied Logic)."},{"key":"35_CR5","doi-asserted-by":"publisher","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. Zeitchr. fur Math. Logic und Grundlagen der Math. 33 (1987) 423\u2013452.","journal-title":"Zeitchr. fur Math. Logic und Grundlagen der Math"},{"key":"35_CR6","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/BF00881951","volume":"13","author":"R. Pliu\u0161kevi\u010dius","year":"1994","unstructured":"Pliu\u0161kevi\u010dius R.: The saturated tableaux for a linear miniscoped Horn-like temporal logic. Journal of Automated Reasoning 13 (1994) 51\u201367.","journal-title":"Journal of Automated Reasoning"},{"issue":"1\u20132","key":"35_CR7","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1080\/11663081.1998.10510936","volume":"8","author":"R. Pliu\u0161kevi\u010dius","year":"1998","unstructured":"Pliu\u0161kevi\u010dius R.: Replacement of induction by similarity saturation in a first-order linear temporal logic. Journal of Applied Non-Classical Logics 8(1\u20132) (1998) 141\u2013169.","journal-title":"Journal of Applied Non-Classical Logics"},{"issue":"3","key":"35_CR8","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/BF02465850","volume":"39","author":"R. Pliu\u0161kevi\u010dius","year":"1999","unstructured":"Pliu\u0161kevi\u010dius R.: Infinitary calculus for a restricted first-order linear temporal logic without contraction of quantified formulas. Lithuanian Mathematical Journal 39(3) (1999) 378\u2013397.","journal-title":"Lithuanian Mathematical Journal"},{"key":"35_CR9","unstructured":"Pliu\u0161kevi\u010dius R.: An effective deductive procedure for a restricted first-order linear temporal logic. (Submitted to Annals of Pure and Applied Logic)."},{"key":"35_CR10","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(86)90157-X","volume":"47","author":"A. Szalas","year":"1986","unstructured":"Szalas A.: Concerning the semantic consequence relation in first-order temporal logic. Theoretical Comput. Sci. 47 (1986) 329\u2013334.","journal-title":"Theoretical Comput. Sci."},{"key":"35_CR11","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0304-3975(87)90129-0","volume":"54","author":"A. Szalas","year":"1987","unstructured":"Szalas A.: A complete axiomatic characterization of first-order temporal logic of linear time. Theoretical Comput. Sci. 54 (1987) 199\u2013214.","journal-title":"Theoretical Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Computational Logic \u2014 CL 2000"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44957-4_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T09:30:53Z","timestamp":1558258253000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44957-4_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677970","9783540449577"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-44957-4_35","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"15 December 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}