{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:58:20Z","timestamp":1725487100048},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540426127"},{"type":"electronic","value":"9783540454229"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45422-5_3","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T15:01:34Z","timestamp":1183561294000},"page":"18-32","source":"Crossref","is-referenced-by-count":7,"title":["Towards First-Order Temporal Resolution"],"prefix":"10.1007","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,9,3]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"S. Abiteboul, V. Vianu, B. Fordham, and Y. Yesha. Relational transducers for electronic commerce. In Proceedings of 17th Symposium on Database Systems (PODS\u20191998), pages 179\u2013187. ACM Press, 2000.","DOI":"10.1006\/jcss.2000.1708"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. Resolution theorem proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1, pages 19\u2013100. Elsevier Science and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"E. B\u00f6rger, E. Gr\u00f4del, and Yu. Gurevich. The Classical Decision Problem. Springer Verlag, 1997.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"3_CR4","unstructured":"A. Degtyarev and M. Fisher. Propositional temporal resolution revised. In H.J. Ohlbach, editor, Proc. of 7th UK Workshop on Automated Reasoning (ARW\u201900), London, U.K., June 2000."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"M. Fisher, C. Dixon, and M. Peim. Clausal temporal resolution. ACM Transactions on Computation Logic, 2(1), January 2001.","DOI":"10.1145\/371282.371311"},{"key":"3_CR6","unstructured":"M. Fisher. A resolution method for temporal logic. In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI\u201991), 1991."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"M. Fisher. A normal form for first-order temporal formulae. In D. Kapur, editor, 11 th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, Saratoga Springs, USA, 1992. Springer Verlag.","DOI":"10.1007\/3-540-55602-8_178"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"M. Fisher. Anormal form for temporal logics and its applications in theorem-proving and execution. Journal of Logic and Computation, 7(4), 1997.","DOI":"10.1093\/logcom\/7.4.429"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"C.G. Ferm\u00fcller, A. Leitsch, U. Hustadt, and T. Tammet. Resolution decision procedures. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 2, pages 1791\u20131852. Elsevier Science and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50027-8"},{"key":"3_CR10","series-title":"Lect Notes Comput Sci","first-page":"402","volume-title":"Proceedings on Colloquium on Temporal Logic and Specification","author":"D. Gabbay","year":"1987","unstructured":"D. Gabbay. Declarative past and imperative future:executive temporal logic for interactive systems. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proceedings on Colloquium on Temporal Logic and Specification, volume 398 of Lecture Notes in Computer Science, pages 402\u2013450, Altrincham, U.K., 1987. Springer Verlag."},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","volume":"106","author":"I. Hodkinson","year":"2000","unstructured":"I. Hodkinson, F. Wolter, and M. Zakharyaschev. Fragments of first-order temporal logics. Annals of Pure and Applied logic, 106:85\u2013134, 2000.","journal-title":"Annals of Pure and Applied logic"},{"issue":"3","key":"3_CR12","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"D.A. Plaisted and S.A. Greenbaum. A structure-preserving clause form transformation. Journal of Symbolic Computation, 2(3):293\u2013304, September 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"M. Spielmann. Verification of relational transducers for electronic commerce. In Proceedings of 19th Symposium on Database Systems (PODS\u20192000), pages 92\u2013103, Dallas, Texas, 2000. ACM Press.","DOI":"10.1145\/335168.335212"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(86)90157-X","volume":"47","author":"A. Szalas","year":"1986","unstructured":"A. Szalas. Concerning the semantic consequence relation in first-order temporal logic. Theoretical Computer Science, 47:329\u2013334, 1986.","journal-title":"Theoretical Computer Science"},{"key":"3_CR15","unstructured":"P. Wolper. Syshthesis of Communicating Processes from Temporal Logic Specifications. Ph.d. dissertation, Stanford University, 1982."},{"key":"3_CR16","unstructured":"M. Wolter, F. and. Z Akharyaschev. Spatio-temporal representation and reasoning based on RCC-8. In Proceedings of the 7th Conference on Principles of Knowledge Representation and Reasoning (KR\u20192000), pages 3\u201314, Montreal, Canada, 2000."},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"F. Wolter and M. Zakharyaschev. Axiomatizing the monodic fragment of first-order temporal logic. To appear in Annals of Pure and Applied logic., 2001.","DOI":"10.1016\/S0168-0072(01)00124-5"},{"issue":"5","key":"3_CR18","first-page":"1046","volume":"293","author":"_. N. Zamov","year":"1987","unstructured":"]_ N. Zamov. The resolution method without skolemization. Soviet Mathematical Doklady, 293(5):1046\u20131049, 1987.","journal-title":"Soviet Mathematical Doklady"}],"container-title":["Lecture Notes in Computer Science","KI 2001: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45422-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T03:02:44Z","timestamp":1556593364000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45422-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540426127","9783540454229"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45422-5_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}