{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:22:03Z","timestamp":1753888923260},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540552536"},{"type":"electronic","value":"9783540468035"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55253-7_22","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T04:57:07Z","timestamp":1330232227000},"page":"371-389","source":"Crossref","is-referenced-by-count":31,"title":["Basic superposition is complete"],"prefix":"10.1007","author":[{"given":"Robert","family":"Nieuwenhuis","sequence":"first","affiliation":[]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"22_CR1","unstructured":"L. Bachmair, N. Dershowitz, D. Plaisted: Completion without failure. In H. Ait-Kaci and M. Nivat, editors, Resolution of equations in algebraic structures, vol 2: Rewriting Techniques, pp 1-30, Academic Press, (1989)."},{"key":"22_CR2","first-page":"162","volume":"516","author":"L. Bachmair","year":"1991","unstructured":"L. Bachmair, H. Ganzinger: Completion of first-order clauses with equality, (final version) 2nd Intl. Workshop on Conditional and Typed Term Rewriting, Montreal, LNCS 516, pp. 162\u2013181, (1991).","journal-title":"LNCS"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"H. Comon: Solving Symbolic Ordering Constraints. In proc. 5th IEEE Symp. Logic in Comp. Sc. Philadelphia. (June 1990).","DOI":"10.1142\/S0129054190000278"},{"key":"22_CR4","volume-title":"Handbook of Theoretical Computer Science, vol. B: Formal Methods and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz, J-P. Jouannaud: Rewrite systems, in Handbook of Theoretical Computer Science, vol. B: Formal Methods and Semantics. (J. van Leeuwen, ed.), North Hollad, Amsterdam, 1990."},{"key":"22_CR5","unstructured":"N. Dershowitz, J-P. Jouannaud: Notations for Rewriting. in Bulletin of the EATCS, no. 43, Feb 1991."},{"key":"22_CR6","unstructured":"J. Hsiang, M. Rusinowitch: Proving refutational completeness of theorem proving strategies: The transfinite semantic tree method. Submitted for publication (1989)."},{"key":"22_CR7","unstructured":"J.M. Hullot: Compilation de Formes Canoniques dans les Teories Equationnelles, These de 3eme Cycle, Universite de Paris Sud, 1980."},{"key":"22_CR8","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. E. Knuth","year":"1970","unstructured":"D.E. Knuth, P.B. Bendix: Simple word problems in universal algebras. J. Leech, editor, Computational Problems in Abstract Algebra, 263\u2013297, Pergamon Press, Oxford, 1970."},{"issue":"3","key":"22_CR9","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"C. Kirchner and H. Kirchner, M. Rusinowitch: Deduction with Symbolic Constraints. Revue Francaise d'Intelligence Artificielle. Vol 4. No. 3. pp. 9\u201352. Special issue on automatic deduction. (1990).","journal-title":"Revue Francaise d'Intelligence Artificielle"},{"key":"22_CR10","unstructured":"R. Nieuwenhuis: First-order completion techniques. Research report UPC-LSI, 1991."},{"key":"22_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0020-0190(91)90053-K","volume":"39","author":"R. Nieuwenhuis","year":"1991","unstructured":"R. Nieuwenhuis, P. Nivela: Efficient deduction in equality Horn logic by Horncompletion, Information Processing Letters, no. 39, pp. 1\u20136, July 1991.","journal-title":"Information Processing Letters"},{"key":"22_CR12","first-page":"246","volume":"516","author":"R. Nieuwenhuis","year":"1991","unstructured":"R. Nieuwenhuis, F. Orejas: Clausal Rewriting. 2nd Intl. Workshop on Conditional and Typed Term Rewriting, Montreal, LNCS 516, pp. 246\u2013261, (1991).","journal-title":"LNCS"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis, F. Orejas, A. Rubio: TRIP: an implementation of clausal rewriting. In Proc. 10th Int. Conf. on Automated Deduction. Kaiserslautern, 1990. LNCS, pp 667\u2013668.","DOI":"10.1007\/3-540-52885-7_133"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis, A. Rubio: Theorem Proving with Ordering Constrained Clauses. Research report UPC-LSI, 1991. (submitted).","DOI":"10.1007\/3-540-55602-8_186"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"G.E. Peterson: Complete Sets of Reductions with Constraints. In Proc. 10th Int. Conf. on Automated Deduction. Kaiserslautern, 1990. LNCS, pp 381\u2013395.","DOI":"10.1007\/3-540-52885-7_101"},{"key":"22_CR16","volume-title":"Report 87-R-128","author":"M. Rusinowitch","year":"1987","unstructured":"M. Rusinowitch: Theorem-proving with resolution and superposition: an extension of Knuth and Bendix procedure as a complete set of inference rules. Report 87-R-128, CRIN, Nancy, 1987."}],"container-title":["Lecture Notes in Computer Science","ESOP '92"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55253-7_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:58:27Z","timestamp":1605628707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55253-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540552536","9783540468035"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-55253-7_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}