{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:09:45Z","timestamp":1725664185446},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_102","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:50:25Z","timestamp":1330293025000},"page":"388-402","source":"Crossref","is-referenced-by-count":8,"title":["Theorem proving in cancellative abelian monoids (extended abstract)"],"prefix":"10.1007","author":[{"given":"Harald","family":"Ganzinger","sequence":"first","affiliation":[]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"39_CR1","unstructured":"J\u00fcrgen Avenhaus and Klaus Becker. Conditional rewriting modulo a built-in algebra. SEKI Report SR-92-11, Fachbereich Informatik, Univ. Kaiserslautern, 1992."},{"key":"39_CR2","first-page":"1","volume-title":"LNCS 968","author":"L. Bachmair","year":"1994","unstructured":"Leo Bachmair and Harald Ganzinger. Associative-commutative superposition. In Nachum Dershowitz and Naomi Lindenstrauss, eds., Conditional and Typed Rewrite Systems, 4th International Workshop, CTRS-94, Jerusalem, Israel, July 1994, LNCS 968, pp. 1\u201314. Springer-Verlag."},{"key":"39_CR3","first-page":"435","volume-title":"LNAI 814","author":"L. Bachmair","year":"1994","unstructured":"Leo Bachmair and Harald Ganzinger. Ordered chaining for total orderings. In Alan Bundy, ed., Twelfth International Conference on Automated Deduction, Nancy, France, June\/July 1994, LNAI 814, pp. 435\u2013450. Springer-Verlag."},{"issue":"3","key":"39_CR4","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. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217\u2013247, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"39_CR5","first-page":"83","volume-title":"LNCS 713","author":"L. Bachmair","year":"1993","unstructured":"Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Superposition with simplification as a decision procedure for the monadic class with equality. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, eds., Computational Logic and Proof Theory, Third Kurt G\u00f6del Colloquium, Brno, Czech Republic, August 1993, LNCS 713, pp. 83\u201396. Springer-Verlag."},{"issue":"3\/4","key":"39_CR6","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. Refutational theorem proving for hierarchic first-order theories. Applicable Algebra in Engineering, Communication and Computing, 5(3\/4):193\u2013212, April 1994.","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"key":"39_CR7","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 A. Plaisted. Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation, 1:329\u2013349, 1985.","journal-title":"Journal of Symbolic Computation"},{"key":"39_CR8","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0004-3702(85)90015-3","volume":"27","author":"W. W. Bledsoe","year":"1985","unstructured":"W. W. Bledsoe, K. Kunen, and R. Shostak. Completeness results for inequality provers. Artificial Intelligence, 27:255\u2013288, 1985.","journal-title":"Artificial Intelligence"},{"key":"39_CR9","unstructured":"Robert S. Boyer and J Strother Moore. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In Jean E. Hayes, Donald Michie, and Judith Richards, eds., Machine Intelligence 11: Logic and the acquisition of knowledge, ch. 5, pp. 83\u2013124. Oxford University Press, 1988."},{"key":"39_CR10","first-page":"178","volume-title":"LNAI 449","author":"H. B\u00fcrckert","year":"1990","unstructured":"Hans-J\u00fcrgen B\u00fcrckert. A resolution principle for clauses with constraints. In Mark E. Stickel, ed., 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 1990, LNAI 449, pp. 178\u2013192. Springer-Verlag."},{"key":"39_CR11","volume-title":"LNAI 568","author":"H. B\u00fcrckert","year":"1991","unstructured":"Hans-J\u00fcrgen B\u00fcrckert. A Resolution Principle for a Logic with Restricted Quantifiers. LNAI 568. Springer-Verlag, Berlin, Heidelberg, New York, 1991."},{"key":"39_CR12","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, ed., Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, ch. 6, pp. 243\u2013320. Elsevier Science Publishers B.V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"39_CR13","unstructured":"Harald Ganzinger and Robert Nieuwenhuis. The Saturate system. URL: http:\/\/www.mpi-sb.mpg.de\/SATURATE\/Saturate.html, 1994."},{"key":"39_CR14","volume-title":"Technical Report MPI-I-96-2-001","author":"H. Ganzinger","year":"1996","unstructured":"Harald Ganzinger and Uwe Waldmann. Theorem proving in cancellative abelian monoids. Technical Report MPI-I-96-2-001, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, January 1996. URL: ftp:\/\/ftp.mpi-sb.mpg.de\/pub\/guide\/staff\/uwe\/paper\/MPI-I-96-2-001.ps.gz."},{"key":"39_CR15","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BF00263449","volume":"8","author":"L. M. Hines","year":"1992","unstructured":"Larry M. Hines. Completeness of a prover for dense linear logics. Journal of Automated Reasoning, 8:45\u201375, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"39_CR16","first-page":"416","volume-title":"LNAI 814","author":"L. M. Hines","year":"1994","unstructured":"Larry M. Hines. Str+ve and integers. In Alan Bundy, ed., Twelfth International Conference on Automated Deduction, Nancy, France, June\/July 1994, LNAI 814, pp. 416\u2013430. Springer-Verlag."},{"key":"39_CR17","first-page":"990","volume-title":"Complete inference rules for the cancellation laws (extended abstract)","author":"J. Hsiang","year":"1987","unstructured":"Jieh Hsiang, Micha\u00ebl Rusinowitch, and Ko Sakai. Complete inference rules for the cancellation laws (extended abstract). In John McDermott, ed., Proceedings of the Tenth International Joint Conference on Artificial Intelligence, Milan, Italy, August 1987, vol. 2, pp. 990\u2013992. Morgan Kaufmann Publishers, Inc."},{"issue":"1","key":"39_CR18","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/0304-3975(92)90165-C","volume":"104","author":"J. Jouannaud","year":"1992","unstructured":"Jean-Pierre Jouannaud and Claude March\u00e9. Termination and completion modulo associativity, commutativity and identity. Theoretical Computer Science, 104(1):29\u201351, October 1992.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"39_CR19","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Claude Kirchner, H\u00e9l\u00e8ne Kirchner, and Micha\u00ebl Rusinowitch. Deduction with symbolic constraints. Revue Fran\u00e7aise d'Intelligence Artificielle, 4(3):9\u201352, 1990.","journal-title":"Revue Fran\u00e7aise d'Intelligence Artificielle"},{"key":"39_CR20","first-page":"394","volume-title":"Normalised narrowing and normalised completion","author":"C. March\u00e9","year":"1994","unstructured":"Claude March\u00e9. Normalised narrowing and normalised completion. In Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France, July 1994, pp. 394\u2013403. IEEE Computer Society Press."},{"key":"39_CR21","first-page":"477","volume-title":"LNAI 607","author":"R. Nieuwenhuis","year":"1992","unstructured":"Robert Nieuwenhuis and Albert Rubio. Theorem proving with ordering constrained clauses. In Deepak Kapur, ed., 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 1992, LNAI 607, pp. 477\u2013491. Springer-Verlag."},{"key":"39_CR22","first-page":"545","volume-title":"LNAI 814","author":"R. Nieuwenhuis","year":"1994","unstructured":"Robert Nieuwenhuis and Albert Rubio. AC-superposition with constraints: no AC-unifiers needed. In Alan Bundy, ed., Twelfth International Conference on Automated Deduction, Nancy, France, June\/July 1994, LNAI 814, pp. 545\u2013559. Springer-Verlag."},{"key":"39_CR23","first-page":"748","volume-title":"LNAI 607","author":"S. Owre","year":"1992","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, ed., 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 1992, LNAI 607, pp. 748\u2013752. Springer-Verlag."},{"issue":"2","key":"39_CR24","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson","year":"1981","unstructured":"Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233\u2013264, April 1981.","journal-title":"Journal of the ACM"},{"key":"39_CR25","doi-asserted-by":"crossref","unstructured":"M. M.Richter. Some reordering properties for inequality proof trees. In E. B\u00f6rger, G. Hasenj\u00e4ger, and D. R\u00f6dding, eds., Logic and Machines: Decision Problems and Complexity, 1984, LNCS 171, pp. 183\u2013197. Springer-Verlag.","DOI":"10.1007\/3-540-13331-3_41"},{"key":"39_CR26","first-page":"374","volume-title":"LNCS 690","author":"A. Rubio","year":"1993","unstructured":"Albert Rubio and Robert Nieuwenhuis. A precedence-based total AC-compatible ordering. In Claude Kirchner, ed., Rewriting Techniques and Applications, 5th International Conference, RTA-93, Montreal, Canada, June 1993, LNCS 690, pp. 374\u2013388. Springer-Verlag."},{"key":"39_CR27","first-page":"111","volume-title":"ch. 7: Ensembles complets de r\u00e8gles d'inf\u00e9rence pour les axiomes de r\u00e9gularit\u00e9","author":"M. Rusinowitch","year":"1989","unstructured":"Micha\u00ebl Rusinowitch. D\u00e9monstration Automatique: Techniques de R\u00e9\u00e9criture, ch. 7: Ensembles complets de r\u00e8gles d'inf\u00e9rence pour les axiomes de r\u00e9gularit\u00e9, pp. 111\u2013127. InterEditions, Paris, 1989."},{"key":"39_CR28","doi-asserted-by":"crossref","unstructured":"J\u00fcrgen Stuber. Superposition theorem proving for abelian groups represented as integer modules. To appear in Proc. RTA'96, 1996.","DOI":"10.1007\/3-540-61464-8_41"},{"key":"39_CR29","first-page":"530","volume-title":"LNAI 814","author":"L. Vigneron","year":"1994","unstructured":"Laurent Vigneron. Associative-commutative deduction with constraints. In Alan Bundy, ed., Twelfth International Conference on Automated Deduction, Nancy, France, June\/July 1994, LNAI 814, pp. 530\u2013544. Springer-Verlag."},{"key":"39_CR30","volume-title":"Technical Report MPI-I-92-216","author":"U. Wertz","year":"1992","unstructured":"Ulrich Wertz. First-order theorem proving modulo equations. Technical Report MPI-I-92-216, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, April 1992."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_102.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:33:32Z","timestamp":1619573612000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_102"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_102","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}