{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:08Z","timestamp":1747546928390},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540616979"},{"type":"electronic","value":"9783540706359"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61697-7_17","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:13:10Z","timestamp":1330294390000},"page":"183-194","source":"Crossref","is-referenced-by-count":4,"title":["A master-slave approach to parallel term rewriting on a hierarchical multiprocessor"],"prefix":"10.1007","author":[{"given":"Reinhard","family":"B\u00fcndgen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manfred","family":"G\u00f6bel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"17_CR1","unstructured":"S. Anantharaman and N. Andrianarievelo. Heuristical criteria in refutational theorem proving. In A. Miola, editor, Design and Implementation of Symbolic Computation Systems, 1994. Springer-Verlag."},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"G. Attardi and C. Traverso. A strategy-accurate parallel Buchberger algorithm. In Hong [19].","DOI":"10.1006\/jsco.1996.0022"},{"key":"17_CR3","series-title":"volume 690 of LNCS","volume-title":"Rewriting Techniques and Applications","author":"J. Avenhaus","year":"1993","unstructured":"J. Avenhaus and J. Denzinger. Distributing equational theorem proving.."},{"key":"17_CR4","unstructured":"L. Bachmair, N. Dershowitz, and D. Plaisted. Completion without failure. In H. A\u00eft-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2 of Rewriting Techniques, chapter 1. Academic Press, 1989."},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"M. Bonacina and J. Hsiang. Distributed Deduction by Clause-Diffusion: Distributed Contraction and the Acquarius Prover. J. Symbolic Computation, 19(1\/2\/3), 1995.","DOI":"10.1006\/jsco.1995.1014"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"M. Bonacina and J. Hsiang. Completion procedures as semidecision procedures. In S. Kaplan and M. Okada, editors, Conditional Term Rewriting Systems, 1990. Springer-Verlag.","DOI":"10.1007\/3-540-54317-1_92"},{"key":"17_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00881910","volume":"13","author":"M. Bonacina","year":"1994","unstructured":"M. Bonacina and J. Hsiang. Parallelization of deduction strategies: An analytical study. J. Automated Reasoning, 13:1\u201333, 1994.","journal-title":"J. Automated Reasoning"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"T. Bubeck, M. Hiller, W. K\u00fcchlin, and W. Rosenstiel. Distributed symbolic computation with DTS. In A. Ferreira and J. Rolim, editors, Parallel Algorithms for Irregularly Structured Problems, 2nd Intl. Workshop, IRREGULAR'95, 1995.","DOI":"10.1007\/3-540-60321-2_19"},{"key":"17_CR9","series-title":"volume 690 of LNCS","volume-title":"Rewriting Techniques and Applications","author":"R. B\u00fcndgen","year":"1993","unstructured":"R. B\u00fcndgen. Reduce the redex \u2192 ReDuX.."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"R. B\u00fcndgen, M. G\u00f6bel, and W. K\u00fcchlin. A fine-grained parallel completion procedure. In J. von zur Gathen and M. Giesbrecht, editors, Proc. 1994 International Symposium on Symbolic and Algebraic Computation: ISSAC'94, 1994. ACM Press.","DOI":"10.1145\/190347.190427"},{"key":"17_CR11","unstructured":"R. B\u00fcndgen, M. G\u00f6bel, and W. K\u00fcchlin. Multi-threaded AC term rewriting. In Hong [19]."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"R. B\u00fcndgen, M. G\u00f6bel, and W. K\u00fcchlin. Parallel ReDuX \u2192 PaReDuX. In J. Hsiang, editor, Rewriting Techniques and Applications, 6th Intl. Conf., RTA-95, 1995. Springer-Verlag.","DOI":"10.1007\/3-540-59200-8_74"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"R. B\u00fcndgen, M. G\u00f6bel, and W. K\u00fcchlin. Strategy compliant multi-threaded term completion. J. Symbolic Computation, 1996. To appear.","DOI":"10.1006\/jsco.1996.0027"},{"key":"17_CR14","unstructured":"J. Denzinger. Teamwork: Eine Methode zum Entwurf verteilter, wissensbasierter Theorembeweiser. PhD thesis, Universit\u00e4t Kaiserslautern, 1993."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"J. Denzinger and D. Fuchs. Goal oriented equational theorem proving using teamwork. In Proc. 18th KI-94, 1994. Springer-Verlag.","DOI":"10.1007\/3-540-58467-6_30"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Formal Models and Semantics, volume 2 of Handbook of Theoretical Computer Science, chapter 6. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"17_CR17","unstructured":"B. Fronh\u00f6fer and G. Wrightson, editors. Parallelization in Inference Systems, 1990. Springer-Verlag."},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"M. Fuchs. Learning proof heuristics by adapting parameters. Technical report, Fachbereich Informatik, Universi\u00e4t Kaiserslautern, 1995.","DOI":"10.1016\/B978-1-55860-377-6.50037-2"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"H. Hong, editor. First Intl. Symp. Parallel Symbolic Computation PASCO'94, 1994. World Scientific.","DOI":"10.1142\/2546"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"J. Hsiang and M. Rusinowitch. On word problems in equational theories. In T. Ottmann, editor, Automata, Languages and Programming, 1987. Springer-Verlag.","DOI":"10.1007\/3-540-18088-5_6"},{"key":"17_CR21","series-title":"volume 690 of LNCS","volume-title":"Rewriting Techniques and Applications","year":"1993","unstructured":"C. Kirchner, editor. Rewriting Techniques and Applications, volume 690 of LNCS, Montreal, Canada, 1993. Springer-Verlag."},{"key":"17_CR22","unstructured":"C. Kirchner and P. Viry. Implementing parallel rewriting. In Fronh\u00f6fer and Wrightson [17]."},{"key":"17_CR23","unstructured":"D. Knuth and P. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra. Pergamon Press, 1970."},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"W. K\u00fcchlin. A theorem-proving approach to the Knuth-Bendix completion algorithm. In J. Calmet, editor, Computer Algebra, 1982. Springer-Verlag.","DOI":"10.1007\/3-540-11607-9"},{"key":"17_CR25","unstructured":"W. K\u00fcchlin. PARSAC-2: A parallel SAC-2 based on threads. In S. Sakata, editor, Applied Algebra, Algebraic Algorithms, and Error-Correcting Codes: 8th International Conference, AAECC-8, 1990. Springer-Verlag."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"W. K\u00fcchlin. The S-threads environment for parallel symbolic computation. In R. Zippel, editor, Computer Algebra and Parallelism, 1992. Springer-Verlag.","DOI":"10.1007\/3-540-55328-2"},{"key":"17_CR27","unstructured":"W. K\u00fcchlin. PARSAC-2: Parallel computer algebra on the desk-top. In J. Fleischer, J. Grabmeier, F. Hehl, and W. K\u00fcchlin, editors, Computer Algebra in Science and Engineering, 1995. World Scientific."},{"key":"17_CR28","unstructured":"W. K\u00fcchlin and J. Ward. Experiments with virtual C Threads. In Proc. Fourth IEEE Symp. on Parallel and Distributed Processing, 1992. IEEE Press."},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"E. Lusk and W. McCune. Experiments with ROO, a parallel automated deduction system. In Fronh\u00f6fer and Wrightson [17].","DOI":"10.1007\/3-540-55425-4_6"},{"key":"17_CR30","first-page":"209","volume":"1","author":"E. Lusk","year":"1985","unstructured":"E. Lusk and R. Overbeek. Reasoning about equality. J. Automated Reasoning, 1:209\u2013228, 1985.","journal-title":"J. Automated Reasoning"},{"key":"17_CR31","volume-title":"Technical Report WSI 95-06","author":"P. Maier","year":"1995","unstructured":"P. Maier, M. G\u00f6bel, and R. B\u00fcndgen. Multi-threaded unfailing completion. Technical Report WSI 95-06, Universit\u00e4t T\u00fcbingen, D-72076 T\u00fcbingen, 1995."},{"key":"17_CR32","unstructured":"J. Schumann. SiCoTHEO \u2014 simple competive parallel theorem provers based on SETHEO. 1995. Proc. PPAI'95, Montreal, Canada, 1995."},{"issue":"4","key":"17_CR33","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1002\/cpe.4330020404","volume":"2","author":"V. Sunderam","year":"1990","unstructured":"V. Sunderam. PVM: A framework for parallel distributed computing. Concurrency: Practice and Experience, 2(4):315\u2013339, 1990.","journal-title":"Concurrency: Practice and Experience"},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In A. Bundy, editor, Automated Deduction-CADE-12, 1994. Springer-Verlag.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"17_CR35","unstructured":"C. Suttner and J. Schumann. Parallel automated theorem proving. In L. Kanal, V. Kumar, H. Kitano, and C. Suttner, editors, Parallel Processing for Artificial Intellegence. Elsevier, 1994."},{"key":"17_CR36","unstructured":"A. Tarski. Logic, Semantics, Metamathematics. Oxford University Press, 1956."}],"container-title":["Lecture Notes in Computer Science","Design and Implementation of Symbolic Computation Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61697-7_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:09:25Z","timestamp":1605647365000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61697-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616979","9783540706359"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-61697-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}