{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:12:08Z","timestamp":1725631928399},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540517436"},{"type":"electronic","value":"9783642751004"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/978-3-642-75100-4_11","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T18:09:29Z","timestamp":1320862169000},"page":"92-101","source":"Crossref","is-referenced-by-count":0,"title":["Eqtheopogles A Completion Theorem Prover for PL1EQ"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Denzinger","sequence":"first","affiliation":[]},{"given":"J\u00fcrgen","family":"M\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","volume-title":"Academic Press","author":"CL Chang","year":"1973","unstructured":"Chang, C.L.; Lee, R.C.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973."},{"key":"11_CR2","volume-title":"University of Kaiserslautern","author":"J Denzinger","year":"1987","unstructured":"Denzinger, J.: Implementation of a Theorem Prover Based on Rewriting- Techniques (in German), project-report, University of Kaiserslautern, 1987."},{"key":"11_CR3","volume-title":"Eqtheopogles","author":"J Denzinger","year":"1988","unstructured":"Denzinger, J.: EQTHEOPOGLES (in German), M.S. Thesis, University of Kaiserslautern, 1988."},{"key":"11_CR4","unstructured":"Denzinger, J.; Kassel, S.; M\u00fcller, J.: Proving Theorems with the CTP (EQ-)THEOPOGLES, Overview, user manual and solutions, technical report, University of Kaiserslautern, to appear 1989."},{"key":"11_CR5","volume-title":"University of Kaiserslautern","author":"J Denzinger","year":"1987","unstructured":"Denzinger, J.; M\u00fcller, J.: THEOPOGLES user manual, University of Kaiserslautern, 1987."},{"key":"11_CR6","volume-title":"report University of Illinois","author":"J Hsiang","year":"1982","unstructured":"Hsiang, J.: Topics in Automated Theorem Proving and Program Generation, report University of Illinois, 1982."},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0747-7171(87)80024-X","volume":"3","author":"J Hsiang","year":"1987","unstructured":"Hsiang, J.: Rewrite Method for Theorem Proving in First Order Theory with Equality, J. of Symbolic Computation 3, 1987, pp. 133\u2013151.","journal-title":"J. of Symbolic Computation"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G Huet","year":"1981","unstructured":"Huet, G.: A Complete Proof of Correctness of the Knuth-Bendix Completion algorithm, J. of Comp, and System Sciences 23, 1981, pp. 11\u201321.","journal-title":"J. of Comp, and System Sciences"},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/S0747-7171(88)80019-1","volume":"6","author":"D Kapur","year":"1988","unstructured":"Kapur, D.; Musser, D.R.; Narendran, P.: Only Prime Superpositions Need be Considered in the Knuth-Bendix Completion Procedure, J. of Symb. Comp. 6, 1988, pp. 19\u201336.","journal-title":"J. of Symb. Comp"},{"key":"11_CR10","volume-title":"Proceedings CADE","author":"D Kapur","year":"1988","unstructured":"Kapur, D.; Zhang, H.: First-Order Theorem Proving using Conditional Rewrite Rules, Proceedings CADE, 1988."},{"key":"11_CR11","first-page":"263","volume-title":"Simple Word Problems in Universal Algebra, Computational Algebra","author":"DE Knuth","year":"1970","unstructured":"Knuth, D.E.; Bendix, P.B.: Simple Word Problems in Universal Algebra, Computational Algebra, J.Leach, Pergamon Press, 1970, pp. 263\u2013297."},{"key":"11_CR12","first-page":"209","volume":"1","author":"EL Lusk","year":"1985","unstructured":"Lusk, E.L.; Overbeek, R.A.: Reasoning about Equality, J. of Automated Reasoning 1, 1985, pp. 209\u2013228.","journal-title":"J. of Automated Reasoning"},{"key":"11_CR13","volume-title":"Proceedings CADE","author":"W McCune","year":"1988","unstructured":"McCune, W.: Challenge Equality Problems in Lattice Theory, Proceedings CADE, 1988."},{"key":"11_CR14","first-page":"287","volume-title":"E-resolution: Extension of Resolution to Include the Equality, Proc","author":"JB Morris","year":"1969","unstructured":"Morris, J.B.: E-resolution: Extension of Resolution to Include the Equality, Proc. IJCAI, Washington D.C., 1969, pp. 287\u2013294."},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"M\u00fcller, J.; Socher-Ambrosius, R.: On the Unnecessity of Multiple-Overlaps in Completion Theorem Proving, Proc. 12th GWAI, 1988, Springer IFB 181.","DOI":"10.1007\/978-3-642-74064-0_18"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"M\u00fcller, J.: THEOPOGLES - A Theorem Prover Based on First-Order Polynomials and a Special Knuth-Bendix Procedure, Proc. 11th GWAI, 1987, Springer IFB 152.","DOI":"10.1007\/978-3-642-73005-4_26"},{"key":"11_CR17","volume-title":"Theorem Proving with Rewrite-Techniques, - Methods, Strategies and Comparisons - (in German), Ph.D","author":"J M\u00fcller","year":"1988","unstructured":"M\u00fcller, J.: Theorem Proving with Rewrite-Techniques, - Methods, Strategies and Comparisons - (in German), Ph.D. Thesis, University of Kaiserslautern, 1988."},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"GE Peterson","year":"1983","unstructured":"Peterson, G.E.: A Technique for Establishing Completeness Results in Theorem Proving with Equality, SIAM Journal of Computing 12, 1, 1983, pp. 82\u2013100.","journal-title":"SIAM Journal of Computing"},{"key":"11_CR19","volume-title":"Demonstration automatique par des techniques de reecriture (in French)","author":"M Rusinowitch","year":"1987","unstructured":"Rusinowitch, M.: Demonstration automatique par des techniques de reecriture (in French), These de Doctorat dTtat en Mathematique, Nancy, 1987."},{"key":"11_CR20","first-page":"135","volume":"4","author":"G Robinson","year":"1969","unstructured":"Robinson, G.; Wos, L.: First-order Theorem Proving with Equality, Mach. Intelligence, vol. 4, Edinburgh, 1969, pp. 135\u2013150.","journal-title":"Mach. Intelligence"},{"key":"11_CR21","volume-title":"The Church-Rosser Property in Computer Algebra and Special Theorem Proving: an Investigation of Critical Pair Completion Algorithms, Ph.D","author":"F Winkler","year":"1984","unstructured":"Winkler, F.: The Church-Rosser Property in Computer Algebra and Special Theorem Proving: an Investigation of Critical Pair Completion Algorithms, Ph.D. Thesis, J.-Kepler University Linz, 1984."},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"698","DOI":"10.1145\/321420.321429","volume":"14","author":"L Wos","year":"1967","unstructured":"Wos, L.; Robinson, G.; Carson, D.; Shalla, L.: The Conzept of Demodulation in Theorem Proving, J. of ACM 14, 1967, pp. 698\u2013709.","journal-title":"J. of ACM"}],"container-title":["Informatik-Fachberichte","GWAI-89 13th German Workshop on Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-75100-4_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,25]],"date-time":"2020-11-25T02:29:47Z","timestamp":1606271387000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-75100-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540517436","9783642751004"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-75100-4_11","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1989]]}}}