{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:07:11Z","timestamp":1761620831043,"version":"3.43.0"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2002,11,1]],"date-time":"2002-11-01T00:00:00Z","timestamp":1036108800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,11,1]],"date-time":"2002-11-01T00:00:00Z","timestamp":1036108800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Studia Logica"],"published-print":{"date-parts":[[2002,11]]},"DOI":"10.1023\/a:1021352309671","type":"journal-article","created":{"date-parts":[[2003,3,20]],"date-time":"2003-03-20T20:22:32Z","timestamp":1048191752000},"page":"147-156","source":"Crossref","is-referenced-by-count":25,"title":["Equality and Monodic First-Order Temporal Logic"],"prefix":"10.1007","volume":"72","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[]},{"given":"Alexei","family":"Lisitsa","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5111628_CR1","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(89)90138-2","volume":"65","author":"M. Abadi","year":"1989","unstructured":"Abadi, M., 'The power of temporal proofs', Theoretical Computer Science 65:35-84, 1989.","journal-title":"Theoretical Computer Science"},{"key":"5111628_CR2","unstructured":"Andr\u00c9ka, H., J. Van Benthem, and I. N\u00c9meti, 'Modal languages and bounded fragments of predicate logic', Technical report, ILLC ML-96-03, 1996, 59 pages."},{"key":"5111628_CR3","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1023\/A:1004275029985","volume":"27","author":"H. Andr\u00c9ka","year":"1998","unstructured":"Andr\u00c9ka, H., J. Van Benthem, and I. N\u00c9meti, 'Modal languages and bounded fragments of predicate logic', Journal of Philosophical Logic 27:217-274, 1998.","journal-title":"Journal of Philosophical Logic"},{"key":"5111628_CR4","doi-asserted-by":"crossref","unstructured":"B\u00d6rger, E., E. Gr\u00c4del, and Yu. Gurevich, The Classical Decision Problem, Springer, 1997.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"5111628_CR5","unstructured":"Craig, W., 'Incompletability, with respect to validity in every finite nonempty domain, of first-order functional calculus', In Proceedings of the International Congress of Mathematicians, page 721, Cambridge, Mass., 1950."},{"key":"5111628_CR6","series-title":"Oxford Logic Guides","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537793.001.0001","volume-title":"Modal Logic","author":"A. V. Chagrov","year":"1997","unstructured":"Chagrov, A. V., and M. V. Zakharyaschev, Modal Logic, Oxford Logic Guides 35, Clarendon Press, Oxford, 1997."},{"key":"5111628_CR7","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, 1997.","DOI":"10.1093\/logcom\/7.4.429"},{"key":"5111628_CR8","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., and H. De Nivelle, 'A superposition decision procedure for the guarded fragment with equality', In Proceedings of LICS-99, 1999, pp. 295-303.","DOI":"10.1109\/LICS.1999.782624"},{"key":"5111628_CR9","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., C. Meyer, and M. Veanes, 'The two-variable guarded fragment with transitive relations', In Proceedings of LICS-99, 1999, pp. 24-34.","DOI":"10.1109\/LICS.1999.782582"},{"key":"5111628_CR10","doi-asserted-by":"crossref","first-page":"1719","DOI":"10.2307\/2586808","volume":"4","author":"E. Gr\u00c4del","year":"1999","unstructured":"Gr\u00c4del, E., 'The restraining power of guards', Journal of Symbolic Logic 4:1719-1742, 1999.","journal-title":"Journal of Symbolic Logic"},{"key":"5111628_CR11","doi-asserted-by":"crossref","unstructured":"H\u00dcttel, H., 'Undecidable equivalence for basic parallel processes', In Proceedings of TACS-94, Lecture Notes in Computer Science 789, Springer-Verlag, 1994, pp. 454-464.","DOI":"10.1007\/3-540-57887-0_110"},{"key":"5111628_CR12","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","volume":"106","author":"I. Hodkinson","year":"2000","unstructured":"Hodkinson, I., F. Wolter, and M. Zakharyaschev, 'Fragments of first-order temporal logics', Annals of Pure and Applied logic 106:85-134, 2000.","journal-title":"Annals of Pure and Applied logic"},{"key":"5111628_CR13","unstructured":"Hodkinson, I., 'Monodic packed fragment with equality is decidable', Studia Logica (this volume)."},{"key":"5111628_CR14","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', Zeitschrift f\u00fcr Mathematische Logic and Grundlagen der Mathematik 33:423-432, 1987.","journal-title":"Zeitschrift f\u00fcr Mathematische Logic and Grundlagen der Mathematik"},{"key":"5111628_CR15","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0020-0190(94)00188-5","volume":"53","author":"G. Kucherov","year":"1995","unstructured":"Kucherov, G., and M. Rusinowitch, 'Undecidability of ground reducibility for word rewriting systems with variables', Information Processing Letters 53:209-215, 1995.","journal-title":"Information Processing Letters"},{"key":"5111628_CR16","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1080\/11663081.1992.10510779","volume":"2","author":"S. Merz","year":"1992","unstructured":"Merz, S., 'Decidability and incompleteness results for first-order temporal logic of linear time', Journal of Applied Non-Classical Logics 2:139-156, 1992.","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"5111628_CR17","doi-asserted-by":"crossref","first-page":"437","DOI":"10.2307\/1970290","volume":"74","author":"M. L. Minsky","year":"1961","unstructured":"Minsky, M. L., 'Recursive unsolvability of Post's problem of \u201ctag\u201d and other topics in theory of Turing machines', Annals of Mathematics 74:437-455, 1961.","journal-title":"Annals of Mathematics"},{"key":"5111628_CR18","unstructured":"Minsky, M. L., Computation: Finite and Infinite Machines, Prentice-Hall International, 1967."},{"key":"5111628_CR19","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0304-3975(88)90045-X","volume":"57","author":"A. Szalas","year":"1988","unstructured":"Szalas, A., and L. Holenderski, 'Incompleteness of first-order logic with until', Theoretical Computer Science 57:317-325, 1988.","journal-title":"Theoretical Computer Science"},{"key":"5111628_CR20","doi-asserted-by":"crossref","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 Computer Science 47:329-334, 1986.","journal-title":"Theoretical Computer Science"},{"key":"5111628_CR21","doi-asserted-by":"crossref","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 Computer Science 54:199-214, 1987.","journal-title":"Theoretical Computer Science"},{"key":"5111628_CR22","first-page":"1","volume-title":"Time and Logic. A Computational Approach","author":"A. Szalas","year":"1995","unstructured":"Szalas, A., 'Temporal logic: a standard approach', In Time and Logic. A Computational Approach, UCL Press Ltd., London, 1995, pp. 1-50."},{"key":"5111628_CR23","first-page":"596","volume":"70","author":"B. A. Trakhtenbrot","year":"1950","unstructured":"Trakhtenbrot, B. A., 'The impossibility of an algorithm for the decision problem for finite models', Dokl. Akad. Nauk SSSR 70:596-572, 1950, English translation in: AMS Transl. Ser. 2, 23(1063):1\u20136.","journal-title":"Dokl. Akad. Nauk SSSR"},{"key":"5111628_CR24","doi-asserted-by":"crossref","first-page":"39","DOI":"10.2307\/2964336","volume":"25","author":"R. Vaught","year":"1960","unstructured":"Vaught, R., 'Sentences true in all constructive models', Journal of Symbolic Logic 25:39-58, 1960.","journal-title":"Journal of Symbolic Logic"},{"key":"5111628_CR25","unstructured":"Wolter, F., and M. Zakharyaschev, 'Axiomatizing the monodic fragment of first-order temporal logic', Annals of Pure and Applied logic, to appear."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021352309671.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021352309671\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021352309671.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:22:31Z","timestamp":1754630551000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021352309671"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,11]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,11]]}},"alternative-id":["5111628"],"URL":"https:\/\/doi.org\/10.1023\/a:1021352309671","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2002,11]]}}}