{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T20:40:12Z","timestamp":1737060012848,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540430759"},{"type":"electronic","value":"9783540455752"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45575-2_11","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T01:30:22Z","timestamp":1180575022000},"page":"95-108","source":"Crossref","is-referenced-by-count":2,"title":["Adaptive Saturation-Based Reasoning"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Riazanov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,12,18]]},"reference":[{"key":"11_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/3-540-59200-8_72","volume-title":"DISCOUNT: a system for distributed equational deduction","author":"J. Avenhaus","year":"1995","unstructured":"J. Avenhaus, J. Denzinger, and M. Fuchs. DISCOUNT: a system for distributed equational deduction. In J. Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA\u201495), volume 914 of Lecture Notes in Computer Science, pages 397\u2013402, Kaiserslautern, 1995."},{"key":"11_CR2","unstructured":"H. de Nivelle. Bliksem 1.10 User\u2019s Manual. MPI f\u00fcr Informatik, Saarbr\u00fccken, 2000."},{"key":"11_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Term Indexing","author":"P. Graf","year":"1996","unstructured":"P. Graf. Term Indexing, volume 1053 of Lecture Notes in Computer Science. Springer Verlag, 1996."},{"issue":"2","key":"11_CR4","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"Th. Hillenbrand","year":"1997","unstructured":"Th. Hillenbrand, A. Buch, R. Vogt, and B. L\u00f6chner. Waldmeister: Highperformance equational deduction. Journal of Automated Reasoning, 18(2):265\u2013270, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"E.L. Lusk. Controlling redundancy in large search spaces: Argonne-style theorem proving through the years. In A. Voronkov, editor, Logic Programming and Automated Reasoning. International Conference LPAR\u201992., volume 624 of Lecture Notes in Artificial Intelligence, pages 96\u2013106, St.Petersburg, Russia, July 1992.","DOI":"10.1007\/BFb0013052"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"W.W. McCune. OTTER 3.0 reference manual and guide. Technical Report ANL-94\/6, Argonne National Laboratory, January 1994.","DOI":"10.2172\/10129052"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"M. Moser, O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, and K. Mayr. SETHEO and E-SETHEO-the CADE-13 systems. Journal of Automated Reasoning, 18:237\u2013246, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"I.V. Ramakrishnan, R. Sekar, and A. Voronkov. Term indexing. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 26, pages 1853\u20131964. Elsevier Science, 2001.","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"A. Riazanov and A. Voronkov. Vampire. In H. Ganzinger, editor, Automated Deduction-CADE-16. 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 292\u2013296, Trento, Italy, July 1999.","DOI":"10.1007\/3-540-48660-7_26"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"A. Riazanov and A. Voronkov. Vampire 1.1 (system description). In R. Gore, A. Leitsch, and T. Nipkow, editors, Automated Reasoning. First International Joint Conference, IJCAR 2001, volume 2083 of Lecture Notes in Artificial Intelligence, pages 376\u2013380, Siena, Italy, June 2001.","DOI":"10.1007\/3-540-45744-5_29"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"S. Schulz. System abstract: E 0.61. In R. Gore, A. Leitsch, and T. Nipkow, editors, Automated Reasoning. First International Joint Conference, IJCAR 2001, volume 2083 of Lecture Notes in Artificial Intelligence, pages 370\u2013375, Siena, Italy, June 2001.","DOI":"10.1007\/3-540-45744-5_28"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"J. Schumann and B. Fischer. NORA\/HAMMR: Making deduction-based software component retrieval practical. In Proc. Automated Software Engineering (ASE-97), pages 246\u2013254, Lake Tahoe, November 1997. IEEE Computer Society Press.","DOI":"10.1109\/ASE.1997.632845"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe. The CADE-16 ATP system competition. Journal of Automated Reasoning, 2000. to appear.","DOI":"10.1023\/A:1006393501098"},{"issue":"2","key":"11_CR14","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"T. Tammet. Gandalf. Journal of Automated Reasoning, 18(2):199\u2013204, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR15","unstructured":"A. Voronkov. CASC 16 1 2. Preprint CSPP-4, Department of Computer Science, University of Manchester, February 2000."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, E. Keen, C. Theobalt, and D. Topic. System description: Spass version 1.0.0. In H. Ganzinger, editor, Automated Deduction\u2014CADE-16. 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 378\u2013382,Trento, Italy, July 1999.","DOI":"10.1007\/3-540-48660-7_34"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45575-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T20:12:52Z","timestamp":1737058372000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45575-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430759","9783540455752"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45575-2_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}