{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:22:18Z","timestamp":1725495738392},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643012"},{"type":"electronic","value":"9783540697213"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0052379","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T01:31:11Z","timestamp":1149643871000},"page":"317-331","source":"Crossref","is-referenced-by-count":2,"title":["Coupling saturation-based provers by exchanging positive\/negative information"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Fuchs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,18]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"J. Avenhaus and J. Denzinger. Distributing equational theorem proving. In Proc. 5th RTA, pages 62\u201376, Montreal, 1993. LNCS 690.","DOI":"10.1007\/3-540-56868-9_6"},{"key":"24_CR2","doi-asserted-by":"crossref","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.","DOI":"10.1007\/3-540-59200-8_72"},{"key":"24_CR3","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":"24_CR4","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":"24_CR5","doi-asserted-by":"crossref","unstructured":"J. Denzinger and M. Fuchs. Goal oriented equational theorem proving. In Proc. 18th KI-94, pages 343\u2013354, Saarbr\u00fccken, 1994. LNAI 861.","DOI":"10.1007\/3-540-58467-6_30"},{"key":"24_CR6","unstructured":"J. Denzinger and D. Fuchs. Referees for teamwork. In Proc. FLAIRS '96, pages 454\u2013458, Key West, 1996."},{"key":"24_CR7","unstructured":"D. Fuchs and J. Denzinger. Cooperation in theorem proving by loosely coupled heuristics. Technical Report SR-97-03 (ftp:\/\/ftp.uni-kl.de\/reports_unikl\/computer_science\/SEKI\/1997\/Fuchs.SR-97-03.ps.gz), University of Kaiserslautern, Kaiserslautern, 1997."},{"key":"24_CR8","unstructured":"D. Fuchs. Coupling saturation-based provers by exchanging positive\/negative information. Technical Report SR-97-07 (ftp:\/\/ftp.unikl.de\/reports_uni-kl\/computer_science\/SEKI\/1997\/Fuchs.SR-97-07.ps.gz), University of Kaiserslautern, Kaiserslautern, 1997."},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"D. Fuchs. Inference Rights for Controlling Search in Generating Theorem Provers. In Proc. EPIA '97, pages 25\u201336, Coimbra, 1997. LNAI 1323.","DOI":"10.1007\/BFb0023908"},{"key":"24_CR10","volume-title":"Technical Report ANL-94\/6","author":"W. McCune","year":"1994","unstructured":"W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL-94\/6, Argonne National Laboratory, Argonne, 1994."},{"key":"24_CR11","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":"24_CR12","unstructured":"G. Sutcliffe. A heterogeneous parallel deduction system. In Proc. FGCS'92 Workshop W3, 1992."},{"key":"24_CR13","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","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0052379","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T02:33:33Z","timestamp":1555641213000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0052379"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643012","9783540697213"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0052379","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}