{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:09Z","timestamp":1747546929817},"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_22","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:08:48Z","timestamp":1330294128000},"page":"303-319","source":"Crossref","is-referenced-by-count":4,"title":["Temporal reasoning over linear discrete time"],"prefix":"10.1007","author":[{"given":"Manuel","family":"Enciso","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Inma P.","family":"Guzm\u00e1n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlos","family":"Rossi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"22_CR1","unstructured":"A. Artosi and G. Governatori. Labeled model modal logic. In CADE12 Workshop on Automated Model Building. Springer-Verlag. LNAI, 1994. 838"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"M. Abadi and Z. Manna. Modal theorem proving. In Springer-Verlag, editor, 8th Int. Conf. on Automated Deduction. Lecture Notes in Computer Science, 1986.","DOI":"10.21236\/ADA325959"},{"issue":"2","key":"22_CR3","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/77600.77617","volume":"37","author":"M. Abadi","year":"1990","unstructured":"M. Abadi and Z. Manna. Nonclausal deduction in first-order temporal logic. ACM Journal, 37(2):279\u2013317, April 1990.","journal-title":"ACM Journal"},{"key":"22_CR4","unstructured":"G. Aguilera, I.P. de Guzm\u00e1n and M. Ojeda. Automated model building via syntactic trees transformations. In Proceedings of CADE-12 Workshop on Automated Model Building, pages 4\u201310, Nancy, France. June 1994."},{"key":"22_CR5","first-page":"198","volume":"838","author":"G. Aguilera","year":"1994","unstructured":"G. Aguilera, I.P. de Guzm\u00e1n and M. Ojeda. TAS-D++ syntactic trees transformations for automated theorem proving. Lectures Notes in Artifial Intelligence n. 838, pages 198\u2013216. Sept 1994.","journal-title":"Lectures Notes in Artifial Intelligence"},{"issue":"1","key":"22_CR6","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1080\/11663081.1995.10510841","volume":"5","author":"G. Aguilera","year":"1995","unstructured":"G. Aguilera, I.P. de Guzm\u00e1n and M. Ojeda. Increasing the efficiency of automated theorem proving. Journal of Applied non-Classical logics 5 (1):9\u201329. 1995.","journal-title":"Journal of Applied non-Classical logics"},{"key":"22_CR7","volume-title":"Parallel temporal resolution","author":"C. Dixon","year":"1995","unstructured":"C. Dixon, M. Fisher, and R. Johnson. Parallel temporal resolution. In International Workshop on Temporal Representation and Reasoning TIME'95, Melbourne. Florida. EEUU, 1995."},{"key":"22_CR8","volume-title":"PhD thesis","author":"M. Enciso","year":"1995","unstructured":"M. Enciso. Demostraci\u00f3n Autom\u00e1tica de Teoremas: Eficiencia y Paralelismo. PhD thesis, Universidad de M\u00e1laga. Espa\u00f1a, 1995."},{"key":"22_CR9","unstructured":"M. Enciso and I.P. de Guzm\u00e1n. A new and complete Theorem Prover for Temporal Logic. In In Proceedings of IJCAI-95 Workshop on Executable Temporal Logics. Montreal, Canada. Aug. 1995."},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"M. Fitting. Destructive modal resolution. Journal of Logic and Computation, 1(1), 1990.","DOI":"10.1093\/logcom\/1.1.83"},{"key":"22_CR11","unstructured":"A. Galton, editor. Temporal Logic and Their Applications. Academic Press, 1987."},{"key":"22_CR12","unstructured":"L. Fari\u00f1as del Cerro and A. Herzig. Modal Deduction with applications in Epistemic and Temporal Logics. Springer Verlag, 1991."},{"key":"22_CR13","unstructured":"M. Fisher. A resolution method for temporal logic. In 12th International Joint Conference on Artificial Intelligence (IJCAI), Sydney. Australia, 1991."},{"key":"22_CR14","volume-title":"LNAI. 918","author":"G. Governatori","year":"1995","unstructured":"G. Governatori. Labeled tableaux for multimodal logics. In 4th Workshop on Theorem Proving, Analytic Tableaux and Related Methods, Berlin. German, 1995. Springer-Verlag. LNAI. 918"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"R. Hahnle. Automated Deduction in Multiple-valued Logics. Oxford University Press, 1993.","DOI":"10.1093\/oso\/9780198539896.001.0001"},{"key":"22_CR16","volume-title":"LNAI","author":"R. Hahnle","year":"1994","unstructured":"R. Hahnle and O. Ibens. Improving temporal logic tableaux using integer constraints. In 1st International Conference on Temporal Logic. Springer-Verlag. LNAI., Munich. German, 1994. Vol. 827"},{"key":"22_CR17","unstructured":"R. Johnson. A blackboard approach to parallel temporal tableaux. In Artificial Intelligence Methodologies, Systems and Applications (AIMSA). World Scientific, 1994."},{"key":"22_CR18","volume-title":"PhD thesis","author":"A. Massini","year":"1993","unstructured":"A. Massini. A Proof Theory of Modalities for Computer Science. PhD thesis, Universita di Pisa-Genova-Udine, Italy, 1993."},{"key":"22_CR19","unstructured":"A. Ramsay. Formal Methods in Artificial Intelligence. Cambridge University Press, 1988."},{"key":"22_CR20","volume-title":"PhD thesis","author":"F. Sanz","year":"1992","unstructured":"F. Sanz. Hacia una alternativa a resoluci\u00f3n. PhD thesis, Universidad de M\u00e1laga, Spain, 1992."},{"key":"22_CR21","volume-title":"Automated proof search in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics","author":"L. A. Wallen","year":"1990","unstructured":"L. A. Wallen. Automated proof search in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics. The MIT Press, Cambridge, Massachusetts, 1990."}],"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_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:39:49Z","timestamp":1713634789000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61630-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616306","9783540706434"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-61630-6_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}