{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:06:06Z","timestamp":1725663966389},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584674"},{"type":"electronic","value":"9783540489795"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58467-6_30","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:13:48Z","timestamp":1330272828000},"page":"343-354","source":"Crossref","is-referenced-by-count":10,"title":["Goal oriented equational theorem proving using team work"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Denzinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthias","family":"Fuchs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"30_CR1","first-page":"184","volume":"429","author":"D. Anantharaman","year":"1990","unstructured":"Anantharaman, D.; Andrianarievelo, N.: Heuristical criteria in refutational theorem proving, Proc. DISCO '90, LNCS 429, 1990, pp. 184\u2013193.","journal-title":"LNCS"},{"key":"30_CR2","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":"LNCS"},{"key":"30_CR3","volume-title":"Coll. on the Resolution of Equations in Algebraic Structures","author":"L. Bachmair","year":"1987","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":"30_CR4","first-page":"272","volume":"722","author":"M.P. Bonacina","year":"1993","unstructured":"Bonacina, M.P.; Hsiang, J.: The clause diffusion methodology for distributed deduction, Proc. DISCO '92, LNCS 722, 1993, pp. 272\u2013287.","journal-title":"LNCS"},{"unstructured":"Bl\u00e4sius, K.H.: Equality reasoning based on graphs, Ph.D. thesis, University of Kaiserslautern, 1986.","key":"30_CR5"},{"doi-asserted-by":"crossref","unstructured":"Chalin, J.; Anantharaman, S. et al.: REVEAL \u2014 a user's guide, Tech. rep. LIFO.94-12, University of Orleans, 1994.","key":"30_CR6","DOI":"10.1108\/eb047920"},{"unstructured":"Cleve, J.; Hutter, D.: Guiding equational proofs by attribute functions, SEKI-Report SR-93-15, University of Saarbr\u00fccken, 1993.","key":"30_CR7"},{"unstructured":"Denzinger, J.: Teamwork: A method to design distributed knowledge based theorem provers (in German), Ph.D. thesis, University of Kaiserslautern, 1993.","key":"30_CR8"},{"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":"30_CR9"},{"unstructured":"Fuchs, M.: The application of goal-oriented heuristics for proving equational theorems via the unfailing Knuth-Bendix completion procedure. A case study: lattice ordered groups, SEKI-Report SR-94-02, University of Kaiserslautern, 1994.","key":"30_CR10"},{"issue":"4","key":"30_CR11","first-page":"798","volume":"27","author":"G. Hnet","year":"1980","unstructured":"Hnet, G.: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems, J. of ACM 27, No. 4, 1980, pp. 798\u2013821.","journal-title":"J. of ACM"},{"unstructured":"Kimth, D.E.; Bendix, P.B.: Simple Word Problems in Universal Algebra, Computational Algebra, J. Leech, Pergamon Press, 1970, pp. 263\u2013297.","key":"30_CR12"},{"unstructured":"Kokorin, A.I.; Kopytov, V.M.: Fully ordered groups, Halsted Press, 1974.","key":"30_CR13"},{"key":"30_CR14","first-page":"781","volume":"607","author":"E. Lusk","year":"1992","unstructured":"Lusk, E.; Wos, L.: Benchmark problems in which equality plays the major role, Proc. CADE-11, LNAI 607, 1992, pp. 781\u2013785.","journal-title":"LNAI"},{"doi-asserted-by":"crossref","unstructured":"McCune, W.W.: OTTER 3.0 Reference manual and Guide, Tech. rep. ANL-94\/6, Argonne National Laboratory, 1994.","key":"30_CR15","DOI":"10.2172\/10129052"},{"unstructured":"Socher, R.: A Goal Oriented Strategy Based on Completion, Tech. rep. TR#91\/18, SUNY at Stony Brook, 1991.","key":"30_CR16"},{"key":"30_CR17","doi-asserted-by":"crossref","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","KI-94: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58467-6_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T07:29:53Z","timestamp":1640935793000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58467-6_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584674","9783540489795"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-58467-6_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}