{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:03Z","timestamp":1747546923299},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651413"},{"type":"electronic","value":"9783540495451"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49545-2_10","type":"book-chapter","created":{"date-parts":[[2007,8,6]],"date-time":"2007-08-06T18:41:28Z","timestamp":1186425688000},"page":"139-153","source":"Crossref","is-referenced-by-count":2,"title":["Requirement-Based Cooperative Theorem Proving"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Fuchs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,2,26]]},"reference":[{"key":"10_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/3-540-59200-8_72","volume-title":"Proc. 6th RTA","author":"J. Avenhaus","year":"1995","unstructured":"J. Avenhaus, J. Denzinger, and M. Fuchs. DISCOUNT: A System For Distributed Equational Deduction. In Proc. 6th RTA, pages 397\u2013402, Kaiserslautern, 1995. LNCS 914."},{"key":"10_CR2","volume-title":"Coll. on the Resolution of Equations in Algebraic Structures","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair, N. Dershowitz, and D.A. Plaisted. Completion without Failure. In Coll. on the Resolution of Equations in Algebraic Structures. Academic Press, Austin, 1989."},{"issue":"3","key":"10_CR3","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217\u2013247, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"10_CR4","doi-asserted-by":"crossref","first-page":"177","DOI":"10.3233\/FI-1995-24128","volume":"24","author":"M.P. Bonacina","year":"1995","unstructured":"M.P. Bonacina and J. Hsiang. The Clause-Diffusion methodology for distributed deduction. Fundamenta Informaticae, 24:177\u2013207, 1995.","journal-title":"Fundamenta Informaticae"},{"issue":"4","key":"10_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. Journal of Symbolic Computation, 21(4):507\u2013522, 1996.","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR6","unstructured":"J. Denzinger. Knowledge-based distributed search using teamwork. In Proc. ICMAS-95, pages 81\u201388, San Francisco, 1995. AAAI-Press."},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"J. Denzinger and D. Fuchs. Enhancing conventional search systems with multi-agent techniques: a case study. In Proc. ICMAS-98, Paris, France, 1998.","DOI":"10.1109\/ICMAS.1998.699242"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"W. Ertel. OR-Parallel Theorem Proving with Random Competition. In Proceedings of LPAR\u201992, pages 226\u2013237, St. Petersburg, Russia, 1992. Springer LNAI 624.","DOI":"10.1007\/BFb0013064"},{"key":"10_CR9","series-title":"Technical Report","volume-title":"Knowledge-based cooperation between theorem provers by TECHS","author":"D. Fuchs","year":"1997","unstructured":"D. Fuchs and J. Denzinger. Knowledge-based cooperation between theorem provers by TECHS. Technical Report SR-97-11, University of Kaiserslautern, Kaiserslautern, 1997."},{"key":"10_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/BFb0052379","volume-title":"Proc. 9th RTA","author":"D. Fuchs","year":"1998","unstructured":"D. Fuchs. Coupling saturation-based provers by exchanging positive\/negative information. In Proc. 9th RTA, pages 317\u2013331, Tsukuba, Japan, 1998. LNCS 1379."},{"key":"10_CR11","series-title":"Technical Report","volume-title":"Requirement-based cooperative theorem proving","author":"D. Fuchs","year":"1998","unstructured":"D. Fuchs. Requirement-based cooperative theorem proving. Technical Report SR-98-02 ( ftp:\/\/ftp.uni-kl.de\/reports_uni-kl\/computer_science\/SEKI\/1998\/Fuchs.SR-98-02.ps.gz ), University of Kaiserslautern, Kaiserslautern, 1998."},{"key":"10_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume-title":"Proc. ICALP87","author":"J. Hsiang","year":"1987","unstructured":"J. Hsiang and M. Rusinowitch. On word problems in equational theories. In Proc. ICALP87, pages 54\u201371. LNCS 267, 1987."},{"issue":"2","key":"10_CR13","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1023\/A:1005824522737","volume":"18","author":"G. Sutcliffe","year":"1997","unstructured":"G. Sutcliffe and C.B. Suttner. The results of the cade-13 ATP system competition. Journal of Automated Reasoning, 18(2):271\u2013286, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C.B. Suttner, and T. Yemenis. The TPTP Problem Library. In CADE-12, pages 252\u2013266, Nancy, 1994. LNAI 814.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"10_CR15","unstructured":"G. Sutcliffe. A heterogeneous parallel deduction system. In Proc. FGCS\u201992 Workshop W3, 1992."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"C. Weidenbach, B. Gaede, and G. Rock. Spass & Flotter Version 0.42. In Proc. CADE-13, pages 141\u2013145, New Brunswick, 1996. LNAI 1104.","DOI":"10.1007\/3-540-61511-3_75"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49545-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T17:09:50Z","timestamp":1587834590000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49545-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651413","9783540495451"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-49545-2_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}