{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:23Z","timestamp":1749125183401},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540613770"},{"type":"electronic","value":"9783540685074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_54","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:35:51Z","timestamp":1330292151000},"page":"468-485","source":"Crossref","is-referenced-by-count":2,"title":["Positive deduction modulo regular theories"],"prefix":"10.1007","author":[{"given":"Laurent","family":"Vigneron","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"2\u20133","key":"27_CR1","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0304-3975(89)90003-0","volume":"67","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair and N. Dershowitz. Completion for Rewriting Modulo a Congruence. Theoretical Computer Science, 67(2\u20133):173\u2013202, October 1989.","journal-title":"Theoretical Computer Science"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. On Restrictions of Ordered Paramodulation with Simplification. In M. E. Stickel, editor, Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture Notes in Computer Science, pages 427\u2013441. Springer-Verlag, July 1990.","DOI":"10.1007\/3-540-52885-7_105"},{"issue":"3","key":"27_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and H. Ganzinger. Rewrite-based Equational Theorem Proving with Selection and Simplification. Journal of Logic and Computation, 4(3):1\u201331, 1994.","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"27_CR4","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic Paramodulation. Information and Computation, 121(2):172\u2013192, 1995.","journal-title":"Information and Computation"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"L. Bachmair and D. Plaisted. Associative Path Orderings. In Proceedings 1st Conference on Rewriting Techniques and Applications, Dijon (France), volume 202 of Lecture Notes in Computer Science, Springer-Verlag, 1985.","DOI":"10.1007\/3-540-15976-2_11"},{"key":"27_CR6","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand. Proving Theorems with the Modification Method. SIAM Journal of Computing, 4:412\u2013430, 1975.","journal-title":"SIAM Journal of Computing"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"C. Delor and L. Puel. Extension of the Associative Path Ordering to a Chain of Associative Symbols. In C. Kirchner, editor, Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada), volume 690 of Lecture Notes in Computer Science, pages 389\u2013404. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56868-9_29"},{"key":"27_CR8","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science. Elsevier Science Publishers B. V. (North-Holland), 1990."},{"key":"27_CR9","volume-title":"PhD thesis","author":"A. Fortenbacher","year":"1989","unstructured":"A. Fortenbacher. Effizientes Rechnen in AC-Gleichungstheorien. PhD thesis, Universit\u00e4t Karlsruhe (Germany), February 1989."},{"issue":"3","key":"27_CR10","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M. Rusinowitch. Proving Refutational Completeness of Theorem Proving Strategies: The Transfinite Semantic Tree Method. Journal of the ACM, 38(3):559\u2013587, July 1991.","journal-title":"Journal of the ACM"},{"key":"27_CR11","volume-title":"Th\u00e8se de Doctorat de Troisi\u00e8me Cycle","author":"J.-M. Hullot","year":"1980","unstructured":"J.-M. Hullot. Compilation de Formes Canoniques dans les Th\u00e9ories \u00e9quationelles, Th\u00e8se de Doctorat de Troisi\u00e8me Cycle, Universit\u00e9 de Paris Sud, Orsay (France), 1980."},{"key":"27_CR12","first-page":"257","volume-title":"Computational Logic. Essays in honor of Alan Robinson","author":"J.-P. Jouannaud","year":"1991","unstructured":"J.-P. Jouannaud and C. Kirchner. Solving Equations in Abstract Algebras: a Rule-based Survey of Unification. In Jean-Louis Lassez and G. Plotkin, editors, Computational Logic. Essays in honor of Alan Robinson, chapter 8, pages 257\u2013321. MIT Press, Cambridge (MA, USA), 1991."},{"issue":"4","key":"27_CR13","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"J.-P. Jouannaud and H. Kirchner. Completion of a Set of Rules Modulo a Set of Equations. SIAM Journal of Computing, 15(4):1155\u20131194, 1986. Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City (USA), 1984.","journal-title":"SIAM Journal of Computing"},{"key":"27_CR14","unstructured":"D. S. Lankford and A. Ballantyne. Decision Procedures for Simple Equational Theories with Associative Commutative Axioms: Complete Sets of Associative Commutative Reductions. Technical report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977."},{"key":"27_CR15","volume-title":"Th\u00e8se de Doctorat d'Universit\u00e9","author":"C. March\u00e9","year":"1993","unstructured":"C. March\u00e9. R\u00e9\u00e9criture modulo une th\u00e9orie pr\u00e9sent\u00e9e par un syst\u00e8me convergent et d\u00e9cidabilit\u00e9 du probl\u00e8me du mot dans certaines classes de th\u00e9ories \u00e9quationnelles. Th\u00e8se de Doctorat d'Universit\u00e9, Universit\u00e9 de Paris-Sud, Orsay (France), October 1993."},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. Basic Superposition is Complete. In B. Krieg-Br\u00fcckner, editor, Proceedings of ESOP'92, volume 582 of Lecture Notes in Computer Science, pages 371\u2013389. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55253-7_22"},{"key":"27_CR17","unstructured":"E. Paul (E-mail: etienne.paul@issy.cnet.fr). E-Semantic Tree. Unpublished paper, 70 pages, 1994."},{"issue":"1","key":"27_CR18","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. E. Peterson","year":"1983","unstructured":"G. E. Peterson. A Technique for Establishing Completeness Results in Theorem Proving with Equality. SIAM Journal of Computing, 12(1):82\u2013100, 1983.","journal-title":"SIAM Journal of Computing"},{"key":"27_CR19","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson","year":"1981","unstructured":"G. E. Peterson and M. E. Stickel. Complete Sets of Reductions for Some Equational Theories. Journal of the ACM, 28:233\u2013264, 1981.","journal-title":"Journal of the ACM"},{"key":"27_CR20","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin. Building-in Equational Theories. Machine Intelligence, 7:73\u201390, 1972.","journal-title":"Machine Intelligence"},{"key":"27_CR21","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A Machine-oriented Logic Based on the Resolution Principle. Journal of the ACM, 12:23\u201341, 1965.","journal-title":"Journal of the ACM"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"A. Rubio and R. Nieuwenhuis. A Precedence-Based Total AC-Compatible Ordering. In C. Kirchner, editor, Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada), volume 690 of Lecture Notes in Computer Science, pages 374\u2013388. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56868-9_28"},{"key":"27_CR23","unstructured":"M. Rusinowitch. D\u00e9monstration automatique \u2014 Techniques de r\u00e9\u00e9criture. InterEditions, 1989."},{"key":"27_CR24","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","volume":"11","author":"M. Rusinowitch","year":"1991","unstructured":"M. Rusinowitch. Theorem-proving with Resolution and Superposition. Journal of Symbolic Computation, 11:21\u201349, 1991.","journal-title":"Journal of Symbolic Computation"},{"key":"27_CR25","unstructured":"M. Rusinowitch and L. Vigneron. Associative Commutative Deduction. In E. Domenjoud and Claude Kirchner, editors, Proceedings of the 1st CCL Workshop, Le Val d'Ajol (France), October 1992."},{"issue":"1","key":"27_CR26","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/BF01270929","volume":"6","author":"M. Rusinowitch","year":"1995","unstructured":"M. Rusinowitch and L. 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"},{"key":"27_CR27","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M. E. Stickel","year":"1981","unstructured":"M. E. Stickel. A Unification Algorithm for Associative-Commutative Functions. Journal of the ACM, 28:423\u2013434, 1981.","journal-title":"Journal of the ACM"},{"key":"27_CR28","doi-asserted-by":"crossref","unstructured":"L. Vigneron. Associative-Commutative Deduction with Constraints. In A. Bundy, editor, Proceedings 12th International Conference on Automated Deduction, Nancy (France), volume 814 of Lecture Notes in Artificial Intelligence, pages 530\u2013544. Springer-Verlag, June 1994.","DOI":"10.1007\/3-540-58156-1_39"},{"key":"27_CR29","unstructured":"L. Vigneron. Automated Deduction with Symbolic Constraints in Equational Theories. PhD Thesis, Universit\u00e9 Henri Poincar\u00e9 \u2014 Nancy 1, November 1994. Available as Research Report CRIN 94-T-266 (in French)."},{"key":"27_CR30","unstructured":"L. Vigneron. Theorem Proving modulo Regular Theories. Technical report 95-1, Department of Computer Science, SUNY at Stony Brook, Stony Brook, January 1995."},{"key":"27_CR31","unstructured":"U. Wertz. First-Order Theorem Proving Modulo Equations. Technical Report MPI-I-92-216, Max Planck Institut f\u00fcr Informatik, April 1992."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_54.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:31:45Z","timestamp":1619573505000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}