{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:01Z","timestamp":1747546921329},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054245","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"42-46","source":"Crossref","is-referenced-by-count":5,"title":["System description: Cooperation in model elimination: CPTHEO"],"prefix":"10.1007","author":[{"given":"Marc","family":"Fuchs","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Wolf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"6_CR1","first-page":"78","volume":"90","author":"S. E. Conry","year":"1990","unstructured":"S. E. Conry et al., DARES: A Distributed Automated Reasoning System. Proc. AAAI-90, pp. 78\u201385, 1990.","journal-title":"Proc. AAAI"},{"key":"6_CR2","unstructured":"J. Denzinger. Knowledge-based distributed search using teamwork. ICMAS-95, AAAI-Press, pp. 81\u201388, 1995."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"D. Fuchs. Coupling Saturation-Based Provers by Exchanging Positive\/Negative Information. Proc. RTA-98, LNCS 1379, Springer, pp. 317\u2013331, 1998.","DOI":"10.1007\/BFb0052379"},{"key":"6_CR4","unstructured":"M. Fuchs. Similarity-Based Lemma Generation for Model Elimination. Proc. FTP-97 Workshop, RISC-Linz Report Series No. 97-50, pp. 63\u201367, 1997."},{"issue":"2","key":"6_CR5","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"M. Moser et al.. SETHEO and E-SETHEO. The CADE-13 Systems. JAR, 18(2), pp. 237\u2013246, 1997.","journal-title":"JAR"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"J. Schumann. DELTA \u2014 A Bottom-Up Preprocessor for Top-Down Theorem Provers. Proc. CADE-12, Springer, pp. 774\u2013777, 1994.","DOI":"10.1007\/3-540-58156-1_58"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe et al. The TPTP Problem Library. Proc. CADE-12, Springer, pp. 252\u2013266, 1994.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"C. Suttner, J. Schumann. Parallel Automated Theorem Proving. PPAI, Elsevier, pp. 209\u2013257, 1993.","DOI":"10.1016\/B978-0-444-81704-4.50015-6"},{"key":"6_CR9","unstructured":"A. Wolf, M. Fuchs. Cooperative Parallel Automated Theorem Proving. Dynamic Load Distribution for Parallel Applications, Teubner, pp. 129\u2013145, 1997."},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"A. Wolf, R. Letz. Strategy Parallelism in Automated Theorem Proving. Proc. FLAIRS-98 (to appear), 1998.","DOI":"10.1007\/3-540-69778-0_32"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054245","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T06:45:36Z","timestamp":1555656336000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054245"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/bfb0054245","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}