{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:32:58Z","timestamp":1725485578805},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000105"},{"type":"electronic","value":"9783540360780"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36078-6_6","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T02:48:36Z","timestamp":1180666116000},"page":"86-101","source":"Crossref","is-referenced-by-count":5,"title":["Searching for Invariants Using Temporal Resolution"],"prefix":"10.1007","author":[{"given":"James","family":"Brotherston","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anatoli","family":"Degtyarev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexei","family":"Lisitsa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,10,24]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"E. B\u00f6rger, E. Gr\u00e4del, and Yu. Gurevich. The Classical Decision Problem. Springer, 1997.","DOI":"10.1007\/978-3-642-59207-2"},{"issue":"3","key":"6_CR2","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B. Beckert","year":"1995","unstructured":"B. Beckert and J. Posegga. leanTAP: Lean, Tableau-based Deduction. Journal of Automated Reasoning, Vol. 15, No. 3, pages 339\u2013358, 1995.","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"R. J. Boulton and K. Slind. Automatic derivation and application of induction schemes for mutually recursive functions. In Proc. of CL 2000, volume 1861 of LNAI, 2000.","DOI":"10.1007\/3-540-44957-4_42"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"A. Bundy. The use of explicit plans to guide inductive proofs. In Proc. of 9th International Conference on Automated Deduction Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012826"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"A. Bundy. The Automation OfProofBy Mathematical Induction. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1, pages 845\u2013912. Elsevier Science and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50015-1"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"J. Brotherston, A. Degtyarev, M. Fisher and A. Lisitsa. Searching for Invariants using Temporal Resolution. Technical Report ULCS-02-023, University of Liverpool, Department of Computer Science, 2002, http:\/\/www.csc.liv.ac.uk\/research\/techreports\/","DOI":"10.1007\/3-540-36078-6_6"},{"key":"6_CR7","unstructured":"A. Degtyarev and M. Fisher. Propositional temporal resolution revised. In Proc. of 7th UK Workshop on Automated Reasoning (ARW\u201900). London, U.K., June 2000."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and M. Fisher. Towards first-order temporal resolution. In Proccedings ofKI-2001, volume 2174 of LNAI, 2001.","DOI":"10.1007\/3-540-45422-5_3"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"A. Degtyarev, M. Fisher and A. Lisitsa. Equality and monodic first-order temporal logic. Studia Logica, Vol. 72, No. 2, 2002.","DOI":"10.1023\/A:1021352309671"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"A. Degtyarev, M. Fisher and B. Konev. Simplified clausal resolution procedure for propositional linear-time temporal logic. To appear in Proc. of TABLEAUX\u201902, 2002.","DOI":"10.1007\/3-540-45616-3_7"},{"key":"6_CR11","unstructured":"A. Degtyarev, M. Fisher, A. Lisitsa and R. Pliuskevicius. Simple decision procedures for non-monodic decidable fragments of FOLTL. In preparation, 2002."},{"key":"6_CR12","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":"6_CR13","doi-asserted-by":"crossref","unstructured":"M. Fisher. A normal 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":"6_CR14","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"},{"key":"6_CR15","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1002\/malq.19870330506","volume":"33","author":"H. Kawai","year":"1987","unstructured":"H. Kawai. Sequential Calculus for a First Order Infinitary Temporal Logic. Zeitschrift f\u00fcr Mathematische Logic and Grundlagen der Mathematik, 33:423\u2013432, 1987.","journal-title":"Zeitschrift f\u00fcr Mathematische Logic and Grundlagen der Mathematik"},{"key":"6_CR16","series-title":"Lect Notes Comput Sci","first-page":"240","volume-title":"Proccedings of CSL\u201988","author":"B. Paech","year":"1988","unstructured":"B. Paech. Gentzen Systems for Propositional Temporal Logics. Proccedings of CSL\u201988, volume 385 of LNCS, p. 240\u2013253. Springer Verlag, 1988."},{"key":"6_CR17","unstructured":"R. Pliuskevicius. A decidable deductive procedure for a restricted FTL. In Proc. of 7th UK Workshop on Automated Reasoning (ARW\u201900). London, U.K., June 2000."},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"J. Richardson, A. Smaill, and I. Green. System description: proof planning in higher-order logic with lambdaclam. In Proc. of CADE\u201915, volume 1421 of LNAI, 1998.","DOI":"10.1007\/BFb0054254"},{"key":"6_CR19","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":"6_CR20","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"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36078-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T15:18:14Z","timestamp":1556464694000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36078-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000105","9783540360780"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-36078-6_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}