{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:57:07Z","timestamp":1781927827143,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540223450","type":"print"},{"value":"9783540259848","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-25984-8_3","type":"book-chapter","created":{"date-parts":[[2010,9,11]],"date-time":"2010-09-11T02:31:38Z","timestamp":1284172298000},"page":"60-74","source":"Crossref","is-referenced-by-count":4,"title":["Efficient Checking of Term Ordering Constraints"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Riazanov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"2-3","key":"3_CR1","first-page":"127","volume":"15","author":"T.. Hillenbrand","year":"2002","unstructured":"Hillenbrand, T., L\u00f6chner, B.: A Phytography of Waldmeister. AI Communications\u00a015(2-3), 127\u2013133 (2002)","journal-title":"AI Communications"},{"key":"3_CR2","volume-title":"Partial Evaluation and Automatic Program Generation","author":"N.D. Jones","year":"1993","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall International, Englewood Cliffs (1993)"},{"key":"3_CR3","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"issue":"2","key":"3_CR4","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00021-X","volume":"183","author":"K. Korovin","year":"2003","unstructured":"Korovin, K., Voronkov, A.: Orienting rewrite rules with the Knuth-Bendix order. Information and Computation\u00a0183(2), 165\u2013186 (2003)","journal-title":"Information and Computation"},{"key":"3_CR5","unstructured":"L\u00f6chner, B., Schulz, S.: An Evaluation of Shared Rewriting. In: de Nivelle, H., Schulz, S. (eds.) Proc. of the 2nd International Workshop on the Implementation of Logics, MPI Preprint, Saarbr\u00fccken. Max-Planck-Institut f\u00fcr Informatik, pp. 33\u201348 (2001)"},{"issue":"2","key":"3_CR6","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1006\/inco.2002.3146","volume":"178","author":"R. Nieuwenhuis","year":"2002","unstructured":"Nieuwenhuis, R., Rivero, J.M.: Practical algorithms for deciding path ordering constraint satisfaction. Information and Computation\u00a0178(2), 422\u2013440 (2002)","journal-title":"Information and Computation"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 7. vol.\u00a0I, pp. 371\u2013443. Elsevier Science, Amsterdam (2001)"},{"key":"3_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-40006-0_15","volume-title":"Logics in Artificial Intelligence","author":"A. Riazanov","year":"2000","unstructured":"Riazanov, A., Voronkov, A.: Partially adaptive code trees. In: Brewka, G., Moniz Pereira, L., Ojeda-Aciego, M., de Guzm\u00e1n, I.P. (eds.) JELIA 2000. LNCS (LNAI), vol.\u00a01919, pp. 209\u2013223. Springer, Heidelberg (2000)"},{"issue":"2-3","key":"3_CR9","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"3_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-540-45085-6_34","volume-title":"Automated Deduction \u2013 CADE-19","author":"A. Riazanov","year":"2003","unstructured":"Riazanov, A., Voronkov, A.: Efficient instance retrieval with standard and relational path indexing. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 380\u2013396. Springer, Heidelberg (2003)"},{"issue":"1-2","key":"3_CR11","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","volume":"36","author":"A. Riazanov","year":"2003","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. Journal of Symbolic Computations\u00a036(1-2), 101\u2013115 (2003)","journal-title":"Journal of Symbolic Computations"},{"key":"3_CR12","unstructured":"Rivero, J.M.A.: Data Structures and Algorithms for Automated Deduction with Equality. Phd thesis, Universitat Polit\u00e8cnica de Catalunya, Barcelona (May 2000)"},{"issue":"2-3","key":"3_CR13","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E - a braniac theorem prover. AI Communications\u00a015(2-3), 111\u2013126 (2002)","journal-title":"AI Communications"},{"key":"3_CR14","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library. tptp v. 2.4.1. Technical report, University of Miami (2001)"},{"issue":"2","key":"3_CR15","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"Tammet, T.: Gandalf. Journal of Automated Reasoning\u00a018(2), 199\u2013204 (1997)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-25984-8_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:21:23Z","timestamp":1620012083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-25984-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223450","9783540259848"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-25984-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}