{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T21:51:32Z","timestamp":1778277092514,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540405597","type":"print"},{"value":"9783540450856","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_21","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T09:13:30Z","timestamp":1288084410000},"page":"274-278","source":"Crossref","is-referenced-by-count":30,"title":["TRP++ 2.0: A Temporal Resolution Prover"],"prefix":"10.1007","author":[{"given":"Ullrich","family":"Hustadt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boris","family":"Konev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Bentley, J., Sedgewick, R.: Fast algorithms for sorting and searching strings. In: SODA: ACM-SIAM Symposium on Discrete Algorithms (1997)"},{"key":"21_CR2","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"673","DOI":"10.1007\/3-540-61511-3_121","volume-title":"Automated Deduction - Cade-13","author":"C. Dixon","year":"1996","unstructured":"Dixon, C.: Search strategies for resolution in temporal logics. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 673\u2013687. Springer, Heidelberg (1996)"},{"key":"21_CR3","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-94-015-9586-5_8","volume-title":"Advances in Temporal Logic","author":"C. Dixon","year":"2000","unstructured":"Dixon, C.: Using Otter for temporal resolution. In: Advances in Temporal Logic, pp. 149\u2013166. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"21_CR4","first-page":"997","volume-title":"Handbook of Theoretical Computer Science, ch. 16","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, ch. 16, pp. 997\u20131072. Elsevier, Amsterdam (1990)"},{"key":"21_CR5","first-page":"99","volume-title":"Proc. IJCAI 1991","author":"M. Fisher","year":"1991","unstructured":"Fisher, M.: A resolution method for temporal logic. In: Proc. IJCAI 1991, pp. 99\u2013104. Morgan Kaufmann, San Francisco (1991)"},{"issue":"1","key":"21_CR6","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M. Fisher","year":"2001","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Transactions on Computational Logic\u00a02(1), 12\u201356 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0020439","volume-title":"Distributed Algorithms","author":"J.-H. Hoepman","year":"1994","unstructured":"Hoepman, J.-H.: Uniform deterministic self-stabilizing ring-orientation on oddlength rings. In: Tel, G., Vit\u00e1nyi, P.M.B. (eds.) WDAG 1994. LNCS, vol.\u00a0857, pp. 265\u2013279. Springer, Heidelberg (1994)"},{"issue":"5","key":"21_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker Spin. IEEE Trans. on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"21_CR9","unstructured":"Hustadt, U., Konev, B.: TRP++: A temporal resolution prover. In: Proc. WIL 2002 (2002), Available as \n                    \n                      http:\/\/www.lsi.upc.es\/~roberto\/wilproceedings.html"},{"key":"21_CR10","first-page":"533","volume-title":"Proc. KR 2002","author":"U. Hustadt","year":"2002","unstructured":"Hustadt, U., Schmidt, R.A.: Scientific benchmarking with temporal logic decision procedures. In: Proc. KR 2002, pp. 533\u2013544. Morgan Kaufmann, San Francisco (2002)"},{"key":"21_CR11","volume-title":"The Art of Computer Programming: Sorting and Searching","author":"D.E. Knuth","year":"1973","unstructured":"Knuth, D.E.: The Art of Computer Programming: Sorting and Searching, vol.\u00a0III. Addison-Wesley, Reading (1973)"},{"issue":"3","key":"21_CR12","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1093\/logcom\/8.3.293","volume":"8","author":"A.S. Rao","year":"1998","unstructured":"Rao, A.S., Georgeff, M.P.: Decision procedures for BDI logics. Journal of Logic and Computation\u00a08(3), 293\u2013343 (1998)","journal-title":"Journal of Logic and Computation"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. Journal of Symbolic Computation (to appear)","DOI":"10.1016\/S0747-7171(03)00040-3"},{"key":"21_CR14","volume-title":"Solving the Frame Problem","author":"M.P. Shanahan","year":"1997","unstructured":"Shanahan, M.P.: Solving the Frame Problem. MIT Press, Cambridge (1997)"},{"key":"21_CR15","unstructured":"Tansel, A. (ed.): Temporal Databases: theory, design, and implementation. Benjamin\/ Cummings (1993)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T18:58:08Z","timestamp":1553194688000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}