{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:44:03Z","timestamp":1725493443328},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664925"},{"type":"electronic","value":"9783540482420"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48242-3_9","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:28:09Z","timestamp":1184588889000},"page":"131-147","source":"Crossref","is-referenced-by-count":2,"title":["Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Waldmann","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Conditional and Typed Rewriting Systems, 4th International Workshop, CTRS-94","author":"L. Bachmair","year":"1994","unstructured":"Leo Bachmair and Harald Ganzinger. Associative-commutative superposition. In Nachum Dershowitz and Naomi Lindenstrauss, eds., Conditional and Typed Rewriting Systems, 4th International Workshop, CTRS-94, Jerusalem, Israel, July 13\u201315, 1994, LNCS 968, pp. 1\u201314. Springer-Verlag."},{"issue":"3","key":"9_CR2","doi-asserted-by":"publisher","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":"9_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory, Third Kurt G\u00f6del Colloquium","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 24\u201327, 1993, LNCS 713, pp. 83\u201396. Springer-Verlag."},{"issue":"3\/4","key":"9_CR4","doi-asserted-by":"publisher","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":"9_CR5","doi-asserted-by":"crossref","unstructured":"E[dward] Cardoza, R[ichard] Lipton, and A[lbert] R. Meyer. Exponential space complete problems for petri nets and commutative semigroups: Preliminary report. In Eighth Annual ACM Symposium on Theory of Computing, Hershey, PA, USA, May 3\u20135, 1976, pp. 50\u201354.","DOI":"10.1145\/800113.803630"},{"key":"9_CR6","series-title":"LNAI","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-56732-1","volume-title":"Resolution Methods for the Decision Problem","author":"C. Ferm\u00fcller","year":"1993","unstructured":"C[hristian] Ferm\u00fcller, A[lexander] Leitsch, Tanel Tammet, and Nail Zamov. Resolution Methods for the Decision Problem. LNAI 679. Springer-Verlag, Berlin, Heidelberg, New York, 1993."},{"key":"9_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/3-540-56944-8_47","volume-title":"Logic Programming and Automated Reasoning, 4th International Conference, LPAR\u201993","author":"C. Ferm\u00fcller","year":"1993","unstructured":"Christian Ferm\u00fcller and Gernot Salzer. Ordered paramodulation and resolution as decision procedure. In Andrei Voronkov, ed., Logic Programming and Automated Reasoning, 4th International Conference, LPAR\u201993, St. Petersburg, Russia, July 13\u201320, 1993, LNCS 698, pp. 122\u2013133. Springer-Verlag."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Harald Ganzinger and Hans de Nivelle. A superposition decision procedure for the guarded fragment with equality. In Fourteenth Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2\u20135, 1999, pp. 295\u2013303. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1999.782624"},{"key":"9_CR9","unstructured":"Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, and Renate Schmidt. A resolution-based decision procedure for extensions of K4. In Advances in Modal Logic\u2019 98, 1998. To appear."},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Harald Ganzinger and Uwe Waldmann. Theorem proving in cancellative abelian monoids (extended abstract). In Michael A. McRobbie and John K. Slaney, eds., Automated Deduction \u2014 CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30\u2013August 3, 1996, LNAI 1104, pp. 388\u2013402. Springer-Verlag.","DOI":"10.1007\/3-540-61511-3_102"},{"issue":"3","key":"9_CR11","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W. H. Joyner Jr","year":"1976","unstructured":"William H. Joyner Jr. Resolution strategies as decision procedures. Journal of the ACM, 23(3):398\u2013417, July 1976.","journal-title":"Journal of the ACM"},{"issue":"3","key":"9_CR12","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0001-8708(82)90048-2","volume":"46","author":"E. W. Mayr","year":"1982","unstructured":"Ernst W. Mayr and Albert R. Meyer. The complexity of the word problems for commutative semigroups and polynomial ideals. Advances in Mathematics, 46(3):305\u2013329, December 1982.","journal-title":"Advances in Mathematics"},{"issue":"6","key":"9_CR13","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1016\/S0747-7171(19)80003-2","volume":"14","author":"E. Paul","year":"1992","unstructured":"Etienne Paul. A general refutational completeness result for an inference procedure based on associative-commutative unification. Journal of Symbolic Computation, 14(6):577\u2013618, December 1992.","journal-title":"Journal of Symbolic Computation"},{"issue":"2","key":"9_CR14","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":"9_CR15","first-page":"73","volume-title":"Machine Intelligence 7","author":"G. D. Plotkin","year":"1972","unstructured":"Gordon D. Plotkin. Building-in equational theories. In Bernard Meltzer and Donald Michie, eds., Machine Intelligence 7, ch. 4, pp. 73\u201390. American Elsevier, New York, NY, USA, 1972."},{"issue":"1","key":"9_CR16","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BF01270929","volume":"6","author":"M. Rusinowitch","year":"1995","unstructured":"Micha\u00ebl Rusinowitch and Laurent Vigneron. Automated deduction with associative-commutative operators. Applicable Algebra in Engineering, Communication and Computing, 6(1):23\u201356, January 1995.","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"issue":"4","key":"9_CR17","doi-asserted-by":"publisher","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J. R. Slagle","year":"1974","unstructured":"James R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity, and associativity. Journal of the ACM, 21(4):622\u2013642, October 1974.","journal-title":"Journal of the ACM"},{"key":"9_CR18","volume-title":"Cancellative Abelian Monoids in Refutational Theorem Proving","author":"U. Waldmann","year":"1997","unstructured":"Uwe Waldmann. Cancellative Abelian Monoids in Refutational Theorem Proving. Dissertation, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany, 1997. http:\/\/www.mpi-sb.mpg.de\/~uwe\/paper\/PhD.ps.gz ."},{"issue":"1","key":"9_CR19","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0020-0190(98)00084-2","volume":"67","author":"U. Waldmann","year":"1998","unstructured":"Uwe Waldmann. Extending reduction orderings to ACU-compatible reduction orderings. Information Processing Letters, 67(1):43\u201349, July 16, 1998.","journal-title":"Information Processing Letters"},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"Uwe Waldmann. Superposition for divisible torsion-free abelian groups. In Claude Kirchner and H\u00e9l\u00e8ne Kirchner, eds., Automated Deduction \u2014 CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5\u201310, 1998, LNAI 1421, pp. 144\u2013159. Springer-Verlag.","DOI":"10.1007\/BFb0054257"},{"key":"9_CR21","series-title":"Technical Report","volume-title":"First-order theorem proving modulo equations","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, Germany, April 1992."}],"container-title":["Lecture Notes in Computer Science","Logic for Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48242-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,24]],"date-time":"2020-04-24T21:51:35Z","timestamp":1587765095000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48242-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664925","9783540482420"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-48242-3_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}