{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:21:22Z","timestamp":1725898882461},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540591320"},{"type":"electronic","value":"9783540491989"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014420","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T18:08:44Z","timestamp":1134324524000},"page":"1-29","source":"Crossref","is-referenced-by-count":5,"title":["Combining algebra and universal algebra in first-order theorem proving: The case of commutative rings"],"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"}]},{"given":"J\u00fcrgen","family":"Stuber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,26]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"L. Bachmair and N. Dershowitz, 1986. Commutation, transformation, and termination. Proc. 8th Conf. on Automated Deduction, San Diego, CA, LNCS 230, pp. 5\u201320. Springer.","DOI":"10.1007\/3-540-16780-3_76"},{"key":"1_CR2","series-title":"Technical Report MPI-I-93-267","volume-title":"Associative-commutative superposition","author":"L. Bachmair","year":"1993","unstructured":"L. Bachmair and H. Ganzinger, 1993. Associative-commutative superposition. Technical Report MPI-I-93-267, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken. To appear in Proc. CTRS Workshop 1994."},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger, 1994a. Buchberger's algorithm: A constraint-based completion procedure. Proc. 1st Int. Conf. on Constraints in Computational Logics, Munich, Germany, LNCS 845, pp. 285\u2013301. Springer.","DOI":"10.1007\/BFb0016860"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger, 1994b. Ordered chaining for total orderings. Proc. 12th Int. Conf. on Automated Deduction, Nancy, France, LNCS 814, pp. 435\u2013450. Springer.","DOI":"10.1007\/3-540-58156-1_32"},{"issue":"3","key":"1_CR5","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and H. Ganzinger, 1994c. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation4(3): 217\u2013247. Revised version of Technical Report MPI-I-93-250, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"1_CR6","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","volume":"1","author":"L. Bachmair","year":"1985","unstructured":"L. Bachmair and D. Plaisted, 1985. Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation1: 329\u2013349.","journal-title":"Journal of Symbolic Computation"},{"issue":"3\/4","key":"1_CR7","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair, H. Ganzinger and U. Waldmann, 1994. Refutational theorem proving for hierarchic first-order theories. Applicable Algebra in Engineering, Communication and Computing5(3\/4): 193\u2013212. Earlier version: Theorem Proving for Hierarchic First-Order Theories. Proc. 3rd Int. Conf. on Algebraic and Logic Programming, Volterra, Italy, LNCS 632. Springer, 1992.","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"1_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"L. Bachmair, 1991. Canonical Equational Proofs. Birkh\u00e4user, Boston."},{"key":"1_CR9","first-page":"83","volume-title":"Machine Intelligence 11","author":"R. S. Boyer","year":"1988","unstructured":"R. S. Boyer and J. S. Moore, 1988. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In J. E. Hayes, D. Michie and J. Richards (eds), Machine Intelligence 11, chapter 5, pp. 83\u2013124. Clarendon Press, Oxford."},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"B. Buchberger and R. Loos, 1983. Algebraic simplification. Computer Algebra: Symbolic and Algebraic Computation, 2nd edn, pp. 11\u201343. Springer.","DOI":"10.1007\/978-3-7091-7551-4_2"},{"key":"1_CR11","volume-title":"PhD thesis","author":"B. Buchberger","year":"1965","unstructured":"B. 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":"1_CR12","doi-asserted-by":"crossref","unstructured":"B. Buchberger, 1985. Gr\u00f6bner bases: An algorithmic method in polynomial ideal theory. In N. K. Bose (ed.), Recent Trends in Multidimensional Systems Theory, chapter 6, pp. 184\u2013232. D. Reidel Publishing Company.","DOI":"10.1007\/978-94-009-5225-6_6"},{"key":"1_CR13","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(87)80020-2","volume":"3","author":"B. Buchberger","year":"1987","unstructured":"B. Buchberger, 1987. History and basic features of the critical pair\/completion procedure. Journal of Symbolic Computation3: 3\u201338.","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert, 1990. A resolution principle for clauses with constraints. Proc. 10th Int. Conf. on Automated Deduction, Kaiserslautern, Germany, LNCS 449, pp. 178\u2013192. Springer.","DOI":"10.1007\/3-540-52885-7_87"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud, 1990. Rewrite systems. In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics, chapter 6, pp. 243\u2013320. Elsevier\/MIT Press.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"1_CR16","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/S0747-7171(88)80020-8","volume":"6","author":"A. Kandri-Rody","year":"1988","unstructured":"A. Kandri-Rody and D. Kapur, 1988. Computing a Gr\u00f6bner basis of a polynomial ideal over a euclidean domain. Journal of Symbolic Computation6: 19\u201336.","journal-title":"Journal of Symbolic Computation"},{"issue":"3","key":"1_CR17","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"C. Kirchner, H. Kirchner and M. Rusinowitch, 1990. Deduction with symbolic constraints. Revue Fran\u00e7aise d'Intelligence Artificielle4(3): 9\u201352. Special issue on automatic deduction.","journal-title":"Revue Fran\u00e7aise d'Intelligence Artificielle"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"P. Le Chenadec, 1984. Canonical forms in finitely presented algebras. Proc. 7th Int. Conf. on Automated Deduction, Napa, CA, LNCS 170, pp. 142\u2013165. Springer. Book version published by Pitman, London, 1986.","DOI":"10.1007\/978-0-387-34768-4_9"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"R. Loos, 1981. Term reduction systems and algebraic algorithms. Proc. 5th GI Workshop on Artificial Intelligence, Bad Honnef, Informatik Fachberichte 47, pp. 214\u2013234. Springer.","DOI":"10.1007\/978-3-662-02328-0_20"},{"key":"1_CR20","first-page":"394","volume-title":"Normalised rewriting and normalised completion","author":"G. March\u00e9","year":"1994","unstructured":"G. March\u00e9, 1994. Normalised rewriting and normalised completion. Proc. 9th Ann. IEEE Symp. on Logic in Computer Science, Paris, pp. 394\u2013403. IEEE Computer Society Press."},{"issue":"2","key":"1_CR21","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"2","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen, 1979. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems2(2): 245\u2013257.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio, 1994. AC-supeiposition with constraints: no AC-unifiers needed. Proc. 12th Int. Conf. on Automated Deduction, Nancy, France, LNCS 814, pp. 545\u2013559. Springer.","DOI":"10.1007\/3-540-58156-1_40"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby and N. Shankar, 1992. PVS: A prototype verification system, 11th Int. Conf. on Automated Deduction, Saratoga Springs, NY, LNCS 607, pp. 748\u2013752. Springer.","DOI":"10.1007\/3-540-55602-8_217"},{"issue":"2","key":"1_CR24","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson","year":"1981","unstructured":"G. E. Peterson and M. E. Stickel, 1981. Complete sets of reductions for some equational theories. Journal of the ACM28(2): 233\u2013264.","journal-title":"Journal of the ACM"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"L. Vigneron, 1994. Associative-commutative deduction with constraints. Proc. 12th Int. Conf. on Automated Deduction, Saratoga Springs, NY, LNCS 814, pp. 530\u2013544. Springer.","DOI":"10.1007\/3-540-58156-1_39"},{"key":"1_CR26","series-title":"Technical Report MPI-I-92-216","volume-title":"First-order theorem proving modulo equations","author":"U. Wertz","year":"1992","unstructured":"U. Wertz, 1992. First-order theorem proving modulo equations. Technical Report MPI-I-92-216, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken."}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Data Type Specification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014420","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T14:03:17Z","timestamp":1586613797000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014420"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540591320","9783540491989"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/bfb0014420","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}