{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:13:09Z","timestamp":1725484389454},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441854"},{"type":"electronic","value":"9783540457510"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45751-8_16","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T22:42:07Z","timestamp":1179268927000},"page":"235-249","source":"Crossref","is-referenced-by-count":3,"title":["Algorithms for Guiding Clausal Temporal Resolution"],"prefix":"10.1007","author":[{"given":"M. Carmen Fern\u00e1ndez","family":"Gago","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/S0747-7171(89)80070-7","volume":"8","author":"M. Abadi","year":"1989","unstructured":"M. Abadi and Z. Manna. Temporal Logic Programming. Journal of Symbolic Computation, 8: 277\u2013295, 1989.","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"16_CR2","doi-asserted-by":"crossref","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":"16_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/BFb0047117","volume-title":"Proceedings of the 7th International Conference on Automated Deduction","author":"A. Cavalli","year":"1984","unstructured":"A. Cavalli and L. Farinas del Cerro. A Decision Method for Linear Temporal Logic. In R.E. Shostak, editor, Proceedings of the 7th International Conference on Automated Deduction, volume 170 of Lecture Notes in Computer Science, pages 113\u2013127. Springer-Verlag, 1984."},{"issue":"3","key":"16_CR4","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1006\/jcss.1995.1088","volume":"51","author":"J. Chomicki","year":"1995","unstructured":"J. Chomicki and D. Niwinski. On the Feasibility of Checking Temporal Integrity Constraints. Journal of Computer and System Sciences, 51(3):523\u2013535, December 1995.","journal-title":"Journal of Computer and System Sciences"},{"key":"16_CR5","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1023\/A:1018942108420","volume":"22","author":"C. Dixon","year":"1998","unstructured":"C. Dixon. Temporal Resolution using a Breadth-First Search Algorithm. Annals of Mathematics and Artificial Intelligence, 22:87\u2013115, 1998.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"C. Dixon and M. Fisher. The Set of Support Strategy in Temporal Resolution. In Proceedings of TIME-98 the Fifth International Workshop on Temporal Representation and Reasoning, Sanibel Island, Florida, May 1998. IEEE Computer Society Press.","DOI":"10.1109\/TIME.1998.674140"},{"key":"16_CR7","unstructured":"M.C. Fern\u00e1ndez-Gago. Efficient Control of Temporal Reasoning. Transfer Report, Manchester Metropolitan University, 2000."},{"key":"16_CR8","unstructured":"M. Fisher. A Resolution Method for Temporal Logic. In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI), pages 99\u2013104, Sydney, Australia, August 1991. Morgan Kaufman."},{"issue":"4","key":"16_CR9","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1093\/logcom\/7.4.429","volume":"7","author":"M. Fisher","year":"1997","unstructured":"M. Fisher. A Normal Form for Temporal Logic and its Application in Theorem-Proving and Execution. Journal of Logic and Computation, 7(4):429\u2013456, August 1997.","journal-title":"Journal of Logic and Computation"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"M. Fisher, C. Dixon, and M. Peim. Clausal Temporal Resolution. In Transactions on Computational Logic 2(1), January 2001.","DOI":"10.1145\/371282.371311"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. The Temporal Analysis of Fairness. In Proceedings of the 7th ACM Symposium on the Principles of Programming Languages, pages 163\u2013173, Las Vegas, Nevada, January 1980.","DOI":"10.1145\/567446.567462"},{"key":"16_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1992."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. A CM Journal, 12(1):23\u201341, January 1965.","DOI":"10.1145\/321250.321253"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A. P. Sistla","year":"1987","unstructured":"A. P. Sistla, M. Vardi, and P. Wolper. The Complementation Problem for Buchi Automata with Applications to Temporal Logic. Theoretical Computer Science, 49:217\u2013237, 1987.","journal-title":"Theoretical Computer Science"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"G. Venkatesh. A Decision Method for Temporal Logic based on Resolution. Lecture Notes in Computer Science, 206:272\u2013289, 1986.","DOI":"10.1007\/3-540-16042-6_15"},{"key":"16_CR16","unstructured":"P. Wolper. The Tableau Method for Temporal Logic: An overview. Logique et Analyse, 110-111:119\u2013136, June-Sept 1985."},{"key":"16_CR17","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, G. Robinson, and D. Carson. Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. ACM Journal, 12:536\u2013541, October 1965.","journal-title":"ACM Journal"}],"container-title":["Lecture Notes in Computer Science","KI 2002: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45751-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T20:54:35Z","timestamp":1556398475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45751-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441854","9783540457510"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45751-8_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}