{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:12Z","timestamp":1761611172449},"publisher-location":"Berlin\/Heidelberg","reference-count":50,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019021X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0026103","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T07:47:21Z","timestamp":1132645641000},"page":"165-184","source":"Crossref","is-referenced-by-count":7,"title":["Equational completion in order-sorted algebras extended abstract"],"prefix":"10.1007","author":[{"given":"Isabelle","family":"Gnaedig","sequence":"first","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]},{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"P. Arnold, D. Coleman, C. Dollin, R. Gallimore, H. Gilchrist, and T. Rush. An introduction to the Axis specification language. Technical Report HPL-BRC-TM-87-034, HP Laboratories, Bristol research centre, 1987."},{"key":"12_CR2","volume-title":"Proceedings Second Conference on Rewriting Techniques and Applications","author":"L. Bachmair","year":"1987","unstructured":"L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. In Proceedings Second Conference on Rewriting Techniques and Applications, Springer Verlag, Bordeaux (France), May 1987."},{"key":"12_CR3","unstructured":"L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proceeding of the first symposium on Logic In Computer Science, Boston (USA), 1986."},{"key":"12_CR4","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0304-3975(86)90019-8","volume":"46","author":"G. Bernot","year":"1986","unstructured":"G. Bernot, M. Bidoit, and C. Choppy. Abstract data types with exception handling: an initial approach based on a distinction between exceptions and errors. Theoretical Computer Science, 46:13\u201345, 1986.","journal-title":"Theoretical Computer Science"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"R.M. Burstall, D.B. MacQueen, and D.T. Sannella. Hope: an experimental applicative language, In Conference Record of the 1980 LISP Conference, pages 136\u2013143. Stanford (Californie, USA), 1980.","DOI":"10.1145\/800087.802799"},{"key":"12_CR6","unstructured":"R.J. Cunningham and A.J.J. Dick. Rewrite Systems on a Lattice of Types. Technical Report, Imperial College, Department of Computing, 1983."},{"key":"12_CR7","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279\u2013301, 1982.","journal-title":"Theoretical Computer Science"},{"key":"12_CR8","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/3-540-15976-2_9","volume-title":"Proceedings 1st Conference on Rewriting Techniques and Applications","author":"N. Dershowitz","year":"1985","unstructured":"N. Dershowitz. Termination. In Proceedings 1st Conference on Rewriting Techniques and Applications, pages 180\u2013224, Springer Verlag, Dijon (France), May 1985."},{"key":"12_CR9","unstructured":"N. Dershowitz and D.A. Plaisted. Equational programming. to appear in Machine Intelligence 11, 1985."},{"key":"12_CR10","volume-title":"Proceedings of the EUROCAL conference","author":"A.J.J. Dick","year":"1985","unstructured":"A.J.J. Dick. Eril equational reasoning: an interactive laboratory. In B. Buchberger, editor, Proceedings of the EUROCAL conference, Springer-Verlag, Linz (Austria), 1985."},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"K. Futatsugi, J.A. Goguen, J.P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proceedings of 12th ACM Symposium on Principles of Programming Languages Conference, 1985.","DOI":"10.1145\/318593.318610"},{"key":"12_CR12","unstructured":"I. Gnaedig. Order-sorted equational termination. in preparation, 1987."},{"key":"12_CR13","unstructured":"I. Gnaedig, C. Kirchner, and H. Kirchner. Equational Completion in Order-sorted Algebras. Technical Report 87R086, Centre de Recherche en Informatique de Nancy, 1987."},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"J.A. Goguen, J.P. Jouannaud, and J. Meseguer. Operational semantics for order-sorted algebra. In Proceeding of the 12th ICALP, Nafplion (Greece), pages 221\u2013231, 1985.","DOI":"10.1007\/BFb0015747"},{"key":"12_CR15","unstructured":"J.A. Goguen and J. Meseguer, Completeness of many-sorted equational logic. Technical Report CSLI-84-15, Center for the Study of Language and Information, Stanford University, 1984."},{"key":"12_CR16","unstructured":"J.A. Goguen and J. Meseguer. Order-sorted algebra I: partial and overloaded operators, errors and inheritance. 1986."},{"key":"12_CR17","unstructured":"J.A. Goguen and J. Meseguer. Order-sorted algebra solves the constructor-selector, multiple representation and coercion problem. In Proceeding of the second symposium on Logic In Computer Science, 1987."},{"key":"12_CR18","first-page":"66","volume":"30","author":"J.A. Goguen","year":"1986","unstructured":"J.A. Goguen and J. Meseguer. Remarks on remarks on many-sorted equational logic. Bulletin of EATCS, (30):66\u201373, October 1986.","journal-title":"Bulletin of EATCS"},{"key":"12_CR19","unstructured":"J.A. Goguen, J. Meseguer, and D. Plaisted. Programming with parameterized abstract objects in OBJ. Theory And Practice of Software Technology, 163\u2013193, 1982."},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"C.M. Hoffmann and M.J. O'Donnell. Programming with equations. Transactions on Programming Languages and Systems, 4(1), 1982.","DOI":"10.1145\/357153.357158"},{"key":"12_CR21","first-page":"331","volume-title":"Proceedings of 10th ICALP","author":"J. Hsiang","year":"1983","unstructured":"J. Hsiang and N. Dershowitz. Rewrite methods for clausal and non-clausal theorem proving. In Proceedings of 10th ICALP, pages 331\u2013346, Springer-Verlag, Barcelona (Spain), 1983."},{"key":"12_CR22","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"G. Huet. A complete proof of correctness of the Knuth and Bendix completion algorithm. Journal of Computer Systems and Sciences, 23:11\u201321, 1981.","journal-title":"Journal of Computer Systems and Sciences"},{"issue":"4","key":"12_CR23","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet. Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the Association for Computing Machinery, 27(4):797\u2013821, 1980. Preliminary version in 18th Symposium on Foundations Of Computer Science, IEEE, 1977.","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"2","key":"12_CR24","first-page":"239","volume":"25","author":"G. Huet","year":"1982","unstructured":"G. Huet and J.M. Hullot. Proofs by induction in equational theories with constructors. Journal of the Association for Computing Machinery, 25(2):239\u2013266, 1982. Preliminary version in Proceedings 21st Symposium on Foundations of Computer Science, IEEE, 1980.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"G. Huet and D. Oppen. Equations and rewrite rules: a survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems. Academic Press, 1980.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"12_CR26","unstructured":"J.P. Jouannaud. Church-rosser computations with equational term rewriting systems. In G. Ausiello and M. Protasi, editors, Proceedings of the 4th Conference on Automata, Algebra and Programming, Lecture Notes in Computer Science, Volume 159, Springer-Verlag, 1983."},{"key":"12_CR27","unstructured":"J-P. Jouannaud. Proof algebras. Invited conference to the second Rewriting Techniques and Applications conference, Bordeaux (France), 1987."},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"J.P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing, 15(4), 1986. Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City, 1984.","DOI":"10.1137\/0215084"},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"J.P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. Proceedings 11th ACM Symposium on Principles Of Programming Languages, Salt Lake City, 1984.","DOI":"10.1145\/800017.800519"},{"key":"12_CR30","volume-title":"Proceedings of the 7th Conference on Automated Deduction","author":"J.P. Jouannaud","year":"1984","unstructured":"J.P. Jouannaud and M. Munoz. Termination of a set of rules modulo a set of equations. In Proceedings of the 7th Conference on Automated Deduction, Springer-Verlag, Napa Valley (California, USA), 1984."},{"key":"12_CR31","unstructured":"C. Kirchner. M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories \u00e9quationnelles. Th\u00e8se d'\u00e9tat de l'Universit\u00e9 de Nancy I, 1985."},{"key":"12_CR32","unstructured":"C. Kirchner. Methods and tools for equational unification. In Proceedings of the Colloquium on Resolution of Equations in Algebraic Structures, May 1987."},{"key":"12_CR33","unstructured":"C. Kirchner. Order sorted equational matching. In preparation, 1987."},{"key":"12_CR34","unstructured":"C. Kirchner. Order sorted equational unification. In preparation, 1987."},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"C. Kirchner and H. Kirchner. Reveur-3: implementation of a general completion procedure parametrized by built-in theories and strategies. Science of Computer Programming, (8), 1987.","DOI":"10.1016\/0167-6423(87)90004-9"},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ3. Technical Report 87-R-87, Centre de Recherche en Informatique de Nancy, 1987.","DOI":"10.1007\/3-540-19488-6_123"},{"key":"12_CR37","volume-title":"Proceedings 7th international Conference on Automated Deduction","author":"H. Kirchner","year":"1984","unstructured":"H. Kirchner. A general inductive completion algorithm and application to abstract data types. In R. Shostak, editor, Proceedings 7th international Conference on Automated Deduction, Springer-Verlag, Napa Valley (California, USA), 1984."},{"key":"12_CR38","unstructured":"H. Kirchner. Preuves par compl\u00e9tion dans les vari\u00e9t\u00e9s d'alg\u00e8bres. Th\u00e8se d'\u00e9tat de l'Universit\u00e9 de Nancy I, 1985."},{"key":"12_CR39","unstructured":"D. Knuth and P. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra, Pergamon Press, 1970."},{"key":"12_CR40","unstructured":"D. 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":"12_CR41","unstructured":"D. Lankford and A. Ballantyne. Decision Procedures for Simple Equational Theories with Commutative Axioms: Complete Sets of Commutative Reductions. Technical Report, University of Texas at Austin, Dept. of Mathematics and Computer Science, 1977."},{"key":"12_CR42","unstructured":"D. Lankford and A. Ballantyne. Decision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions. Technical Report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science, 1977."},{"key":"12_CR43","unstructured":"J. Meseguer and J.A. Goguen. Initiality, induction and computability. In M. Nivat and J. Reynolds, editors, Algebraic Methods in Semantics, Cambridge University Press, 1985."},{"key":"12_CR44","unstructured":"J. Meseguer, J.A. Goguen, and G. Smolka. Order sorted unification. In Proceedings of the Colloquium on Resolution of Equations in Algebraic Structures, May 1987."},{"issue":"2","key":"12_CR45","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M. H. A. Newman","year":"1942","unstructured":"M. H. A. Newman. On theories with a combinatorial definition of Equivalence. Annals of Math, 43(2):223\u2013243, 1942.","journal-title":"Annals of Math"},{"key":"12_CR46","unstructured":"W. Nutt, G. Smolka, J.A. Goguen, and J. Meseguer. Order sorted computation. In Proceedings of the Colloquium on Resolution of Equations in Algebraic Structures, May 1987."},{"key":"12_CR47","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"G. Peterson and M. Stickel. Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery, 28:233\u2013264, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"12_CR48","volume-title":"Proceedings 8th Conference on Automated Deduction, Oxford","author":"M. Schmidt-Schauss","year":"1986","unstructured":"M. Schmidt-Schauss. Unification in many sorted equational theories. In J. Siekmann, editor, Proceedings 8th Conference on Automated Deduction, Oxford, Springer Verlag, Oxford (England). 1986."},{"key":"12_CR49","doi-asserted-by":"crossref","unstructured":"Y. Toyama. Term rewriting systems with membership conditions. In Proceedings of the first international workshop on conditional term rewriting systems, Orsay (France), July 1987.","DOI":"10.1007\/3-540-19242-5_17"},{"key":"12_CR50","first-page":"1","volume-title":"Proc. 2nd Conf. on Functional Programming Languages and Computer Architecture","author":"D.A. Turner","year":"1985","unstructured":"D.A. Turner. Miranda: a non-strict functional language with polymorphic types. In Proc. 2nd Conf. on Functional Programming Languages and Computer Architecture, pages 1\u201316, Springer Verlag, Nancy (France), 1985."}],"container-title":["Lecture Notes in Computer Science","CAAP '88"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0026103.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:55:53Z","timestamp":1607550953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0026103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019021X"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/bfb0026103","relation":{},"subject":[]}}