{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T08:58:56Z","timestamp":1725699536587},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540183884"},{"type":"electronic","value":"9783642730054"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1987]]},"DOI":"10.1007\/978-3-642-73005-4_26","type":"book-chapter","created":{"date-parts":[[2012,8,9]],"date-time":"2012-08-09T01:11:18Z","timestamp":1344474678000},"page":"241-250","source":"Crossref","is-referenced-by-count":4,"title":["Theopogles \u2014 A Theorem Prover Based on First-Order Polynomials and a Special Knuth-Bendix Procedure"],"prefix":"10.1007","author":[{"given":"Juergen","family":"Mueller","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Buchberger, B.: Basic Features and Development of the Critical-Pair\/Completion Procedure, 1. Int. Conf. on Rewriting Techniques and Applications (RTA), Dijon, May 1985, Springer LNCS 202, 1\u201345.","DOI":"10.1007\/3-540-15976-2_1"},{"key":"26_CR2","volume-title":"N.Y","author":"CL Chang","year":"1973","unstructured":"Chang, C.L. and Lee, R.C.T.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, N.Y. 1973."},{"key":"26_CR3","unstructured":"Corbin, J., Bidoit, M.: A Rehabilitation of Robinson\u2019s Unification Algorithm, in Information Processing 83, R.E.A. Mason (ed.), Elevier Sc. Pub. ( North Holland ), 909\u2013914"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Fribourg, L.: A Superposition Oriented Theorem Prover, TCS35 (1985), 124\u2013164.","DOI":"10.1016\/0304-3975(85)90011-8"},{"key":"26_CR5","unstructured":"H82] Hsiang, J.: Topics in Automated Theorem Proving and Program Generation Ph.D. Thesis, Dec. 1982, University of Illinois at Urbana-Champaign, UIUCDCS-R-82\u20131113."},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Hsiang, J.: Two Results in Term Rewriting Theorem Proving, Proc. RTA, Dijon, May1985, Springer LNCS 202, 301\u2013324","DOI":"10.1007\/3-540-15976-2_15"},{"key":"26_CR7","volume-title":"Theorem Proving, Proc","author":"J Hsiang","year":"1983","unstructured":"Hsiang, J. and Dershowitz, N.: Rewrite Methods for Clausal and Non-Clausal Theorem Proving, Proc. of the 10. EATCS Int. Colloq. on Automata, Languages and Programming (ICALP ), Spain 1983."},{"key":"26_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, Journal of Computer and System Sciences 23 (1981), 11\u201321.","journal-title":"Journal of Computer and System Sciences"},{"key":"26_CR9","first-page":"263","volume-title":"Simple Word Problems in Universal Algebras in Computational Problems in Abstract Algebras (Ed. J","author":"DE Knuth","year":"1970","unstructured":"Knuth, D.E. and Bendix, P.B.: Simple Word Problems in Universal Algebras in Computational Problems in Abstract Algebras (Ed. J. Leech ), Pergammon Press, 1970, 263\u2013297."},{"key":"26_CR10","first-page":"1985","volume-title":"see also (short version) Proc. of the IJCAI-85","author":"D Kapur","year":"1985","unstructured":"Kapur, D. and Narendran, P.: An Equational Approach to Theorem Proving in First-Order Predicat Calculus, 84CRD322, General Electric Corporate Research and Development Report, Schenectady, N.Y., Sept.1985. see also (short version) Proc. of the IJCAI-85, Los Angeles, CA, Aug. 1985."},{"key":"26_CR11","volume-title":"Amsterdam","author":"[L78] Loveland, B.W.","year":"1978","unstructured":"L78] Loveland, B.W.: Automated Theorem Proving: a logical basis, North Holland, Amsterdam 1978."},{"key":"26_CR12","unstructured":"Pa85] Paul, E On Solving the Equality Problem in Theories defined by Horn Clauses, Poc. Eurocal-85, Linz, Austria."},{"key":"26_CR13","first-page":"191","volume":"2","author":"Seventy-Five Problems for Testing Automatic","year":"1986","unstructured":"Seventy-Five Problems for Testing Automatic Theorem Provers, JAR 2 (1986), 191\u2013216.","journal-title":"Theorem Provers"},{"key":"26_CR14","volume-title":"Automated Reasoning, Prentice-Hall","author":"L Wos","year":"1984","unstructured":"Wos, L. et al., Automated Reasoning, Prentice-Hall, 1984."}],"container-title":["Informatik-Fachberichte","GWAI-87 11th German Workshop on Artifical Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-73005-4_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,25]],"date-time":"2020-11-25T02:06:01Z","timestamp":1606269961000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-73005-4_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987]]},"ISBN":["9783540183884","9783642730054"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-73005-4_26","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1987]]}}}