{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:20:17Z","timestamp":1725664817132},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614647"},{"type":"electronic","value":"9783540685968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61464-8_41","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:41:00Z","timestamp":1330274460000},"page":"33-47","source":"Crossref","is-referenced-by-count":4,"title":["Superposition theorem proving for abelian groups represented as integer modules"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Stuber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"4_CR1","first-page":"1","volume-title":"LNCS 968","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L. and Ganzinger, H. (1994a). Associative-commutative superposition. In Proc. 4th Int. Workshop on Conditional and Typed Rewriting, Jerusalem, LNCS 968, pp. 1\u201314. Springer."},{"issue":"3","key":"4_CR2","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L. and Ganzinger, H. (1994b). Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation4(3): 217\u2013247.","journal-title":"Journal of Logic and Computation"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Bachmair, L. and Ganzinger, H. (1994c). Rewrite techniques for transitive relations. In Proc. 9th Ann. IEEE Symp. on Logic in Computer Science, Paris, pp. 384\u2013393.","DOI":"10.1109\/LICS.1994.316051"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H. and Stuber, J. (1995). Combining algebra and universal algebra in first-order theorem proving: The case of commutative rings. In Proc. 10th Workshop on Specification of Abstract Data Types, Santa Margherita, Italy, LNCS 906.","DOI":"10.1007\/BFb0014420"},{"key":"4_CR5","volume-title":"Technical Report MPI-I-93-236","author":"L. Bachmair","year":"1993","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C. and Snyder, W. (1993). Basic paramodulation. Technical Report MPI-I-93-236, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Boudet, A., Contejean, E. and March\u00e9, C. (1996). AC-complete unification and its application to theorem proving. This volume.","DOI":"10.1007\/3-540-61464-8_40"},{"key":"4_CR7","first-page":"83","volume-title":"Machine Intelligence 11","author":"R. S. Boyer","year":"1988","unstructured":"Boyer, R. S. and Moore, J. S. (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, pp. 83\u2013124. Clarendon Press, Oxford."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. and Jouannaud, J.-P. (1990). Rewrite systems. In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science: Formal Models and Semantics, Vol. B, chapter 6, pp. 243\u2013320. Elsevier\/MIT Press.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Fitting, M. (1990). First-Order Logic and Automated Theorem Proving. Springer.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"4_CR10","volume-title":"Technical Report MPI-I-96-2-001","author":"H. Ganzinger","year":"1996","unstructured":"Ganzinger, H. and Waldmann, U. (1996). Theorem proving in cancellative abelian monoids. Technical Report MPI-I-96-2-001, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany."},{"issue":"4","key":"4_CR11","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P. and Kirchner, H. (1986). Completion of a set of rules modulo a set of equations. SIAM Journal on Computing15(4): 1155\u20131194.","journal-title":"SIAM Journal on Computing"},{"key":"4_CR12","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/S0747-7171(88)80020-8","volume":"6","author":"A. Kandri-Rody","year":"1988","unstructured":"Kandri-Rody, A. and Kapur, D. (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":"4_CR13","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C., Kirchner, H. and Rusinowitch, M. (1990). Deduction with symbolic constraints. Revue Fran\u00e7aise d'Intelligence Artificielle4(3): 9\u201352.","journal-title":"Revue Fran\u00e7aise d'Intelligence Artificielle"},{"key":"4_CR14","first-page":"142","volume-title":"LNCS 170","author":"P. Chenadec Le","year":"1984","unstructured":"Le Chenadec, P. (1984). Canonical forms in finitely presented algebras. In Proc. 7th Int. Conf. on Automated Deduction, Napa, CA, LNCS 170, pp. 142\u2013165. Springer. Book version published by Pitman, Londons, 1986."},{"key":"4_CR15","first-page":"394","volume-title":"Normalised rewriting and normalised completion","author":"C. March\u00e9","year":"1994","unstructured":"March\u00e9, C. (1994). Normalised rewriting and normalised completion. In Proc. 9th Symp. on Logic in Computer Science, Paris, pp. 394\u2013403. IEEE Computer Society Press."},{"key":"4_CR16","first-page":"477","volume-title":"LNCS 607","author":"R. Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R. and Rubio, A. (1992). Theorem proving with ordering constrained clauses. In 11th International Conference on Automated Deduction, Saratoga Springs, NY, LNCS 607, pp. 477\u2013491. Springer."},{"key":"4_CR17","first-page":"545","volume-title":"LNCS 814","author":"R. Nieuwenhuis","year":"1994","unstructured":"Nieuwenhuis, R. and Rubio, A. (1994). AC-superposition with constraints: no AC-unifiers needed. In Proc. 12th Int. Conf. on Automated Deduction, Nancy, France, LNCS 814, pp. 545\u2013559. Springer."},{"key":"4_CR18","first-page":"530","volume-title":"LNCS 814","author":"L. Vigneron","year":"1994","unstructured":"Vigneron, L. (1994). Associative-commutative deduction with constraints. In Proc. 12th Int. Conf. on Automated Deduction, Nancy, France, LNCS 814, pp. 530\u2013544. Springer."},{"key":"4_CR19","first-page":"21","volume-title":"LNCS 310","author":"T. C. Wang","year":"1988","unstructured":"Wang, T. C. (1988). Elements of Z-module reasoning. In Proc. 9th Int. Conf. on Automated Deduction, Argonne, LNCS 310, pp. 21\u201340. Springer."},{"key":"4_CR20","volume-title":"Technical Report MPI-I-92-216","author":"U. Wertz","year":"1992","unstructured":"Wertz, U. (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","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61464-8_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:32:07Z","timestamp":1619559127000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}