{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:19:29Z","timestamp":1725664769393},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540616306"},{"type":"electronic","value":"9783540706434"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61630-6_23","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:09:00Z","timestamp":1330276140000},"page":"320-336","source":"Crossref","is-referenced-by-count":0,"title":["Similarity saturation for first order linear temporal logic with UNLESS"],"prefix":"10.1007","author":[{"given":"Regimantas","family":"Pliu\u0161kevi\u010dius","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"23_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(89)90138-2","volume":"64","author":"M. Abadi","year":"1989","unstructured":"M. Abadi: The power of temporal proofs. Theoret. Comput. Sci. 64, 35\u201384 (1989)","journal-title":"Theoret. Comput. Sci."},{"key":"23_CR2","first-page":"135","volume":"379","author":"H. Andreka","year":"1989","unstructured":"H. Andreka, J. Nemeti, J. Sain: On the strenghth of temporal proof. LNCS 379, 135\u2013144 (1989)","journal-title":"LNCS"},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1093\/comjnl\/30.2.134","volume":"30","author":"H. Barringer","year":"1987","unstructured":"H. Barringer: Up and down the temporal way. The Comput Journ. 30, 134\u2013148 (1987)","journal-title":"The Comput Journ."},{"key":"23_CR4","first-page":"53","volume-title":"Temporal logics and their applications","author":"H. Barringer","year":"1987","unstructured":"H. Barringer: The use of temporal logic in the compositional specification of concurrent systems. In: A. Galton (ed.): Temporal logics and their applications. London: Academic Press 1987, pp. 53\u201390"},{"key":"23_CR5","unstructured":"M. Ben-Ari: Mathematical Logic for Computer Science. Prentice Hall 1993"},{"key":"23_CR6","first-page":"370","volume":"607","author":"M. Fisher","year":"1992","unstructured":"M. Fisher: A normal form for first order temporal formulae. LNCS 607, 370\u2013384 (1992)","journal-title":"LNCS"},{"key":"23_CR7","first-page":"409","volume":"398","author":"D.M. Gabbay","year":"1987","unstructured":"D.M. Gabbay: The declarative past and the imperative future. LNCS 398, 409\u2013448 (1987)","journal-title":"LNCS"},{"key":"23_CR8","volume-title":"Vol. 1. Oxford Science Foundations","author":"M. Gabbay","year":"1994","unstructured":"M. Gabbay, I. Hodkinson, M. Reynolds: Temporal logic. Mathematical Foundations and Computational Aspects. Vol. 1. Oxford Science Foundations. Oxford: Claredon Press 1994"},{"key":"23_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-71549-5","volume-title":"Temporal Logic of Programs","author":"F. Kroger","year":"1987","unstructured":"F. Kroger: Temporal Logic of Programs. Berlin etc: Spriger-Verlag 1987"},{"key":"23_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0304-3975(90)90161-A","volume":"73","author":"F. Kroger","year":"1990","unstructured":"F. Kroger: On the interpretability of arithmetic in temporal logic. Theoret. Comput. Sci. 73, 47\u201360 (1990)","journal-title":"Theoret. Comput. Sci."},{"key":"23_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems Specifications","author":"Z. Manna","year":"1992","unstructured":"Z. Manna, A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems Specifications. New York etc: Springer-Verlag 1992"},{"key":"23_CR12","first-page":"382","volume":"620","author":"R. Pliu\u0161kevi\u010dius","year":"1992","unstructured":"R. Pliu\u0161kevi\u010dius: Complete sequential calculi for the first order symmetrical linear temporal logic with UNTIL and SINCE. LNCS 620, 382\u2013393 (1992)","journal-title":"LNCS"},{"key":"23_CR13","first-page":"289","volume":"713","author":"R. Pliu\u0161kevi\u010dius","year":"1993","unstructured":"R. Pliu\u0161kevi\u010dius: On saturation principle for a linear temporal logic. LNCS 713, 289\u2013300 (1993)","journal-title":"LNCS"},{"key":"23_CR14","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/BF00881951","volume":"13","author":"R. Pliu\u0161kevi\u010dius","year":"1994","unstructured":"R. Pliu\u0161kevi\u010dius: The saturated tableaux for linear miniscoped Horn-like temporal logic. Journal of Automated Reasoning 13, 51\u201367 (1994)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR15","unstructured":"R. Pliukevi\u010dius: On the replacement of induction for a first order linear temporal logic. Proc. of Second World Conf. on the Fund. of Artif. Intell. 1995, pp. 331\u2013342"},{"key":"23_CR16","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0304-3975(92)90067-P","volume":"95","author":"I. Sain","year":"1992","unstructured":"I. Sain: Temporal logics need their clocks. Theoret. Comput. Sci. 95, 75\u201395 (1992","journal-title":"Theoret. Comput. Sci."},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"J. Sakalauskait\u0117: A sequent calculus for a first order linear temporal logic with equality. LNCS 620, 430\u2013440","DOI":"10.1007\/BFb0023895"},{"key":"23_CR18","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0304-3975(87)90129-0","volume":"54","author":"A. Szalas","year":"1987","unstructured":"A. Szalas: A complete axiomatic characterization of first order temporal logic of linear time. Theoret. Comput. Sci. 54, 199\u2013214 (1987)","journal-title":"Theoret. Comput. Sci."},{"key":"23_CR19","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(88)90045-X","volume":"57","author":"A. Szalas","year":"1988","unstructured":"A. Szalas, L. Holenderski: Incompleteness of first-order logic with UNTIL. Theoret. Comput. Sci. 57, 317\u2013325 (1988)","journal-title":"Theoret. Comput. Sci."},{"key":"23_CR20","doi-asserted-by":"crossref","first-page":"943","DOI":"10.1080\/00207178608933645","volume":"44","author":"J.G. Thistle","year":"1986","unstructured":"J.G. Thistle, W.M. Wonham: Control problems in a temporal logic framework. Int. J. Control 44, 943\u2013976 (1986)","journal-title":"Int. J. Control"},{"key":"23_CR21","first-page":"119","volume":"28","author":"P. Wolper","year":"1985","unstructured":"P. Wolper: The tableaux method for temporal logic: an overview. Log. et anal. 28, 119\u2013136 (1985)","journal-title":"Log. et anal."}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61630-6_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:08:55Z","timestamp":1605629335000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61630-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616306","9783540706434"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-61630-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}