{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:08:18Z","timestamp":1784844498870,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540592006","type":"print"},{"value":"9783540492238","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59200-8_72","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:07:18Z","timestamp":1330258038000},"page":"397-402","source":"Crossref","is-referenced-by-count":24,"title":["DISCOUNT: A system for distributed equational deduction"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Avenhaus","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00f6rg","family":"Denzinger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthias","family":"Fuchs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"31_CR1","first-page":"62","volume":"690","author":"J. Avenhaus","year":"1993","unstructured":"Avenhaus, J.; Denzinger, J.: Distributing equational theorem proving, Proc. 5th RTA, Montreal, LNCS 690, 1993, pp. 62\u201376.","journal-title":"Proc. 5th RTA, Montreal, LNCS"},{"key":"31_CR2","unstructured":"Bachmair, L.; Dershowitz, N.; Plaisted, D.A.: Completion without Failure, Coll. on the Resolution of Equations in Algebraic Structures, Austin (1987), Academic Press, 1989."},{"key":"31_CR3","unstructured":"Bonacina, M.P.; Hsiang, J.: The clause-diffusion methodology for distributed deduction, Fundamenta Informaticae, Special issue on term rewriting systems, D.A. Plaisted (ed.), in press"},{"key":"31_CR4","unstructured":"Denzinger, J.: Teamwork: A method to design distributed knowledge based theorem provers (in German), Ph.D. thesis, University of Kaiserslautern, 1993."},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"Denzinger, J.; Fuchs, M.: Goal oriented equational theorem proving using teamwork, Proc. 18th KI-94, Saarbr\u00fccken, LNAI 861, 1994, pp. 343\u2013354; also available as SEKI-Report SR-94-04, University of Kaiserslautern, 1994.","DOI":"10.1007\/3-540-58467-6_30"},{"key":"31_CR6","unstructured":"Denzinger, J.; Pitz, W.: Das DISCOUNT-System: Benutzerhandbuch, SEKI working paper SWP-92-16, Universit\u00e4t Kaiserslautern, 1992."},{"key":"31_CR7","unstructured":"Denzinger, J.; Schulz, S.: Analysis and Representation of Equational Proofs Generated by a Distributed Completion Based Proof System, SEKI-Report SR-94-05, University of Kaiserslautern, 1994."},{"key":"31_CR8","unstructured":"Denzinger, J.; Schulz, S.: Recording, Analyzing and Presenting Distributed Deduction Processes, Proc. PASCO '94, Linz, 1994, pp. 114\u2013123."},{"key":"31_CR9","first-page":"54","volume":"267","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J.; Rusinowitch, M.: On word problems in equational theories, Proc. 14th ICALP, Karlsruhe, LNCS 267, 1987, pp. 54\u201371.","journal-title":"Proc. 14th ICALP, Karlsruhe, LNCS"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Knuth, D.E.; Bendix, P.B.: Simple Word Problems in Universal Algebra, Computational Algebra, J. Leech, Pergamon Press, 1970, pp. 263\u2013297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"31_CR11","unstructured":"Lind, J.: Sicheres Broadcasting, Projektarbeit, Fachbereich Informatik, Universit\u00e4t Kaiserslautern, 1993."},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Stickel, M.E.: A case study of theorem proving by the Knuth-Bendix method: Discovering that x3=x implies ring commutativity, Proc. CADE 7, Napa, CA, USA, 1984, LNCS 170, pp. 248-258","DOI":"10.1007\/978-0-387-34768-4_15"},{"key":"31_CR13","unstructured":"Tarski, A.: Logic, Semantics, Metamathematics, Oxford University Press, 1956"},{"key":"31_CR14","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00881872","volume":"11","author":"H. Zhang","year":"1993","unstructured":"Zhang, H.: Automated proofs of equality problems in Overbeek's competition, JAR 11, 1993, pp. 333\u2013351.","journal-title":"JAR"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59200-8_72.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:26:04Z","timestamp":1605630364000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59200-8_72"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540592006","9783540492238"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-59200-8_72","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}