{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:28:49Z","timestamp":1725488929652},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_38","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T03:18:26Z","timestamp":1186888706000},"page":"486-500","source":"Crossref","is-referenced-by-count":9,"title":["The Next Waldmeister Loop"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Hillenbrand","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"L\u00f6chner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"38_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/3-540-59200-8_72","volume-title":"Proceedings of the 6th International Conference on Rewriting Techniques and Applications","author":"J. Avenhaus","year":"1995","unstructured":"J. Avenhaus, J. Denzinger, and M. Fuchs. Discount: a system for distributed equational deduction. In J. Hsiang, ed., Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of LNCS, pp. 397\u2013402. Springer-Verlag, 1995."},{"key":"38_CR2","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and D. A. Plaisted. Rewriting. In A. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, volume I, chapter 9, pp. 535\u2013610. Elsevier, 2001.","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"key":"38_CR3","doi-asserted-by":"crossref","unstructured":"P. Graf. Term Indexing, volume 1053 of LNAI. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61040-5"},{"key":"38_CR4","unstructured":"Th. Hillenbrand. Schnelles Gleichheitsbeweisen: Vom Vervollst\u00e4ndigungskalk\u00fcl zum Waldmeister-System. Diplomarbeit, Universit\u00e4t Kaiserslautern, Fachbereich Informatik, 2000. Available via http:\/\/www.mpi-sb.mpg.de\/~hillen\/documents\/SchnellesBeweisen.ps.gz ."},{"key":"38_CR5","unstructured":"Th. Hillenbrand and B. L\u00f6chner. The next Waldmeister loop (extended abstract). In H. de Nivelle and S. Schulz, eds., Proceedings of the Second International Workshop on Implementation of Logics, Technical Report MPI-I-2001-2-006, pp. 13\u201321. Max-Planck-Institut f\u00fcr Informatik Saarbr\u00fccken, 2001."},{"key":"38_CR6","unstructured":"W. K\u00fcchlin. An implementation and investigation of the Knuth-Bendix completion procedure. Interner Bericht 17\/82, Universit\u00e4t Karlsruhe, 1982."},{"key":"38_CR7","unstructured":"B. L\u00f6chner and S. Schulz. An evaluation of shared rewriting. In H. de Nivelle and S. Schulz, eds., Proceedings of the Second International Workshop on Implementation of Logics, Technical Report MPI-I-2001-2-006, pp. 33\u201348. Max-Planck-Institut f\u00fcr Informatik Saarbr\u00fccken, 2001."},{"key":"38_CR8","doi-asserted-by":"crossref","unstructured":"W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL-94\/6, Argonne National Laboratory, 1994.","DOI":"10.2172\/10129052"},{"key":"38_CR9","unstructured":"W. McCune. 33 basic test problems: a practical evaluation of some paramod-ulation strategies. In R. Veroff, ed., Automated Reasoning and its Applications: Essays in Honor of Larry Wos, chapter 5, pp. 71\u2013114. MIT Press, 1997."},{"key":"38_CR10","unstructured":"I. V. Ramakrishnan, R. Sekar, and A. Voronkov. Term indexing. In A. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, volume II, chapter 26, pp. 1853\u20131964. Elsevier, 2001."},{"key":"38_CR11","unstructured":"A. Riazanov and A. Voronkov. Limited resource strategy in resolution theorem proving. Technical Report CSPP-7, University of Manchester, 2000. Accepted for publication in Journal of Symbolic Computation."},{"key":"38_CR12","volume-title":"Technical Report 99\/02","author":"C.B. Suttner","year":"1999","unstructured":"C.B. Suttner and G. Sutcliffe. The TPTP problem library (TPTP v2.2.0). Technical Report 99\/02, James Cook University, Townsville, 1999."},{"key":"38_CR13","doi-asserted-by":"crossref","unstructured":"A. Voronkov. Algorithms, datastructures, and other issues in efficient automated deduction (invited talk). In R. Gor\u00e9, A. Leitsch, and T. Nipkow, eds., Proceedings of the First International Joint Conference on Automated Reasoning, volume 2083 of LNAI, pp. 13\u201328. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45744-5_3"},{"key":"38_CR14","unstructured":"Chr. Weidenbach. Combining superposition, sorts and splitting. In A. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, volume II, chapter 27, pp. 1965\u20132013. Elsevier, 2001."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,21]],"date-time":"2021-08-21T12:36:28Z","timestamp":1629549388000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_38","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}