{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T06:10:01Z","timestamp":1747548601739,"version":"3.40.5"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[1999,4,1]],"date-time":"1999-04-01T00:00:00Z","timestamp":922924800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,4,1]],"date-time":"1999-04-01T00:00:00Z","timestamp":922924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[1999,4]]},"DOI":"10.1023\/a:1018919214722","type":"journal-article","created":{"date-parts":[[2003,2,19]],"date-time":"2003-02-19T22:07:13Z","timestamp":1045692433000},"page":"149-199","source":"Crossref","is-referenced-by-count":2,"title":["A model and a first analysis of distributed\u2010search contraction\u2010based strategies"],"prefix":"10.1007","volume":"27","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"325544_CR1","doi-asserted-by":"crossref","unstructured":"S. Anantharaman and M.P. Bonacina, An application of automated equational reasoning to many-valued logic, in: Proc. of CTRS-90, Lecture Notes in Computer Science, Vol. 516, eds. M. Okada and S. Kaplan (Springer-Verlag, 1991) pp. 156-161.","DOI":"10.1007\/3-540-54317-1_88"},{"issue":"1","key":"325544_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. Automat. Reason. 6(1) (1990) 76-109.","journal-title":"J. Automat. Reason."},{"issue":"1","key":"325544_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/jpdc.1994.1001","volume":"20","author":"M.J. Atallah","year":"1994","unstructured":"M.J. Atallah, F. Dehne, R. Miller, A. Rau-Chaplin and J.J. Tsay, Multisearch techniques: parallel data structures on a mesh-connected computer, J. Parallel Distrib. Comput. 20(1) (1994) 1-13.","journal-title":"J. Parallel Distrib. Comput."},{"key":"325544_CR4","doi-asserted-by":"crossref","unstructured":"M.J. Atallah and A. Fabri, On the multisearch problem for hypercubes, Comput. Geom. Theory Appl. 5 (1996).","DOI":"10.1016\/0925-7721(94)00023-9"},{"key":"325544_CR5","doi-asserted-by":"crossref","unstructured":"J. Avenhaus, J. Denzinger and M. Fuchs, DISCOUNT: a system for distributed equational deduction, in: Proc. of RTA-95, Lecture Notes in Computer Science, Vol. 914, ed. J. Hsiang (Springer, 1995).","DOI":"10.1007\/3-540-59200-8_72"},{"issue":"1","key":"325544_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L. Bachmair","year":"1988","unstructured":"L. Bachmair and N. Dershowitz, Critical pair criteria for completion, J. Symbolic Comput. 6(1) (1988) 1-18.","journal-title":"J. Symbolic Comput."},{"key":"325544_CR7","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger, Non-clausal resolution and superposition with selection and redundancy criteria, in: Proc. of LPAR-92, Lecture Notes in Artificial Intelligence, Vol. 624, ed. A. Voronkov (Springer-Verlag, 1992) pp. 273-284.","DOI":"10.1007\/BFb0013068"},{"key":"325544_CR8","unstructured":"L. Bachmair and H. Ganzinger, A theory of resolution, Technical Report MPI-I-97-2-005, Max Planck Institut f\u00fcr Informatik, 1997. To appear in: Handbook of Automated Reasoning, eds. J.A. Robinson and A. Voronkov (Elsevier Science)."},{"issue":"2","key":"325544_CR9","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch and W. Snyder, Basic paramodulation, Inform. and Comput. 121(2) (1995) 172-192.","journal-title":"Inform. and Comput."},{"key":"325544_CR10","doi-asserted-by":"crossref","unstructured":"A. B\u00e4umker, W. Dittrich and F. Meyer auf der Heide, Truly efficient parallel algorithms: 1-optimal multisearch for and extension of the BSP model, Technical Report tr-rsfb-96-008, Department of Mathematics and Computer Science, University of Paderborn (1996). See also Proc. of the 3rd European Symp. on Algorithms, Lecture Notes in Computer Science, Vol. 979 (1995) pp. 17\u201330.","DOI":"10.1007\/3-540-60313-1_131"},{"key":"325544_CR11","doi-asserted-by":"crossref","unstructured":"A. B\u00e4umker, W. Dittrich and A. Pietracaprina, The complexity of parallel multisearch on coarse grained machines, Algoritmica. Special Issue on Coarse Grained Parallel Algorithms (1998).","DOI":"10.1007\/PL00008261"},{"key":"325544_CR12","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. Symbolic Comput. 21 (1996) 507-522.","journal-title":"J. Symbolic Comput."},{"key":"325544_CR13","doi-asserted-by":"crossref","unstructured":"M.P. Bonacina, Experiments with subdivision of search in distributed theorem proving, in: Proc. of PASCO-97, eds. M. Hitz and E. Kaltofen (ACM Press, 1997) pp. 88-100.","DOI":"10.1145\/266670.266696"},{"key":"325544_CR14","unstructured":"M.P. Bonacina, Mechanical proofs of the Levi commutator problem, in: Notes of the CADE-15 Workshop on Problem Solving Methodologies with Automated Deduction, eds. P. Baumgartner et al. (1998) pp. 1-10."},{"key":"325544_CR15","unstructured":"M.P. Bonacina, Ten years of parallel theorem proving: a perspective, in: Notes of the FLoC-99 Workshop on Strategies in Automated Deduction, eds. B. Gramlich, H. Kirchner and F. Pfenning (1999) pp. 3-15. Full version: A taxonomy of parallel strategies for deduction, Technical Report 99-07, Department of Computer Science, University of Iowa (May 1999)."},{"key":"325544_CR16","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/BF00881888","volume":"12","author":"M.P. Bonacina","year":"1994","unstructured":"M.P. Bonacina and J. Hsiang, On subsumption in distributed derivations, J. Automat. Reason. 12 (1994) 225-240.","journal-title":"J. Automat. Reason."},{"key":"325544_CR17","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. Automat. Reason. 13 (1994) 1-33.","journal-title":"J. Automat. Reason."},{"key":"325544_CR18","first-page":"177","volume":"24","author":"M.P. Bonacina","year":"1995","unstructured":"M.P. Bonacina and J. Hsiang, The Clause-Diffusion methodology for distributed deduction, Fund. Inform. 24 (1995) 177-207.","journal-title":"Fund. Inform."},{"key":"325544_CR19","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1006\/jsco.1995.1014","volume":"19","author":"M.P. Bonacina","year":"1995","unstructured":"M.P. Bonacina and J. Hsiang, Distributed deduction by Clause-Diffusion: distributed contraction and the Aquarius prover, J. Symbolic Comput. 19 (1995) 245-267.","journal-title":"J. Symbolic Comput."},{"key":"325544_CR20","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, Theor. Comput. Sci. 146 (1995) 199-242.","journal-title":"Theor. Comput. Sci."},{"key":"325544_CR21","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1006\/inco.1998.2739","volume":"147","author":"M.P. Bonacina","year":"1998","unstructured":"M.P. Bonacina and J. Hsiang, On the modelling of search in theorem proving \u2014 towards a theory of strategy analysis, Inform. and Comput. 147 (1998) 171-208.","journal-title":"Inform. and Comput."},{"key":"325544_CR22","doi-asserted-by":"crossref","unstructured":"R. B\u00fcndgen, M. G\u00f6bel and W. K\u00fcchlin, A master-slave approach to parallel term-rewriting on a hierarchical multiprocessor, in: Proc. of the 4th DISCO, Lecture Notes in Computer Science, Vol. 1128, eds. J. Calmet and C. Limongelli (Springer, 1996) pp. 184-194.","DOI":"10.1007\/3-540-61697-7_17"},{"key":"325544_CR23","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. Symbolic Comput. 21 (1996) 475-506.","journal-title":"J. Symbolic Comput."},{"key":"325544_CR24","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. Symbolic Comput. 21 (1996) 523-541.","journal-title":"J. Symbolic Comput."},{"key":"325544_CR25","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud, Rewrite systems, in: Handbook of Theoretical Computer Science, Vol. B, ed. J. van Leeuwen (Elsevier, 1990) pp. 243-320.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"325544_CR26","unstructured":"B. Fronh\u00f6fer and G. Wrightson, eds., Parallelization in Inference Systems, Lecture Notes in Artificial Intelligence, Vol. 590 (Springer-Verlag, 1990)."},{"key":"325544_CR27","doi-asserted-by":"crossref","unstructured":"D. Fuchs, Requirement-based cooperative theorem proving, in: Proc. of JELIA-98, Lecture Notes in Artificial Intelligence, Vol. 1489, eds. J. Dix, L. Fari\u00f1as del Cerro and U. Furbach (Springer, 1998) pp. 139-153.","DOI":"10.1007\/3-540-49545-2_10"},{"key":"325544_CR28","doi-asserted-by":"crossref","unstructured":"M. Fuchs and A. Wolf, Cooperation in model elimination: CPTHEO, in: Proc. of CADE-15, Lecture Notes in Artificial Intelligence, Vol. 1421, eds. C. Kirchner and H. Kirchner (Springer, 1998) pp. 42-46.","DOI":"10.1007\/BFb0054245"},{"key":"325544_CR29","doi-asserted-by":"crossref","unstructured":"W. Gropp and E. Lusk, User's guide for mpich, a portable implementation of MPI, Technical Report 96\/6, MCS Division, Argonne National Laboratory (1996).","DOI":"10.2172\/378911"},{"key":"325544_CR30","doi-asserted-by":"crossref","unstructured":"J. Hsiang and M. Rusinowitch, On word problems in equational theories, in: Proc. of the 14th ICALP, Lecture Notes in Computer Science, Vol. 267, ed. Th. Ottman (Springer-Verlag, 1987) pp. 54-71.","DOI":"10.1007\/3-540-18088-5_6"},{"issue":"3","key":"325544_CR31","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M. Rusinowitch, Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method, J. ACM 38(3) (1991) 559-587.","journal-title":"J. ACM"},{"key":"325544_CR32","unstructured":"D. Kapur and H. Zhang, A case study of the completion procedure: proving ring commutativity problems, in: Computational Logic \u2014 Essays in Honor of Alan Robinson, eds. J.-L. Lassez and G. Plotkin (MIT Press, 1991) pp. 360-394."},{"key":"325544_CR33","doi-asserted-by":"crossref","unstructured":"C. Kirchner, C. Lynch and C. Scharff, Fine-grained concurrent completion, in: Proc. of RTA-96, Lecture Notes in Computer Science, Vol. 1103, ed. H. Ganzinger (Springer, 1996) pp. 3-17.","DOI":"10.1007\/3-540-61464-8_39"},{"key":"325544_CR34","unstructured":"R. Kowalski, Search strategies for theorem proving, in: Machine Intelligence, Vol. 5, eds. B. Meltzer and D. Michie (Edinburgh University Press, 1969) pp. 181-201."},{"key":"325544_CR35","doi-asserted-by":"crossref","unstructured":"A. Leitsch, The Resolution Calculus (Springer, 1997).","DOI":"10.1007\/978-3-642-60605-2"},{"key":"325544_CR36","unstructured":"D.W. Loveland, Automated Theorem Proving: A Logical Basis (North-Holland, 1978)."},{"key":"325544_CR37","doi-asserted-by":"crossref","unstructured":"W.W. McCune, Otter 3.0 reference manual and guide, Technical Report 94\/6, MCS Division, Argonne National Laboratory (1994).","DOI":"10.2172\/10129052"},{"key":"325544_CR38","unstructured":"W.W. McCune, 33 Basic test problems: a practical evaluation of some paramodulation strategies, in: Automated Reasoning and its Applications: Essays in Honor of Larry Wos, ed. R. Veroff (MIT Press, 1997) pp. 71-114."},{"issue":"3","key":"325544_CR39","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W.W. McCune","year":"1997","unstructured":"W.W. McCune, Solution of the Robbins problem, J. Automat. Reason. 19(3) (1997) 263-276.","journal-title":"J. Automat. Reason."},{"key":"325544_CR40","doi-asserted-by":"crossref","unstructured":"R. Niewenhuis, J.M. Rivero and M.A. Vallejo, The Barcelona prover, J. Automat. Reason. 18(2) (1997).","DOI":"10.1023\/A:1005862710017"},{"key":"325544_CR41","unstructured":"D.A. Plaisted, Mechanical theorem proving, in: Formal Techniques in Artificial Intelligence, ed. R.B. Banerji (Elsevier, 1990)."},{"key":"325544_CR42","doi-asserted-by":"crossref","unstructured":"D.A. Plaisted, Equational reasoning and term rewriting systems, in: Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 1, eds. D. Gabbay et al. (Oxford University Press, 1993) pp. 274-367.","DOI":"10.1093\/oso\/9780198537458.003.0005"},{"key":"325544_CR43","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":"325544_CR44","unstructured":"C.B. Suttner and J. Schumann, Parallel automated theorem proving, in: Parallel Processing for Artificial Intelligence, eds. L. Kanal et al. (Elsevier, 1994)."},{"issue":"2","key":"325544_CR45","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1005887414560","volume":"18","author":"T. Tammet","year":"1997","unstructured":"T. Tammet, Gandalf, J. Automat. Reason. 18(2) (1997) 199-204.","journal-title":"J. Automat. Reason."},{"key":"325544_CR46","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2307\/421131","volume":"1","author":"A. Urquhart","year":"1995","unstructured":"A. Urquhart, The complexity of propositional proofs, Bull. Symbolic Logic 1 (1995) 425-467.","journal-title":"Bull. Symbolic Logic"},{"key":"325544_CR47","doi-asserted-by":"crossref","unstructured":"C. Weidenbach, B. Gaede and G. Rock, SPASS & FLOTTER, in: Proc. of CADE-13, Lecture Notes in Artificial Intelligence, Vol. 1104, eds. M. McRobbie and J. Slaney (Springer, 1996) pp. 141-145.","DOI":"10.1007\/3-540-61511-3_75"},{"key":"325544_CR48","doi-asserted-by":"crossref","unstructured":"A. Wolf and R. Letz, Strategy parallelism in automated theorem proving, in: Proc. of FLAIRS-98 (1998).","DOI":"10.1007\/3-540-69778-0_32"},{"key":"325544_CR49","doi-asserted-by":"crossref","unstructured":"H. Zhang, Herky: high performance rewriting in RRL, in: Proc. of CADE-11, Lecture Notes in Artificial Intelligence, Vol. 607, ed. D. Kapur (Springer-Verlag, 1992) pp. 696-700.","DOI":"10.1007\/3-540-55602-8_206"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018919214722.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1018919214722\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018919214722.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:31:09Z","timestamp":1747546269000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1018919214722"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,4]]},"references-count":49,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[1999,4]]}},"alternative-id":["325544"],"URL":"https:\/\/doi.org\/10.1023\/a:1018919214722","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[1999,4]]}}}