{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:11:35Z","timestamp":1725664295306},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540591559"},{"type":"electronic","value":"9783540492009"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59155-9_8","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:04:14Z","timestamp":1330257854000},"page":"128-146","source":"Crossref","is-referenced-by-count":6,"title":["On the use of constraints in automated deduction"],"prefix":"10.1007","author":[{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"8_CR1","first-page":"50","volume-title":"Unification in the union of disjoint equational theories: Combining decision procedures","author":"F. Baader","year":"1992","unstructured":"Franz Baader and Klaus Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N.Y., USA), pages 50\u201365, 1992."},{"issue":"2\u20133","key":"8_CR2","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"},{"issue":"3","key":"8_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"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (N.Y., USA), pages 462\u2013476, 1992.","DOI":"10.1007\/3-540-55602-8_185"},{"key":"8_CR5","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. A. Plaisted. Termination orderings for associative-commutative rewriting systems. Journal of Symbolic Computation, 1:329\u2013349, 1985.","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"T. B. Baird, G. E. Peterson, and Ralph W. Wilkerson. Complete sets of reductions modulo associativity, commutativity and identity. In N. Dershowitz, editor, Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA), volume 355 of Lecture Notes in Computer Science, pages 29\u201344. Springer-Verlag, April 1989.","DOI":"10.1007\/3-540-51081-8_98"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert. A Resolution Principle for a Logic with Restricted Quantifiers, volume 568 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-55034-8"},{"key":"8_CR8","unstructured":"Jacques Chabin. Unification G\u00e9n\u00e9rale par Surr\u00e9duction Ordonn\u00e9e Contrainte et Surr\u00e9duction Dirig\u00e9e. Th\u00e8se de Doctorat d'Universit\u00e9, Universit\u00e9 d'Orl\u00e9ans, January 1994."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"H. Comon. Completion of rewrite systems with membership constraints. In W. Kuich, editor, Proceedings of ICALP 92, volume 623 of Lecture Notes in Computer Science. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55719-9_91"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pages 244\u2013320. Elsevier Science Publishers B. V. (North-Holland), 1990. Also as: Research report 478, LRI.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, pages 244\u2013320. Elsevier Science Publishers B. V. (North-Holland), 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"8_CR12","unstructured":"E. Domenjoud. Outils pour la d\u00e9duction automatique dans les th\u00e9ories associatives-commutatives. Th\u00e8se de Doctorat d'Universit\u00e9, Universit\u00e9 de Nancy 1, September 1991."},{"key":"8_CR13","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00263448","volume":"8","author":"E. Domenjoud","year":"1992","unstructured":"E. Domenjoud. A technical note on AC-unification. the number of minimal unifiers of the equation \u03b1x 1+...+\u03b1x p \u2250 AC \u03b2y 1+...\u03b2y q . Journal of Automated Reasoning, 8:39\u201344, 1992. Also as research report CRIN 89-R-2.","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01189020","volume":"3","author":"M. Fern\u00e1ndez","year":"1992","unstructured":"M. Fern\u00e1ndez. Narrowing based procedures for equational disunification. Applicable Algebra in Engineering, Communication and Computation, 3:1\u201326, 1992.","journal-title":"Applicable Algebra in Engineering, Communication and Computation"},{"key":"8_CR15","unstructured":"A. Frisch and Scherl R. A general framework for modal deduction. In J. A. Allen, R. Fikes, and E. Sandewall, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Second International Conference, San Mateo, CA, USA, 1991."},{"key":"8_CR16","unstructured":"G. Huet. Constrained Resolution: A Complete Method for Higher Order Logic. PhD thesis, Case Western Reserve University, 1972."},{"issue":"4","key":"8_CR17","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\u00e9l\u00e9ne 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":"8_CR18","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud and C. March\u00e9. Completion modulo associativity, commutativity and identity (AC1). In A. Miola, editor, Proceedings of DISCO'90, volume 429 of Lecture Notes in Computer Science, pages 111\u2013120. Springer-Verlag, April 1990.","DOI":"10.1007\/3-540-52531-9_130"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Claude Kirchner and H\u00e9l\u00e9ne Kirchner. Constrained equational reasoning. In Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, Portland (Oregon), pages 382\u2013389. ACM Press, July 1989. Report CRIN 89-R-220.","DOI":"10.1145\/74540.74585"},{"issue":"3","key":"8_CR20","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Claude Kirchner, H\u00e9l\u00e8ne Kirchner, and M. Rusinowitch. Deduction with symbolic constraints. Revue d'Intelligence Artificielle, 4(3):9\u201352, 1990. Special issue on Automatic Deduction.","journal-title":"Revue d'Intelligence Artificielle"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"H. Kirchner and P.-E. Moreau. Prototyping completion with constraints using computational systems. Technical report submitted, 1994.","DOI":"10.1007\/3-540-59200-8_79"},{"key":"8_CR22","unstructured":"H. Kirchner and C. Ringeissen. Constraint solving by narrowing in combined algebraic domains. In P. Van Hentenryck, editor, Proc. 11th International Conference on Logic Programming, pages 617\u2013631. The MIT press, 1994."},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"C. Lynch and W. Snyder. Redundancy criteria for constrained completion. In C. Kirchner, editor, Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada), volume 690 of Lecture Notes in Computer Science, pages 2\u201316. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56868-9_2"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"U. Martin and T. Nipkow. Ordered rewriting and confluence. In M. E. Stickel, editor, Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture Notes in Computer Science, pages 366\u2013380. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_100"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"P. Narendran and M. Rusinowitch. Any ground associative-commutative theory has a finite canonical system. In R. V. Book, editor, Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy). Springer-Verlag, 1991.","DOI":"10.1007\/3-540-53904-2_115"},{"key":"8_CR26","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":"8_CR27","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. Theorem proving with ordering constrained clauses. In D. Kapur, editor, Proceedings of CADE-11, volume 607 of Lecture Notes in Computer Science, pages 477\u2013491. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_186"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. AC-superposition with constraints: no AC-unifiers needed. In A. Bundy, editor, Proceedings 12th International Conference on Automated Deduction, Nancy (France), volume 814 of Lecture Notes in Artificial Intelligence, pages 545\u2013559. Springer-Verlag, June 1994.","DOI":"10.1007\/3-540-58156-1_40"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"G. E. Peterson. Complete sets of reductions with constraints. In M. E. Stickel, editor, Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), volume 449 of Lecture Notes in Computer Science, pages 381\u2013395. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_101"},{"key":"8_CR30","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":"8_CR31","volume-title":"PhD thesis, FB Informatik","author":"G. Smolka","year":"1989","unstructured":"G. Smolka. Logic Programming over Polymorphically Order-Sorted Types. PhD thesis, FB Informatik, Universit\u00e4t Kaiserslautern, Germany, 1989."},{"issue":"4","key":"8_CR32","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"M. Stickel. Automated deduction by theory resolution. Journal of Automated Reasoning, 1(4):285\u2013289, 1985.","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR33","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"}],"container-title":["Lecture Notes in Computer Science","Constraint Programming: Basics and Trends"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59155-9_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:25:42Z","timestamp":1605630342000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59155-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540591559","9783540492009"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-59155-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}