{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:04:23Z","timestamp":1725566663415},"publisher-location":"Berlin, Heidelberg","reference-count":56,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_27","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"368-375","source":"Crossref","is-referenced-by-count":1,"title":["Twenty Years Later"],"prefix":"10.1007","author":[{"given":"Jean-Pierre","family":"Jouannaud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Aiken, A., Wimmers, E.: Type inclusion constraints and type inference. In: Proc. 7th ACM Conference on Functional programming and Computer Archtecture, Copenhaguen, Denmark, pp. 31\u201341 (1993)","DOI":"10.1145\/165180.165188"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Conditional and Typed Rewriting Systems","author":"L. Bachmair","year":"1991","unstructured":"Bachmair, L., Ganzinger, H.: Completion of first-order clause with equality by strict superposition. In: Okada, M., Kaplan, S. (eds.) CTRS 1990. LNCS, vol.\u00a0516, Springer, Heidelberg (1991)"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"10th International Conference on Automated Deduction","author":"L. Bachmair","year":"1990","unstructured":"Bachmair, L., Ganzinger, H.: On restrictions of ordered paramodulation with simplification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, Springer, Heidelberg (1990)"},{"key":"27_CR4","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Technical Report MPI-I-91-208, Max-Planck- Institut f\u00fcr Informatik, Saarbr\u00fccken (September 1991); to appear in Journal of Logic and Computation"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013068","volume-title":"Logic Programming and Automated Reasoning","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H.: Non-clausal resolution and superposition with selection and redundancy criteria. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, Springer, Heidelberg (1992)"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-11","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and superposition. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, Springer, Heidelberg (1992)"},{"key":"27_CR7","volume-title":"Proceedings of the Eigth Annual IEEE Symposium on Logic in Computer Science","author":"L. Bachmair","year":"1993","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Set constraints are the monadic class. In: Proceedings of the Eigth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Los Alamitos (1993)"},{"key":"27_CR8","volume-title":"Conference Record of the 30th Symposium on Principles of Programming Languages","author":"G. Barthe","year":"2003","unstructured":"Barthe, G., Cirstea, H., Kirchner, C., Liquori, L.: Pure patern type systems. In: Conference Record of the 30th Symposium on Principles of Programming Languages, New-Orleans, USA, January 2003, ACM, New York (2003)"},{"issue":"1","key":"27_CR9","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1017\/S0960129504004426","volume":"15","author":"F. Blanqui","year":"2005","unstructured":"Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science\u00a015(1), 37\u201392 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"key":"27_CR10","unstructured":"Blanqui, F.: Inductive types in the Calculus of Algebraic Constructions. Fundamenta Informaticae (to appear)"},{"key":"27_CR11","unstructured":"Blanqui, F., Jouannaud, J.-P., Strub, P.-Y.: A calculus of congruent constructions. Technical report, \u00c9cole Polytechnique (2005) (submitted)"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Trees in Algebra and Programming - CAAP \u201996","author":"A. Boudet","year":"1996","unstructured":"Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol.\u00a01059, pp. 30\u201343. Springer, Heidelberg (1996)"},{"key":"27_CR13","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1016\/S0747-7171(89)80054-9","volume":"8","author":"A. Boudet","year":"1989","unstructured":"Boudet, A., Jouannaud, J.-P., Schmidt-Schau\u00df, M.: Unification in Boolean rings and Abelian groups. Journal of Symbolic Computation\u00a08, 449\u2013477 (1989)","journal-title":"Journal of Symbolic Computation"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/BFb0030589","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"A. Bouhoula","year":"1997","unstructured":"Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 67\u201392. Springer, Heidelberg (1997)"},{"key":"27_CR15","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/LICS.1997.614920","volume-title":"Twelfth Annual IEEE Symposium on Logic in Computer Science","author":"A. Bouhoula","year":"1997","unstructured":"Bouhoula, A., Jouannaud, J.-P.: Automata-driven automated induction. In: Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw,Poland, June 1997, pp. 14\u201325. IEEE Comp. Soc. Press, Los Alamitos (1997)"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Abstract Software Specifications","author":"R.M. Burstall","year":"1980","unstructured":"Burstall, R.M., Goguen, J.A.: The semantics of CLEAR, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol.\u00a086, Springer, Heidelberg (1980)"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/3-540-56868-9_25","volume-title":"Rewriting Techniques and Applications","author":"A.-C. Caron","year":"1993","unstructured":"Caron, A.-C., Coquid\u00e9, J.-L., Dauchet, M.: Encompassment properties and automata with constraints. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 328\u2013342. Springer, Heidelberg (1993)"},{"key":"27_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-24849-1_9","volume-title":"Types for Proofs and Programs","author":"J. Chrzaszcz","year":"2004","unstructured":"Chrzaszcz, J.: Modules in coq are and will be correct. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 135\u2013150. Springer, Heidelberg (2004)"},{"key":"27_CR19","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1109\/LICS.1995.523285","volume-title":"Tenth Annual IEEE Symposium on Logic in Computer Science","author":"H. Comon","year":"1995","unstructured":"Comon, H.: Sequentiality, second-order monadic logic and tree automata. In: Kozen, D. (ed.) Tenth Annual IEEE Symposium on Logic in Computer Science, San Diego, CA, June 1995, pp. 508\u2013517. IEEE Comp. Soc. Press, Los Alamitos (1995)"},{"issue":"2","key":"27_CR20","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H. Comon","year":"1994","unstructured":"Comon, H., Delor, C.: Equational formulae with membership constraints. Information and Computation\u00a0112(2), 167\u2013216 (1994)","journal-title":"Information and Computation"},{"key":"27_CR21","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Information and Computation\u00a076, 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"27_CR22","first-page":"114","volume-title":"Proceedings of the Fourth Jerusalem Conference on Information Technology","author":"N. Dershowitz","year":"1984","unstructured":"Dershowitz, N.: Equations as programming language. In: Proceedings of the Fourth Jerusalem Conference on Information Technology, Jerusalem, Israe, May 1984, pp. 114\u2013124. IEEE Computer Society, Los Alamitos (1984)"},{"key":"27_CR23","series-title":"AMAST series in Computing","doi-asserted-by":"crossref","DOI":"10.1142\/3831","volume-title":"Cafeobj-report: The language, proof techniques and methodologies for object-oriented algebraic specification.","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R., Futatsugi, K.: Cafeobj-report: The language, proof techniques and methodologies for object-oriented algebraic specification. AMAST series in Computing, vol.\u00a06. World Scientific, Singapore (1998)"},{"key":"27_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/3-540-45657-0_27","volume-title":"Computer Aided Verification","author":"M. Rusinowitch","year":"2002","unstructured":"Rusinowitch, M., et al.: The aviss security protocols analysis tool \u2013 system description. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 349. Springer, Heidelberg (2002)"},{"key":"27_CR25","unstructured":"Fribourg, L., Peixoto, M.V.: Automates concurrents \u00e0 contraintes. Technique et Science Informatiques\u00a013(6) (1994)"},{"key":"27_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"STACS 93","author":"R. Gilleron","year":"1993","unstructured":"Gilleron, R., Tison, S., Tommasi, M.: Solving systems of set constraints using tree automata. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 1993. LNCS, vol.\u00a0665, Springer, Heidelberg (1993)"},{"key":"27_CR27","doi-asserted-by":"crossref","unstructured":"Gonthier, G., L\u00e9vy, J.-J., Mellies, P.-A.: An abstract standardisation theorem. In: Proc. 7th IEEE Symp. on Logic in Computer Science, Santa Cruz, CA (1992)","DOI":"10.1109\/LICS.1992.185521"},{"key":"27_CR28","unstructured":"Goubault-Larrecq, J.: R\u00e9solution ordonn\u00e9e avec s\u00e9lection et classes d\u00e9cidables de la logique du premier ordre (2004), available from the web"},{"key":"27_CR29","unstructured":"Gregoire, B.: Compilation de termes de preuves. Un mariage entre Coq et OCaml. PhD thesis, \u00c9cole Polytechnique, Palaiseau, France (2003)"},{"key":"27_CR30","unstructured":"Hermant, O.: A rewriting abstract machine for coq (2004)"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume-title":"Automata, Languages and Programming","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol.\u00a0267, pp. 54\u201371. Springer, Heidelberg (1987)"},{"key":"27_CR32","unstructured":"Comon, D.L.H., Dauchet, M., Tison, S. (eds.): Tree Automata techniques and Applications, Lille, France (2002), http:\/\/www.grappa.univ-lille3.fr\/tata\/"},{"key":"27_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028013","volume-title":"Computer Science Logic","author":"H. Comon","year":"1998","unstructured":"Comon, H., J\u00fcrsski, Y.: Higher-order matching and tree automata. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol.\u00a01414, Springer, Heidelberg (1998)"},{"issue":"4","key":"27_CR34","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. Journal of the ACM\u00a027(4), 797\u2013821 (1980)","journal-title":"Journal of the ACM"},{"key":"27_CR35","series-title":"Lecture Notes in Computer Science","volume-title":"5th Conference on Automated Deduction","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol.\u00a087, Springer, Heidelberg (1980)"},{"key":"27_CR36","unstructured":"Jouannaud, J.-P.: Modular associative commutative confluence. Technical report, \u00c9cole Polytechnique (2005)"},{"key":"27_CR37","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"J.-P. Jouannaud","year":"1991","unstructured":"Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: A rule-based survey of unification. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic: Essays in Honor of Alan Robinson, MIT-Press, Cambridge (1991)"},{"key":"27_CR38","unstructured":"Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in equational theories without constructors. In: Logic in Computer Science (June 1986)"},{"key":"27_CR39","unstructured":"Jouannaud, J.-P., Rubio, A., van Raamsdonk, F.: Higher-order rewriting with types and arities. Technical report, \u00c9cole Polytechnique (2005) (submitted)"},{"issue":"3","key":"27_CR40","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Fran\u00e7aise d\u2019Intelligence Artificielle\u00a04(3), 9\u201352 (1990); Special issue on automatic deduction","journal-title":"Revue Fran\u00e7aise d\u2019Intelligence Artificielle"},{"key":"27_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-48483-3_12","volume-title":"Recent Trends in Algebraic Development Techniques","author":"C. Kirchner","year":"1999","unstructured":"Kirchner, C., Moreau, P.: Non deterministic computations in elan. In: Fiadeiro, J.L. (ed.) WADT 1998. LNCS, vol.\u00a01589, pp. 168\u2013183. Springer, Heidelberg (1999)"},{"key":"27_CR42","unstructured":"Lankford, D.S.: Canonical inference. Memo ATP-32, University of Texas at Austin (March 1975)"},{"key":"27_CR43","doi-asserted-by":"crossref","unstructured":"Lugiez, D., Moysset, J.-L.: Complement problems and tree automata in AC-like theories. In: Proc. Symp. on Theoretical Aspects of Computer Science, W\u00fcrzburg (1993); also available as techincal report CRIN 92-R-175","DOI":"10.1007\/3-540-56503-5_51"},{"issue":"1","key":"27_CR44","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R. Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science\u00a0192(1), 3\u201329 (1998)","journal-title":"Theoretical Computer Science"},{"key":"27_CR45","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: A logical theory of concurrent objects and its realization in the maude language. In: Agha, G., Wegner, P., Yoneezawa, A. (eds.) Research Directions in Object-Based Concurrency (1992) (to appear)","DOI":"10.7551\/mitpress\/2087.003.0017"},{"key":"27_CR46","first-page":"170","volume-title":"Proc. of the 1st IEEE International Conference on Formal Engineering Methods","author":"A.T. Nakagawa","year":"1997","unstructured":"Nakagawa, A.T., Futatsugi, K.: An overview of cafe specification environment. In: Proc. of the 1st IEEE International Conference on Formal Engineering Methods, pp. 170\u2013181. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"27_CR47","volume-title":"Eleventh Annual IEEE Symposium on Logic in Computer Science","author":"R. Nieuwenhuis","year":"1996","unstructured":"Nieuwenhuis, R.: Basic paramodulation and decidable theories. In: Felty, A. (ed.) Eleventh Annual IEEE Symposium on Logic in Computer Science, New-Brunswick, CA, June 1996, IEEE Comp. Soc. Press, Los Alamitos (1996)"},{"key":"#cr-split#-27_CR48.1","unstructured":"Nieuwenhuis, R., Rubio, A.: Completion of first-order clauses by basic superposition with ordering constraints. Tech. report, Dept. L.S.I., Univ. Polit. Catalunya (1991);"},{"key":"#cr-split#-27_CR48.2","unstructured":"To appear in Proc. 11th Conf. on Automated Deduction, Saratoga Springs (1992)"},{"key":"27_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system COQ. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 328\u2013345. Springer, Heidelberg (1993)"},{"issue":"1","key":"27_CR50","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G.E. Peterson","year":"1983","unstructured":"Peterson, G.E.: A technique for establishing completeness results in theorem proving with equality. SIAM Journal on Computing\u00a012(1), 82\u2013100 (1983)","journal-title":"SIAM Journal on Computing"},{"issue":"2-3","key":"27_CR51","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D.A. Plaisted","year":"1985","unstructured":"Plaisted, D.A.: Semantic confluence tests and completion methods. Information and Control\u00a065(2-3), 182\u2013215 (1985)","journal-title":"Information and Control"},{"issue":"2","key":"27_CR52","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R.E. Shostak","year":"1979","unstructured":"Shostak, R.E.: An efficient decision procedure for arithmetic with function symbols. J. of the Association for Computing Machinery\u00a026(2), 351\u2013360 (1979)","journal-title":"J. of the Association for Computing Machinery"},{"key":"27_CR53","unstructured":"Shostak, R.E.: Deciding combinations of theories. Technical Report CSL 132, SRI International (February 1982)"},{"key":"27_CR54","doi-asserted-by":"publisher","first-page":"698","DOI":"10.1145\/321420.321429","volume":"14","author":"L. Wos","year":"1967","unstructured":"Wos, L., Robinson, G., Carson, D., Shalla, L.: The concept of demodulation in theorem proving. Journal of the ACM\u00a014, 698\u2013709 (1967)","journal-title":"Journal of the ACM"},{"key":"27_CR55","volume-title":"Conference Record of the 21st Symposium on Principles of Programming Languages","author":"H. Xi","year":"1998","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: Conference Record of the 21st Symposium on Principles of Programming Languages, San Antonio, Texas, ACM, New York (1998)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,30]],"date-time":"2024-03-30T20:10:35Z","timestamp":1711829435000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}