{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:07:32Z","timestamp":1725574052026},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540240877"},{"type":"electronic","value":"9783540305026"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30502-6_27","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T22:22:20Z","timestamp":1294438940000},"page":"363-379","source":"Crossref","is-referenced-by-count":3,"title":["Rule-Based Programming and Proving: The ELAN Experience Outcomes"],"prefix":"10.1007","author":[{"given":"Claude","family":"Kirchner","sequence":"first","affiliation":[]},{"given":"H\u00e9l\u00e8ne","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"27_CR1","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0304-3975(01)00368-1","volume":"286","author":"E. Astesiano","year":"2002","unstructured":"Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Br\u00fcckner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL: The Common Algebraic Specification Language. Theoretical Computer Science\u00a0286(2), 153\u2013196 (2002)","journal-title":"Theoretical Computer Science"},{"key":"27_CR2","unstructured":"Bergstra, J.A., Tucker, J.V.: Algebraic specifications of computable and semicomputable data structures. Theoretical Computer Science\u00a024 (1983)"},{"key":"27_CR3","unstructured":"Bert, D., Drabik, P., Echahed, R., Declerfayt, O., Demeuse, B., Schobbens, P.-Y., Wautier, F.: Reference manual of the specification language LPG- version 1.8 on SUN workstations. In: Internal report, LIFIA-Grenoble (FRANCE) (January 1989)"},{"key":"27_CR4","unstructured":"Borovansk\u00fd, P., Cirstea, H., Dubois, H., Kirchner, C., Kirchner, H., Moreau, P.-E., Nguyen, Q.-H., Ringeissen, C., Vittek, M.: ELAN V 3.6 User Manual. LORIA, 5th edn., Nancy, France (February 2004)"},{"issue":"285","key":"27_CR5","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0304-3975(01)00358-9","volume":"2","author":"P. Borovansky","year":"2002","unstructured":"Borovansky, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theoretical Computer Science\u00a02(285), 155\u2013185 (2002)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"27_CR6","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1142\/S0129054101000412","volume":"12","author":"P. Borovansk\u00fd","year":"2001","unstructured":"Borovansk\u00fd, P., Kirchner, C., Kirchner, H., Ringeissen, C.: Rewriting with strategies in ELAN: a functional semantics. International Journal of Foundations of Computer Science\u00a012(1), 69\u201398 (2001)","journal-title":"International Journal of Foundations of Computer Science"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings 14th Conference on Rewriting Techniques and Applications, Valencia, Spain","author":"O. Bournez","year":"2003","unstructured":"Bournez, O., C\u00f4me, G.-M., Conraud, V., Kirchner, H., Ib\u0103nescu, L.: A rule-based approach for automated generation of kinetic chemical mechanisms. In: Proceedings 14th Conference on Rewriting Techniques and Applications, Valencia, Spain. LNCS. Springer, Heidelberg (2003)"},{"key":"27_CR8","volume-title":"Deep Inference and Symmetry in Classical Proofs","author":"K. Br\u00fcnnler","year":"2004","unstructured":"Br\u00fcnnler, K.: Deep Inference and Symmetry in Classical Proofs. Logos Verlag, Berlin (2004)"},{"key":"27_CR9","doi-asserted-by":"crossref","first-page":"263","DOI":"10.3233\/FI-1998-34303","volume":"34","author":"C. Castro","year":"1998","unstructured":"Castro, C.: Building Constraint Satisfaction Problem Solvers Using Rewrite Rules and Strategies. Fundamenta Informaticae\u00a034, 263\u2013293 (1998)","journal-title":"Fundamenta Informaticae"},{"key":"27_CR10","unstructured":"Cirstea, H.: Calcul de r\u00e9\u00e9criture\u00a0: fondements et applications. Th\u00e8se de Doctorat d\u2019Universit\u00e9, Universit\u00e9 Henri Poincar\u00e9 - Nancy I (2000)"},{"issue":"3","key":"27_CR11","first-page":"427","volume":"9","author":"H. Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C.: The rewriting calculus \u2014 Part\u00a0I and II. Logic Journal of the Interest Group in Pure and Applied Logics\u00a09(3), 427\u2013498 (2001)","journal-title":"Logic Journal of the Interest Group in Pure and Applied Logics"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/3-540-45127-7_8","volume-title":"Rewriting Techniques and Applications","author":"H. Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C., Liquori, L.: Matching Power. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, p. 77. Springer, Heidelberg (2001)"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science\u00a02(285) (2001)","DOI":"10.1016\/S0304-3975(01)00359-0"},{"issue":"7","key":"27_CR14","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/79204.79210","volume":"33","author":"A. Colmerauer","year":"1990","unstructured":"Colmerauer, A.: An introduction to Prolog III. Communications of the ACM\u00a033(7), 69\u201390 (1990)","journal-title":"Communications of the ACM"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/3-540-51081-8_103","volume-title":"Rewriting Techniques and Applications","author":"M. Dauchet","year":"1989","unstructured":"Dauchet, M.: Simulation of Turing machines by a left-linear rewrite rule. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 109\u2013120. Springer, Heidelberg (1989)"},{"issue":"1","key":"27_CR16","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1017\/S0960129500003236","volume":"11","author":"G. Dowek","year":"2001","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: HOL-\u03bb\u03c3 an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science\u00a011(1), 21\u201345 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"27_CR17","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning\u00a031(1), 33\u201372 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"27_CR18","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Selected papers of the 4th International Workshop on Strategies in Automated Deduction","author":"O. Fissore","year":"2001","unstructured":"Fissore, O., Gnaedig, I., Kirchner, H.: Termination of rewriting with local strategies. In: Bonacina, M.P., Gramlich, B. (eds.) Selected papers of the 4th International Workshop on Strategies in Automated Deduction. Electronic Notes in Theoretical Computer Science, vol.\u00a058. Elsevier Science Publishers B. V, North-Holland (2001)"},{"key":"27_CR19","first-page":"62","volume-title":"Proceedings of the Fourth International Conference on Principles and Practice of Declarative Programming","author":"O. Fissore","year":"2002","unstructured":"Fissore, O., Gnaedig, I., Kirchner, H.: CARIBOO: An induction based proof tool for termination with strategies. In: Proceedings of the Fourth International Conference on Principles and Practice of Declarative Programming, Pittsburgh (USA), pp. 62\u201373. ACM Press, New York (2002)"},{"key":"27_CR20","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings of the Fourth International Workshop on Rewriting Logic and Its Applications","author":"O. Fissore","year":"2002","unstructured":"Fissore, O., Gnaedig, I., Kirchner, H.: Outermost ground termination. In: Proceedings of the Fourth International Workshop on Rewriting Logic and Its Applications, Pisa, Italy. Electronic Notes in Theoretical Computer Science, vol.\u00a071, Elsevier Science Publishers B. V, North-Holland (2002)"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Goguen, J.A.: Some design principles and theory for OBJ-0, a language for expressing and executing algebraic specifications of programs. In: Blum, E., Paul, M., Takasu, S. (eds.) Mathematical Studies of Information Processing, Kyoto, Japan. LNCS, vol.\u00a075, pp. 425\u2013473 (1979), Proceedings of a Workshop held August 1978","DOI":"10.1007\/3-540-09541-1_36"},{"key":"27_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-18420-1_50","volume-title":"Graph Reduction","author":"J.A. Goguen","year":"1987","unstructured":"Goguen, J.A., Kirchner, C., Meseguer, J.: Concurrent term rewriting as a model of computation. In: Fasel, J.H., Keller, R.M. (eds.) Graph Reduction 1986. LNCS, vol.\u00a0279, pp. 53\u201393. Springer, Heidelberg (1987)"},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Faure, G., Kirchner, C.: A rho-calculus of explicit constraint application. In: Proceedings of the 5th workshop on rewriting logic and applications. Electronic Notes in Theoretical Computer Science (2004)","DOI":"10.1016\/j.entcs.2004.06.029"},{"key":"27_CR24","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.-L.: Constraint logic programming. In: Proceedings of the 14th Annual ACM Symposium on Principles Of Programming Languages, Munich, Germany, pp. 111\u2013119 (1987)","DOI":"10.1145\/41625.41635"},{"key":"27_CR25","first-page":"131","volume-title":"Principles and Practice of Constraint Programming. The Newport Papers","author":"C. Kirchner","year":"1995","unstructured":"Kirchner, C., Kirchner, H., Vittek, M.: Designing Constraint Logic Programming Languages using Computational Systems. In: Van Hentenryck, P., Saraswat, V. (eds.) Principles and Practice of Constraint Programming. The Newport Papers, pp. 131\u2013158. MIT Press, Cambridge (1995)"},{"issue":"2","key":"27_CR26","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1017\/S0956796800003907","volume":"11","author":"H. Kirchner","year":"2001","unstructured":"Kirchner, H., Moreau, P.-E.: Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories. Journal of Functional Programming\u00a011(2), 207\u2013251 (2001)","journal-title":"Journal of Functional Programming"},{"key":"27_CR27","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1145\/151257.151260","volume":"2","author":"P. Klint","year":"1993","unstructured":"Klint, P.: A meta-environment for generating programming environments. ACM Transactions on Software Engineering and Methodology\u00a02, 176\u2013201 (1993)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"27_CR28","volume-title":"Foundations of Deductive Databases and Logic Programming","author":"J.-L. Lassez","year":"1988","unstructured":"Lassez, J.-L., Maher, M.J., Marriot, K.: Unification revisited. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming. Morgan-Kaufman, San Francisco (1988)"},{"issue":"1","key":"27_CR29","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1093\/jigpal\/11.1.51","volume":"11","author":"R. Loader","year":"2003","unstructured":"Loader, R.: Higher order \u03b2 matching is undecidable. Logic Journal of the IGPL\u00a011(1), 51\u201368 (2003)","journal-title":"Logic Journal of the IGPL"},{"key":"27_CR30","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science\u00a096, 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-36579-6_5","volume-title":"Compiler Construction","author":"P.-E. Moreau","year":"2003","unstructured":"Moreau, P.-E., Ringeissen, C., Vittek, M.: A Pattern Matching Compiler for Multiple Target Languages. In: Hedin, G. (ed.) CC 2003. LNCS, vol.\u00a02622, pp. 61\u201376. Springer, Heidelberg (2003)"},{"issue":"3-4","key":"27_CR32","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1023\/A:1021975117537","volume":"29","author":"Q.-H. Nguyen","year":"2002","unstructured":"Nguyen, Q.-H., Kirchner, C., Kirchner, H.: External rewriting for skeptical proof assistants. Journal of Automated Reasoning\u00a029(3-4), 309\u2013336 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"27_CR33","series-title":"Journal of Symbolic Computation","volume-title":"Special issue on Order-sorted Rewriting","author":"G. Smolka","year":"1998","unstructured":"Smolka, G.: Special issue on Order-sorted Rewriting. Journal of Symbolic Computation, vol.\u00a025. Academic Press inc., London (1998)"},{"key":"27_CR34","volume-title":"Language Prototyping","author":"A. Deursen van","year":"1996","unstructured":"van Deursen, A., Heering, J., Klint, P.: Language Prototyping. World Scientific, Singapore (1996) ISBN 981-02-2732-9"},{"key":"27_CR35","unstructured":"Visser, E.: Language independent traversals for program transformation. Technical report, Department of Computer Science, Universiteit Utrecht, Utrecht, The Netherlands (2000)"},{"key":"27_CR36","unstructured":"Vittek, M.: ELAN: Un cadre logique pour le prototypage de langages de programmation avec contraintes. Th\u00e8se de Doctorat d\u2019Universit\u00e9, Universit\u00e9 Henri Poincar\u00e9 - Nancy\u00a01 (October 1994)"}],"container-title":["Lecture Notes in Computer Science","Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30502-6_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,17]],"date-time":"2021-11-17T02:55:49Z","timestamp":1637117749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30502-6_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540240877","9783540305026"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30502-6_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}