{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:14:45Z","timestamp":1725488085640},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651413"},{"type":"electronic","value":"9783540495451"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49545-2_8","type":"book-chapter","created":{"date-parts":[[2007,8,6]],"date-time":"2007-08-06T14:41:28Z","timestamp":1186411288000},"page":"107-121","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Analysis of Distributed-Search Contraction-Based Strategies"],"prefix":"10.1007","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,2,26]]},"reference":[{"key":"8_CR1","series-title":"Lect Notes Comput Sci","first-page":"156","volume-title":"CTRS-90","author":"S. Anantharaman","year":"1990","unstructured":"S. Anantharaman and M. P. Bonacina. An application of automated equational reasoning to many-valued logic. In M. Okada and S. Kaplan, editors, CTRS-90, volume 516 of LNCS, pages 156\u2013161. Springer Verlag, 1990."},{"issue":"1","key":"8_CR2","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/BF00302643","volume":"6","author":"S. Anantharaman","year":"1990","unstructured":"S. Anantharaman and J. Hsiang. Automated proofs of the Moufang identities in alternative rings. J. of Automated Reasoning, 6(1):76\u2013109, 1990.","journal-title":"J. of Automated Reasoning"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. Non-clausal resolution and superposition with selection and redundancy criteria. In A. Voronkov, editor, LPAR-92, volume 624 of LNAI, pages 273\u2013284. Springer Verlag, 1992.","DOI":"10.1007\/BFb0013068"},{"key":"8_CR4","unstructured":"L. Bachmair and H. Ganzinger. A theory of resolution. Technical Report MPI-I-97-2-005, Max Planck Institut f\u00fcr Informatik, 1997."},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1006\/jsco.1996.0028","volume":"21","author":"M. P. Bonacina","year":"1996","unstructured":"M. P. Bonacina. On the reconstruction of proofs in distributed theorem proving: a modified Clause-Diffusion method. J. of Symbolic Computation, 21:507\u2013522, 1996.","journal-title":"J. of Symbolic Computation"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"M. P. Bonacina. Experiments with subdivision of search in distributed theorem proving. In M. Hitz and E. Kaltofen, editors, PASCO-97, pages 88\u2013100. ACM Press, 1997.","DOI":"10.1145\/266670.266696"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"M. P. Bonacina. Distributed contraction-based strategies: model and analysis. Technical Report 98-02, Dept. of Computer Science, University of Iowa, 1998.","DOI":"10.1007\/3-540-49545-2_8"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00881910","volume":"13","author":"M. P. Bonacina","year":"1994","unstructured":"M. P. Bonacina and J. Hsiang. Parallelization of deduction strategies: an analytical study. J. of Automated Reasoning, 13:1\u201333, 1994.","journal-title":"J. of Automated Reasoning"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0304-3975(94)00187-N","volume":"146","author":"M. P. Bonacina","year":"1995","unstructured":"M. P. Bonacina and J. Hsiang. Towards a foundation of completion procedures as semidecision procedures. Theoretical Computer Science, 146:199\u2013242, 1995.","journal-title":"Theoretical Computer Science"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"M. P. Bonacina and J. Hsiang. On the modelling of search in theorem proving \u2014 Towards a theory of strategy analysis. Information and Computation, forthcoming, 1998.","DOI":"10.1006\/inco.1998.2739"},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1006\/jsco.1996.0027","volume":"21","author":"R. B\u00fcndgen","year":"1996","unstructured":"R. B\u00fcndgen, M. G\u00f6bel, and W. K\u00fcchlin. Strategy-compliant multi-threaded term completion. J. of Symbolic Computation, 21:475\u2013506, 1996.","journal-title":"J. of Symbolic Computation"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1006\/jsco.1996.0029","volume":"21","author":"J. Denzinger","year":"1996","unstructured":"J. Denzinger and S. Schulz. Recording and analyzing knowledge-based distributed deduction processes. J. of Symbolic Computation, 21:523\u2013541, 1996.","journal-title":"J. of Symbolic Computation"},{"key":"8_CR13","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243\u2013320. Elsevier, Amsterdam, 1990."},{"key":"8_CR14","series-title":"Lect Notes Comput Sci","first-page":"513","volume-title":"3rd RTA","author":"D. Kapur","year":"1989","unstructured":"D. Kapur and H. Zhang. An overview of RRL: rewrite rule laboratory. In N. Dershowitz, editor, 3rd RTA, volume 355 of LNCS, pages 513\u2013529. Springer Verlag, 1989."},{"key":"8_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/3-540-61464-8_39","volume-title":"7th RTA","author":"C. Kirchner","year":"1996","unstructured":"C. Kirchner, C. Lynch, and C. Scharff. Fine-grained concurrent completion. In H. Ganzinger, editor, 7th RTA, volume 1103 of LNCS, pages 3\u201317. Springer Verlag, 1996."},{"key":"8_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-60605-2","volume-title":"The Resolution Calculus","author":"A. Leitsch","year":"1997","unstructured":"A. Leitsch. The Resolution Calculus. Springer, Berlin, 1997."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"W. McCune. Otter 3.0 reference manual and guide. Technical Report 94\/6, MCS Div., Argonne Nat. Lab., 1994.","DOI":"10.2172\/10129052"},{"issue":"3","key":"8_CR18","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"W. McCune. Solution of the Robbins problem. J. of Automated Reasoning, 19(3):263\u2013276, 1997.","journal-title":"J. of Automated Reasoning"},{"key":"8_CR19","first-page":"273","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"D. A. Plaisted","year":"1993","unstructured":"D. A. Plaisted. Equational reasoning and term rewriting systems. In D. Gabbay and J. Siekmann, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 273\u2013364. Oxford University Press, New York, 1993."},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"D. A. Plaisted and Y. Zhu. The Efficiency of Theorem Proving Strategies. Friedr. Vieweg & Sohns, 1997.","DOI":"10.1007\/978-3-322-93862-6"},{"key":"8_CR21","volume-title":"Parallel Processing for Artificial Intelligence","author":"C. B. Suttner","year":"1994","unstructured":"C. B. Suttner and J. Schumann. Parallel automated theorem proving. In L. Kanal, V. Kumar, H. Kitano, and C. B. Suttner, editors, Parallel Processing for Artificial Intelligence. Elsevier, Amsterdam, 1994."},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A. Urquhart","year":"1995","unstructured":"A. Urquhart. The complexity of propositional proofs. Bulletin of Symbolic Logic, 1:425\u2013467, 1995.","journal-title":"Bulletin of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49545-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T10:01:10Z","timestamp":1558260070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49545-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651413","9783540495451"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-49545-2_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"26 February 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}