{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T09:18:16Z","timestamp":1768555096572,"version":"3.49.0"},"reference-count":47,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2000,12,1]],"date-time":"2000-12-01T00:00:00Z","timestamp":975628800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4611,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2000,12]]},"DOI":"10.1016\/s0168-0072(00)00018-x","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T12:56:30Z","timestamp":1027601790000},"page":"85-134","source":"Crossref","is-referenced-by-count":129,"title":["Decidable fragments of first-order temporal logics"],"prefix":"10.1016","volume":"106","author":[{"given":"Ian","family":"Hodkinson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Wolter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Zakharyaschev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0168-0072(00)00018-X_BIB1","unstructured":"M. Abadi, The power of temporal proofs, Proc. Symp. on Logic in Computer Science, Ithaca, June 1987, pp. 176\u2013186."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB2","series-title":"Recent Advances in Temporal Databases","first-page":"43","article-title":"Temporal connectives versus explicit timestamps in temporal query languages","author":"Abiteboul","year":"1995"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB3","doi-asserted-by":"crossref","unstructured":"S. Abiteboul, L. Herr, J. van den Bussche, Temporal versus first-order logic in query temporal databases, ACM Symp. on Principles of Database Systems, Montreal, Canada, 1996, pp. 49\u201357.","DOI":"10.1145\/237661.237674"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB4","doi-asserted-by":"crossref","unstructured":"H. Andr\u00e9ka, I. N\u00e9meti, I. Sain, Completeness problems in verification of programs and program schemes, Mathematical Foundations of Computer Science 1979, Lecture Notes in Computer Science, Springer, Berlin, 1979.","DOI":"10.1007\/3-540-09526-8_17"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB5","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1023\/A:1004275029985","article-title":"Modal languages and bounded fragments of predicate logic","volume":"27","author":"Andr\u00e9ka","year":"1998","journal-title":"J. Philos. Logic"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB6","doi-asserted-by":"crossref","unstructured":"A. Artale, E. Franconi, A computational account for a description logic of time and action, Proc. 4th Conf. on Principles of Knowledge Representation and Reasoning, Montreal, Canada, Morgan Kaufman, Los Altos, CA, 1994, pp. 3\u201314.","DOI":"10.1016\/B978-1-4832-1452-8.50098-1"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB7","unstructured":"A. Artale, E. Franconi, Temporal description logics, in: L. Vila, P. van Beek, M. Boddy, M. Fisher, D. Gabbay, A. Galton, R. Morris (Eds.), Handbook of Time and Temporal Reasoning in Artificial Intelligence, MIT Press, Cambridge, MA, 1999, to appear."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB8","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1080\/11663081.1995.10510854","article-title":"A multi-dimensional terminological knowledge representation language","volume":"5","author":"Baader","year":"1995","journal-title":"J. Appl. Non-Classical Logic"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB9","series-title":"The Classical Decision Problem","author":"B\u00f6rger","year":"1997"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB10","unstructured":"J.R. B\u00fcchi. On a decision method in restricted second-order arithmetic, Logic, Methodology and Philosophy of Science: Proc. 1960 Int. Congress, Stanford University Press, Stanford, CA, 1962, pp. 1\u201311."},{"issue":"2","key":"10.1016\/S0168-0072(00)00018-X_BIB11","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1305\/ndjfl\/1093870820","article-title":"The decision problem for linear temporal logic","volume":"26","author":"Burgess","year":"1985","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB12","doi-asserted-by":"crossref","unstructured":"J. Chomicki, Temporal query languages: a survey, in: D. Gabbay, H.J. Ohlbach (Eds.), Temporal Logic, 1st Int. Conf., Springer, Berlin, Lecture Notes in Artificial Intelligence, Vol. 827, 1994, pp. 506\u2013534.","DOI":"10.1007\/BFb0014006"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB13","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1006\/jcss.1995.1088","article-title":"On the feasibility of checking temporal integrity constraints","volume":"51","author":"Chomicki","year":"1995","journal-title":"J. Comput. Systems Sci."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB14","series-title":"Handbook of Theoretical Computer Science","first-page":"996","article-title":"Temporal and modal logic","author":"Emerson","year":"1990"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB15","series-title":"Reasoning about Knowledge","author":"Fagin","year":"1995"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB16","series-title":"Temporal Logic. Part I","author":"Gabbay","year":"1994"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB17","unstructured":"D. Gabbay, M. Reynolds, M. Finger, Temporal Logic. Part II, Clarendon Press, Oxford, to appear."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB18","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1093\/jigpal\/6.1.73","article-title":"Products of modal logics, Part I","volume":"6","author":"Gabbay","year":"1998","journal-title":"J. IGPL"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB19","first-page":"249","article-title":"Quantification in modal logic","volume":"Vol. 2","author":"Garson","year":"1984"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB20","unstructured":"G. De Giacomo, M. Lenzerini, TBox and ABox reasoning in expressive description logics, Proc. 5th Conference on Principles of Knowledge Representation and Reasoning, Montreal, Canada, Morgan Kaufman, Los Altos, CA, 1996, pp. 316\u2013327."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB21","doi-asserted-by":"crossref","first-page":"1719","DOI":"10.2307\/2586808","article-title":"On the restraining power of guards","volume":"64","author":"Gr\u00e4del","year":"1999","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB22","unstructured":"Y. Gurevich, Elementary properties of ordered abelian groups, Algebra and Logic 3 (1964) 5\u201339. (Russian; an English version is in Trans. Amer. Math. Soc. 46 (1965) 165\u2013192)."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB23","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/0003-4843(77)90014-6","article-title":"Expanded theory of ordered abelian groups","volume":"12","author":"Gurevich","year":"1977","journal-title":"Ann. Math. Logic"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB24","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1145\/4904.4993","article-title":"Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness","volume":"33","author":"Harel","year":"1986","journal-title":"J. ACM"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB25","unstructured":"W. Hodges, Model Theory, Encyclopedia of Mathematics and its Applications, Vol. 42, Cambridge University Press, Cambdrige, U.K., 1993."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB26","unstructured":"H. Kamp, Tense logic and the theory of linear order, Ph.D. Thesis, University of California, Los Angeles, 1968."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB27","first-page":"237","article-title":"Formal properties of \u201cnow\u201d","volume":"37","author":"Kamp","year":"1971","journal-title":"Theoria"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB28","doi-asserted-by":"crossref","first-page":"109","DOI":"10.4064\/fm-59-1-109-116","article-title":"On the elementary theory of linear order","volume":"59","author":"L\u00e4uchli","year":"1966","journal-title":"Fund. Math."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB29","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/BF01458217","article-title":"\u00dcber M\u00f6glichkeiten im Relativkalk\u00fcl","volume":"76","author":"L\u00f6wenheim","year":"1915","journal-title":"Math. Ann."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB30","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","year":"1992"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB31","series-title":"Temporal Verification of Reactive Systems: Safety","author":"Manna","year":"1995"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB32","doi-asserted-by":"crossref","unstructured":"S. Merz, Decidability and incompleteness results for first-order temporal logics of linear time, J. Appl. Non-Classical Logic 2 (1992).","DOI":"10.1080\/11663081.1992.10510779"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB33","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1002\/malq.19750210118","article-title":"On languages with two variables","volume":"21","author":"Mortimer","year":"1975","journal-title":"Z. Math. Logik Grundlagen Math."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB34","doi-asserted-by":"crossref","unstructured":"A. Pnueli, Applications of temporal logic to the specification and verification of reactive systems, a survey of current trends, in Current Trends in Concurrency, Lecture Notes in Computer Science, Springer, Berlin, 1986, pp. 510\u2013584.","DOI":"10.1007\/BFb0027047"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB35","first-page":"1","article-title":"Decidability of second order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Trans. Amer. Math. Soc."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB36","series-title":"Handbook of Mathematical Logic","first-page":"595","article-title":"Decidable theories","author":"Rabin","year":"1977"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB37","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","article-title":"On a problem of formal logic","volume":"30","author":"Ramsey","year":"1930","journal-title":"Proc. London Math. Soc."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB38","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/BF00370836","article-title":"Axiomatising first-order temporal logic: until and since over linear time","volume":"57","author":"Reynolds","year":"1996","journal-title":"Studia Logica"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB39","series-title":"Linear Orderings","author":"Rosenstein","year":"1982"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB40","doi-asserted-by":"crossref","unstructured":"K. Schild, Combining terminological logics with tense logic, Proc. 6th Portuguese Conf. on Artificial Intelligence, Porto, 1993, pp. 105\u2013120.","DOI":"10.1007\/3-540-57287-2_41"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB41","first-page":"477","article-title":"A decision method for validity of sentences in two variables","volume":"27","author":"Scott","year":"1962","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB42","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/0306-4379(80)90009-5","article-title":"Temporal aspect of logical procedure definition","volume":"5","author":"Sernadas","year":"1980","journal-title":"Inform. Systems"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB43","first-page":"478","article-title":"Modal and temporal logics","volume":"Vol. 2","author":"Stirling","year":"1992"},{"key":"10.1016\/S0168-0072(00)00018-X_BIB44","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/0304-3975(86)90157-X","article-title":"Concerning the semantic consequence relation in first-order temporal logic","volume":"47","author":"Szalas","year":"1986","journal-title":"J. Theoret. Comput. Sci."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB45","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0304-3975(88)90045-X","article-title":"Incompleteness of first-order temporal logic with Until","volume":"57","author":"Szalas","year":"1988","journal-title":"J. Theoret. Comput. Sci."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB46","unstructured":"F. Wolter, M. Zakharyaschev, Temporalizing description logics, Proc. FroCoS\u201998, Amsterdam, 1998. in \u2018Frontiers of Combining Systems\u2019, Kluwer Academic Publishers, Dordrecht, 2000, to appear. See http:\/\/www.informatik.uni-leipzig.de\/\u223cwolter."},{"key":"10.1016\/S0168-0072(00)00018-X_BIB47","unstructured":"F. Wolter, M. Zakharyaschev, Decidable fragments of first-order modal logics, Submitted. See http:\/\/www.informatik.uni-leipzig.de\/\u223cwolter, 1999."}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S016800720000018X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S016800720000018X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,12]],"date-time":"2020-01-12T04:37:23Z","timestamp":1578803843000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S016800720000018X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,12]]},"references-count":47,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2000,12]]}},"alternative-id":["S016800720000018X"],"URL":"https:\/\/doi.org\/10.1016\/s0168-0072(00)00018-x","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2000,12]]}}}