{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:09:37Z","timestamp":1763467777568},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_26","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T00:43:15Z","timestamp":1167439395000},"page":"324-340","source":"Crossref","is-referenced-by-count":15,"title":["The Mosaic Method for Temporal Logics"],"prefix":"10.1007","author":[{"given":"Maarten","family":"Marx","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Szabolcs","family":"Mikul\u00e1s","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Reynolds","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","volume-title":"Proceedings of the thirteenth ACM symposium on the principles of Programming Languages","author":"H. Barringer","year":"1986","unstructured":"Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: Proceedings of the thirteenth ACM symposium on the principles of Programming Languages, St. Petersberg Beach, Florida. ACM, New York (January 1986)"},{"issue":"2","key":"26_CR2","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1305\/ndjfl\/1093870820","volume":"26","author":"J.P. Burgess","year":"1985","unstructured":"Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic. Notre Dame J. Formal Logic\u00a026(2), 115\u2013128 (1985)","journal-title":"Notre Dame J. Formal Logic"},{"key":"26_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof methods for modal and intuitionistic logics","author":"M. Fitting","year":"1983","unstructured":"Fitting, M.: Proof methods for modal and intuitionistic logics. Reidel, Dordrechtz (1983)"},{"key":"26_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0013976","volume-title":"Temporal Logic: Mathematical Foundations and Computational Aspects","author":"D. Gabbay","year":"1994","unstructured":"Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects, vol.\u00a01. Oxford University Press, Oxford (1994)"},{"key":"26_CR5","series-title":"CSLI. Lecture Notes","volume-title":"Logics of Time and Computation","author":"R. Goldblatt","year":"1987","unstructured":"Goldblatt, R.: Logics of Time and Computation. In: CSLI. Lecture Notes, vol.\u00a07. The Chicago University Press, Chicago (1987)"},{"key":"26_CR6","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/BF01057938","volume":"53","author":"R. Gor\u00e9","year":"1994","unstructured":"Gor\u00e9, R.: Cut-free sequent and tableau systems for propositional Diodorean modal logics. Studia Logica\u00a053, 433\u2013457 (1994)","journal-title":"Studia Logica"},{"key":"26_CR7","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-94-017-1754-0_6","volume-title":"Handbook of Tableau Methods","author":"R. Gor\u00e9","year":"1999","unstructured":"Gor\u00e9, R.: Tableau methods for modal and temporal logics. In: D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 297\u2013396. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"26_CR8","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/3-540-61208-4_14","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"A. Heuerding","year":"1996","unstructured":"Heuerding, A., Seyfried, M., Zimmermann, H.: Efficient loop-check for backward proof search in some non-classical logics. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS (LNAI), vol.\u00a01071, pp. 210\u2013225. Springer, Heidelberg (1996)"},{"key":"26_CR9","series-title":"Studies in Fuzziness and Soft Computing","first-page":"158","volume-title":"Logic at Work. Essays Dedicated to the Memory of Helena Rasiowa","author":"R. Hirsch","year":"1999","unstructured":"Hirsch, R., Hodkinson, I., Marx, M., Mikul\u00e1s, S., Reynolds, M.: Mosaics and step-by-step. Remarks on A modal logic of relations. In: Orlowska, E. (ed.) Logic at Work. Essays Dedicated to the Memory of Helena Rasiowa. Studies in Fuzziness and Soft Computing, vol.\u00a024, pp. 158\u2013167. Springer, Heidelberg (1999)"},{"key":"26_CR10","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/BF01053026","volume":"53","author":"R. Kashima","year":"1994","unstructured":"Kashima, R.: Cut-free sequent calculi for some tense logics. Studia Logica\u00a053, 119\u2013135 (1994)","journal-title":"Studia Logica"},{"key":"26_CR11","unstructured":"Kamp, H.: Tense logic and the theory of linear order. PhD thesis. University of California, Los Angeles (1968)"},{"issue":"2","key":"26_CR12","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1093\/jigpal\/6.2.305","volume":"6","author":"S. Mikul\u00e1s","year":"1998","unstructured":"Mikul\u00e1s, S.: Taming first-order logic. Journal of the IGPL\u00a06(2), 305\u2013316 (1998)","journal-title":"Journal of the IGPL"},{"key":"26_CR13","unstructured":"N\u00e9meti, I.: Free Algebras and Decidability in Algebraic Logic. PhD thesis, Hungarian Academy of Sciences, Budapest (1986) (in Hungarian)"},{"key":"26_CR14","first-page":"171","volume-title":"Logic Colloquium 1992","author":"I. N\u00e9meti","year":"1995","unstructured":"N\u00e9meti, I.: Decidable versions of first order logic and cylindric-relativized set algebras. In: Csirmaz, L., Gabbay, D., de Rijke, M. (eds.) Logic Colloquium 1992, pp. 171\u2013241. CSLI Publications, Stanford (1995)"},{"key":"26_CR15","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF00713542","volume":"39","author":"H. Ono","year":"1980","unstructured":"Ono, H., Nakamura, A.: On the size of refutation Kripke models for some linear modal and tense logics. Studia Logica\u00a039, 325\u2013333 (1980)","journal-title":"Studia Logica"},{"key":"26_CR16","unstructured":"Reynolds, M.: The complexity of the temporal logic over the reals, submitted Version available at \n                    \n                      http:\/\/www.it.murdoch.edu.au\/~mark\/research\/online"},{"key":"26_CR17","unstructured":"Reynolds, M.: The complexity of the temporal logic with until over general linear time (submitted)"},{"key":"26_CR18","unstructured":"M. Reynolds. Online theorem-prover at \n                    \n                      http:\/\/www.it.murdoch.edu.au\/~mark\/research\/online\/demos\/tempmos\/TempMosApplet.html"},{"key":"26_CR19","series-title":"Lecture Notes in A.I","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035385","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.H. Schmitt","year":"1997","unstructured":"Schmitt, P.H., Goubault-Larrecq, J.: A tableau system for linear-time temporal logic. In: Brinksma, E. (ed.) TACAS 1997. Lecture Notes in A.I, vol.\u00a01217 Springer, Heidelberg (1997)"},{"key":"26_CR20","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. Sistla","year":"1985","unstructured":"Sistla, A., Clarke, E.: Complexity of propositional linear temporal logics. J. ACM\u00a032, 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"26_CR21","volume-title":"Logic at Work","author":"Y. Venema","year":"1999","unstructured":"Venema, Y., Marx, M.: A modal logic of relations. In: Orlowska, E. (ed.) Logic at Work. Springer, Heidelberg (1999)"},{"issue":"110-111","key":"26_CR22","first-page":"119","volume":"28","author":"P. Wolper","year":"1985","unstructured":"Wolper, P.: The tableau method for temporal logic: an overview. Logique et Analyse (N.S.)\u00a028 numbers (110-111), 119\u2013136 (1985)","journal-title":"Logique et Analyse, (N.S.)"},{"key":"26_CR23","unstructured":"Zimmermann, H.: A Directed Tree Calculus for Minimal Tense Logic. Master\u2019s Thesis, Institute for Applied Mathematics and Computer Science, University of Bern, Switzerland (1995)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T23:32:02Z","timestamp":1558308722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/10722086_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}