{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:21:07Z","timestamp":1725456067899},"publisher-location":"Berlin\/Heidelberg","reference-count":25,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354058403X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0016860","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:52:57Z","timestamp":1132732377000},"page":"285-301","source":"Crossref","is-referenced-by-count":21,"title":["Buchberger's algorithm: A constraint-based completion procedure"],"prefix":"10.1007","author":[{"given":"Leo","family":"Bachmair","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Ganzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical equational proofs","author":"L. Bachmair","year":"1991","unstructured":"Leo Bachmair, 1991. Canonical equational proofs. Birkh\u00e4user, Boston."},{"key":"21_CR2","first-page":"5","volume-title":"LNCS 230","author":"L. Bachmair","year":"1986","unstructured":"Leo Bachmair and Nachum Dershowitz, 1986. Commutation, transformation, and termination. In Proc. 8th Conf. on Automated Deduction, Oxford, LNCS 230, pp. 5\u201320. Springer-Verlag, Berlin."},{"key":"21_CR3","first-page":"331","volume-title":"Inference rules for rewrite-based first-order theorem proving","author":"L. Bachmair","year":"1987","unstructured":"Leo Bachmair and Nachum Dershowitz, 1987. Inference rules for rewrite-based first-order theorem proving. In Proc. Second IEEE Symp. Logic in Computer Science (Ithaca, New York), pp. 331\u2013337. IEEE Comp. Soc. Press."},{"key":"21_CR4","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/174652.174655","volume":"41","author":"L. Bachmair","year":"1994","unstructured":"Leo Bachmair and Nachum Dershowitz, 1994. Equational inference, canonical proofs, and proof orderings. Journal of the ACM, Vol. 41, pp. 236\u2013276.","journal-title":"Journal of the ACM"},{"key":"21_CR5","volume-title":"Technical Report MPI-I-93-250","author":"L. Bachmair","year":"1993","unstructured":"Leo Bachmair and Harald Ganzinger, 1993. Ordered chaining for total orderings. Technical Report MPI-I-93-250, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken. To appear in Proc. CADE'94."},{"issue":"No.3","key":"21_CR6","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Leo Bachmair and Harald Ganzinger, 1994. Rewrite-based equational theorem proving with selection and simplification. J. Logic and Computation, Vol. 4, No. 3, pp. 217\u2013247.","journal-title":"J. Logic and Computation"},{"key":"21_CR7","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L. Bachmair","year":"1994","unstructured":"Leo Bachmair, Harald Ganzinger and Uwe Waldmann, 1994. Theorem proving for hierarchic first-order theories. Applicable Algebra in Engineering, Communication and Computing, Vol. 5, pp. 193\u2013212.","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"21_CR8","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","volume":"1","author":"L. Bachmair","year":"1985","unstructured":"Leo Bachmair and David Plaisted, 1985. Termination orderings for associative-commutative rewriting systems. J. Symbolic Computation, Vol. 1, pp. 329\u2013349.","journal-title":"J. Symbolic Computation"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Thomas Becker and Volker Weispfenning, 1993. Gr\u00f6bner bases: a computational approach to commutative algebra. Springer-Verlag.","DOI":"10.1007\/978-1-4612-0913-3"},{"key":"21_CR10","volume-title":"PhD thesis","author":"B. Buchberger","year":"1965","unstructured":"Bruno Buchberger, 1965. An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-Dimensional Ideal. PhD thesis, University of Innsbruck, Austria. (In German)."},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Bruno Buchberger, 1985. Gr\u00f6bner bases: an algorithmic method in polynomial ideal theory. In N.K. Bose, editor, Recent Trends in Multidimensional Systems theory, pp. 184\u2013232. Reidel.","DOI":"10.1007\/978-94-009-5225-6_6"},{"key":"21_CR12","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(87)80020-2","volume":"3","author":"B. Buchberger","year":"1987","unstructured":"Bruno Buchberger, 1987. History and Basic Features of the Critical Pair \/ Completion Procedure. J. Symbolic Computation, Vol. 3, pp. 3\u201338.","journal-title":"J. Symbolic Computation"},{"key":"21_CR13","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/978-3-7091-3406-1","volume-title":"Computer Algebra","author":"B. Buchberger","year":"1982","unstructured":"Bruno Buchberger and R\u00fcdiger Loos, 1982. Algebraic simplification. In Computer Algebra, pp. 14\u201343. Springer-Verlag, Berlin."},{"key":"21_CR14","volume-title":"LNCS 488","author":"R. B\u00fcndgen","year":"1991","unstructured":"Reinhard B\u00fcndgen, 1991. Simulating Buchberger's Algorithm by a Knuth-Bendix Completion Procedure. In Proc. Fourth International Conference on Rewriting Techniques and Applications (Como, Italy), LNCS 488, Berlin, Springer-Verlag."},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud, 1990. Rewrite Systems. In, Handbook of Theoretical Computer Science, vol. B, pp. 243\u2013309. North-Holland.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science, vol. 351","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-50939-9_136","volume-title":"Proc. TAPSOFT '89, Barcelona 1989, volume II","author":"H. Ganzinger","year":"1989","unstructured":"Harald Ganzinger, 1989. Order-Sorted Completion: The Many-Sorted Way (Extended Abstract). In J. D\u00edaz, F. Orejas, editors, Proc. TAPSOFT '89, Barcelona 1989, volume II, Lecture Notes in Computer Science, vol. 351, pp. 244\u2013258, Berlin, Springer-Verlag. Full version in TCS, volume 89, 1991."},{"key":"21_CR17","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","volume":"25","author":"J. Hsiang","year":"1985","unstructured":"Jieh Hsiang, 1985. Refutational theorem proving using term-rewriting systems. Artificial Intelligence, Vol. 25, pp. 255\u2013300.","journal-title":"Artificial Intelligence"},{"issue":"No.4","key":"21_CR18","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J. Jouannaud","year":"1986","unstructured":"Jean-Pierre Jouannaud and H\u00e9l\u00e8ne Kirchner, 1986. Completion of a Set of Rules Modulo a Set of Equations. SIAM Journal on Computing, Vol. 15, No. 4, pp. 1155\u20131194.","journal-title":"SIAM Journal on Computing"},{"key":"21_CR19","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/S0747-7171(88)80020-8","volume":"6","author":"A. Kandri-Rody","year":"1988","unstructured":"Abdeligah Kandri-Rody and Deepak Kapur, 1988. Computing a Gr\u00f6bner basis of a polynomial ideal over a Euclidean domain. J. Symbolic Computation, Vol. 6, pp. 37\u201357.","journal-title":"J. Symbolic Computation"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Deepak Kapur and Paliath Narendran, 1985. An equational approach to theorem proving in first-order predicate calculus. In Proc. Ninth International Joint Conference on Artificial Intelligence, pp. 1146\u20131153, Los Angeles, CA.","DOI":"10.1145\/1012497.1012521"},{"issue":"No.3","key":"21_CR21","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Claude Kirchner, Helene Kirchner and Michael Rusinowitch, 1990. Deduction with symbolic constraints. Revue Fran\u00e7aise d'Intelligence Artificielle, Vol. 4, No. 3, pp. 9\u201352.","journal-title":"Revue Fran\u00e7aise d'Intelligence Artificielle"},{"key":"21_CR22","first-page":"214","volume-title":"Term reduction systems and algebraic algorithms","author":"L. R\u00fcdiger","year":"1981","unstructured":"R\u00fcdiger Loos, 1981. Term reduction systems and algebraic algorithms. In Proceedings of the Fifth GI Workshop on Artificial Intelligence, pp. 214\u2013234, Berlin, Springer-Verlag. Available as Informatik Fachberichte, Vol. 47."},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Claude March\u00e9, 1994. Normalised rewriting and normalised completion. In Proc. IEEE Symposium on Logic in Computer Science. IEEE Comp. Soc. Press. To appear.","DOI":"10.1109\/LICS.1994.316050"},{"key":"21_CR24","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson","year":"1981","unstructured":"Gerald E. Peterson and Mark E. Stickel, 1981. Complete sets of reductions for some equational theories. Journal of the ACM, Vol. 28, pp. 233\u2013264.","journal-title":"Journal of the ACM"},{"key":"21_CR25","unstructured":"Hantao Zhang, 1992. A new method for the Boolean ring based theorem proving. In Proc. Second Int. Symposium on Artificial Intelligence and Mathematics."}],"container-title":["Lecture Notes in Computer Science","Constraints in Computational Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0016860.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:37:02Z","timestamp":1607549822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0016860"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354058403X"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0016860","relation":{},"subject":[]}}