×

ELAN from a rewriting logic point of view. (English) Zbl 1001.68057

Summary: ELAN implements computational systems, a concept that combines two first class entities: rewrite rules and rewriting strategies. ELAN can be used either as a logical framework or to describe and execute deterministic as well as non-deterministic rule-based processes. With the general goal to make precise a rewriting logic-based semantics of ELAN, this paper has three contributions: a presentation of the concepts of rules and strategies available in ELAN, an expression of rewrite rules with matching conditions in conditional rewriting logic, and finally an enrichment mechanism of a rewrite theory into a strategy theory in conditional rewriting logic.

MSC:

68Q42 Grammars and rewriting systems
68T27 Logic in artificial intelligence

Software:

ELAN; Maude; LCF
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abrial, J.-R., The B-Book: Assigning Programs to Meanings (1996), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0915.68015
[2] C. Alvarado, Q.-H. Nguyen, ELANCOQ; C. Alvarado, Q.-H. Nguyen, ELANCOQ
[3] T. Arts, Automatically proving termination and innermost normalisation of term rewriting systems, Ph.D. Thesis, Universiteit Utrecht, 1997.; T. Arts, Automatically proving termination and innermost normalisation of term rewriting systems, Ph.D. Thesis, Universiteit Utrecht, 1997. · Zbl 1379.68191
[4] Baader, F.; Nipkow, T., Term Rewriting and all That (1998), Cambridge University Press: Cambridge University Press Cambridge
[5] L. Bachmair, T. Chen, I.V. Ramakrishnan, Associative-commutative discrimination nets, in: M.-C. Gaudel, J.-P. Jouannaud (Eds.), TAPSOFT ’93: Theory and Practice of Software Development, 4th Intern. Joint Conf. CAAP/FASE, Lecture Notes in Computer Science, Vol. 668, Orsay, France, April 13-17, 1993, Springer, Berlin, pp. 61-74.; L. Bachmair, T. Chen, I.V. Ramakrishnan, Associative-commutative discrimination nets, in: M.-C. Gaudel, J.-P. Jouannaud (Eds.), TAPSOFT ’93: Theory and Practice of Software Development, 4th Intern. Joint Conf. CAAP/FASE, Lecture Notes in Computer Science, Vol. 668, Orsay, France, April 13-17, 1993, Springer, Berlin, pp. 61-74.
[6] Bachmair, L.; Ganzinger, H.; Lynch, C.; Snyder, W., Basic paramodulation, Inform. Comput., 121, 2, 172-192 (1995) · Zbl 0833.68115
[7] H. Barendregt, E. Barendsen, Autartik computations in formal proofs, J. Symbolic Comput., 2002, to appear. 1997.; H. Barendregt, E. Barendsen, Autartik computations in formal proofs, J. Symbolic Comput., 2002, to appear. 1997. · Zbl 1002.68156
[8] E. Beffara, O. Bournez, H. Kacem, C. Kirchner, Verification of timed automata using rewrite rules and strategies, in: N. Dershowitz, A. Frank (Eds.), Proc. BISFAI 2001, Tel Aviv (Israel), June 2001.; E. Beffara, O. Bournez, H. Kacem, C. Kirchner, Verification of timed automata using rewrite rules and strategies, in: N. Dershowitz, A. Frank (Eds.), Proc. BISFAI 2001, Tel Aviv (Israel), June 2001.
[9] Benanav, D.; Kapur, D.; Narendran, P., Complexity of matching problems, J. Symbolic Comput., 3, 1 & 2, 203-216 (1987) · Zbl 0638.68036
[10] Borovanský, P., Implementation of higher-order unification based on calculus of explicit substitutions, (Bartošek, M.; Staudek, J.; Wiedermann, J., Proc. SOFSEM’95: Theory and Practice of Informatics, Lecture Notes in Computer Science, Vol. 1012 (1995), Springer: Springer Berlin), 363-368
[11] P. Borovanský, Le contrôle de la réécriture: étude et implantation d’un formalisme de stratégies, Thèse de Doctorat d’Université, Université Henri Poincaré - Nancy 1, France, October 1998. Also TR LORIA 98-T-326.; P. Borovanský, Le contrôle de la réécriture: étude et implantation d’un formalisme de stratégies, Thèse de Doctorat d’Université, Université Henri Poincaré - Nancy 1, France, October 1998. Also TR LORIA 98-T-326.
[12] P. Borovanský, C. Castro, Cooperation of constraint solvers: using the new process control facilities of ELAN; P. Borovanský, C. Castro, Cooperation of constraint solvers: using the new process control facilities of ELAN
[13] P. Borovanský, H. Cirstea, H. Dubois, C. Kirchner, H. Kirchner, P.-E. Moreau, C. Ringeissen, M. Vittek, ELAN; P. Borovanský, H. Cirstea, H. Dubois, C. Kirchner, H. Kirchner, P.-E. Moreau, C. Ringeissen, M. Vittek, ELAN
[14] Borovanský, P.; Kirchner, C.; Kirchner, H., Controlling rewriting by rewriting, (Meseguer, J., Proc. 1st Internat. Workshop on Rewriting Logic and its Applications, WRLA’96, Electronic Notes in Theoretical Computer Science, Vol. 4 (September 1996), Asilomar: Asilomar California) · Zbl 0912.68088
[15] P. Borovanský, C. Kirchner, H. Kirchner, A functional view of rewriting and strategies for a semantics of ELAN; P. Borovanský, C. Kirchner, H. Kirchner, A functional view of rewriting and strategies for a semantics of ELAN
[16] Borovanský, P.; Kirchner, C.; Kirchner, H.; Moreau, P.-E.; Vittek, M., ELAN: a logical framework based on computational systems, (Meseguer, J., Proc. 1st Internat. Workshop on Rewriting Logic and its Applications, WRLA’96, Electronic Notes in Theoretical Computer Science, Vol. 4 (September 1996), Asilomar: Asilomar California)
[17] P. Borovanský, C. Kirchner, H. Kirchner, C. Ringeissen, Rewriting with strategies in ELAN; P. Borovanský, C. Kirchner, H. Kirchner, C. Ringeissen, Rewriting with strategies in ELAN · Zbl 1319.68125
[18] Castro, C., Solving binary CSP using computational systems, (Meseguer, J., Proc. 1st Internat. Workshop on Rewriting Logic and its Applications, WRLA’96, Electronic Notes in Theoretical Computer Science, Vol. 4 (September 1996), Asilomar: Asilomar California) · Zbl 0912.68097
[19] Castro, C., Building constraint satisfaction problem solvers using rewrite rules and strategies, Fundamenta Informaticae, 34, 263-293 (1998) · Zbl 0943.68095
[20] C. Castro, COLETTE; C. Castro, COLETTE
[21] H. Cirstea, Calcul de réécriture: fondements et applications, Thèse de Doctorat d’Université, Université Henri Poincaré - Nancy I, 2000.; H. Cirstea, Calcul de réécriture: fondements et applications, Thèse de Doctorat d’Université, Université Henri Poincaré - Nancy I, 2000.
[22] H. Cirstea, C. Kirchner, Using rewriting and strategies for describing the B predicate prover, in: Proc. Workshop on Strategies in Automated Deduction, CADE-15, Lindau, Germany, July 1998.; H. Cirstea, C. Kirchner, Using rewriting and strategies for describing the B predicate prover, in: Proc. Workshop on Strategies in Automated Deduction, CADE-15, Lindau, Germany, July 1998.
[23] Cirstea, H.; Kirchner, C., Combining higher-order and first-order computation using \(ρ\)-calculustowards a semantics of ELAN, (Gabbay, D.; de Rijke, M., Frontiers of Combining Systems 2, Research Studies (1999), Wiley: Wiley New York), 95-120 · Zbl 1004.68080
[24] H. Cirstea, C. Kirchner, The simply typed rewriting calculus, in: K. Futatsugi (Ed.), 3rd Internat. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, Kanazawa, Japan, September 2000.; H. Cirstea, C. Kirchner, The simply typed rewriting calculus, in: K. Futatsugi (Ed.), 3rd Internat. Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science, Kanazawa, Japan, September 2000. · Zbl 0962.68084
[25] Cirstea, H.; Kirchner, C., The rewriting calculus — Part I and II, Logic J. Interest Group Pure Appl. Logics, 9, 3, 427-498 (2001)
[26] H. Cirstea, C. Kirchner, Specifying authentication protocols using rewriting and strategies, in: I.V. Ramakrishnan (Ed.), 3rd Internat. Workshop on Practical Aspects of Declarative Languages, Lecture Notes in Computer Science, Vol. 1990, Las Vegas, USA, Springer, Berlin, March 2001, pp. 138-153.; H. Cirstea, C. Kirchner, Specifying authentication protocols using rewriting and strategies, in: I.V. Ramakrishnan (Ed.), 3rd Internat. Workshop on Practical Aspects of Declarative Languages, Lecture Notes in Computer Science, Vol. 1990, Las Vegas, USA, Springer, Berlin, March 2001, pp. 138-153.
[27] Cirstea, H.; Kirchner, C.; Liquori, L., Matching power, (Middeldorp, A., Proc. RTA’2001, Lecture Notes in Computer Science, Vol. 2051 (May 2001), Utrecht, The Netherlands, Springer: Utrecht, The Netherlands, Springer Berlin), 77-92 · Zbl 0981.68065
[28] H. Cirstea, C. Kirchner, L. Liquori, The rho cube, in: F. Honsell (Ed.), Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Vol. 2030, Genova, Italy, Springer, Berlin, April 2001, pp. 166-180.; H. Cirstea, C. Kirchner, L. Liquori, The rho cube, in: F. Honsell (Ed.), Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Vol. 2030, Genova, Italy, Springer, Berlin, April 2001, pp. 166-180. · Zbl 0978.68072
[29] M. Clavel, F. Duran, S. Eker, P. Lincoln, J. Meseguer, Metalevel Computation in Maude, in: C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Internat. Workshop on Rewriting Logic and its Applications, WRLA’98, Electronic Notes in Theoretical Computer Science, Vol. 15, Pont-á-Mousson, France, September 1998, pp. 3-24.; M. Clavel, F. Duran, S. Eker, P. Lincoln, J. Meseguer, Metalevel Computation in Maude, in: C. Kirchner, H. Kirchner (Eds.), Proc. 2nd Internat. Workshop on Rewriting Logic and its Applications, WRLA’98, Electronic Notes in Theoretical Computer Science, Vol. 15, Pont-á-Mousson, France, September 1998, pp. 3-24. · Zbl 0917.68024
[30] M.G. Clavel, J. Meseguer, Axiomatizing reflective logics and languages, in: G. Kiczales (Ed.), Proc. Reflection’96, San Francisco, California, April 1996, pp. 263-288. Xerox PARC, 1996.; M.G. Clavel, J. Meseguer, Axiomatizing reflective logics and languages, in: G. Kiczales (Ed.), Proc. Reflection’96, San Francisco, California, April 1996, pp. 263-288. Xerox PARC, 1996.
[31] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (van Leeuwen, J., Handbook of Theoretical Computer Science (1990), Elsevier Science Publishers BV, North-Holland: Elsevier Science Publishers BV, North-Holland Amsterdam), 244-320, (Chapter 6) · Zbl 0900.68283
[32] E. Domenjoud, A technical note on AC-unification. the number of minimal unifiers of the equation \(αx_1αx_p_{ AC }βy_1βy_{q\) · Zbl 0768.68068
[33] G. Dowek, La part du Calcul., Mémoire d’habilitation, Université de Paris 7, 1999.; G. Dowek, La part du Calcul., Mémoire d’habilitation, Université de Paris 7, 1999.
[34] G. Dowek, T. Hardin, C. Kirchner, Theorem proving modulo, Rapport de Recherche 3400, Institut National de Recherche en Informatique et en Automatique, April 1998, to appear in the JAR.; G. Dowek, T. Hardin, C. Kirchner, Theorem proving modulo, Rapport de Recherche 3400, Institut National de Recherche en Informatique et en Automatique, April 1998, to appear in the JAR. · Zbl 1049.03011
[35] H. Dubois, H. Kirchner, Objects, rules and strategies in ELAN; H. Dubois, H. Kirchner, Objects, rules and strategies in ELAN
[36] Dubois, H.; Kirchner, H., Rule based programming with constraints and strategies, (Apt, K.; Kakas, A. A.C.; Monfroy, E.; Rossi, F., New Trends in Constraints, Papers from the Joint ERCIM/Compulog-Net Workshop, Cyprus, October 25-27, 1999, Lecture Notes in Artificial Intelligence, Vol. 1865 (2000), Springer: Springer Berlin), 274-297
[37] Eker, S., Associative-commutative matching via bipartite graph matching, Comput. J., 38, 5, 381-399 (1995)
[38] O. Fissore, I. Gnaedig, H. Kirchner, Termination of rewriting with local strategies, Technical Report, LORIA, Nancy, France, 2001. http://www.loria.fr/\(^∼\); O. Fissore, I. Gnaedig, H. Kirchner, Termination of rewriting with local strategies, Technical Report, LORIA, Nancy, France, 2001. http://www.loria.fr/\(^∼\) · Zbl 1268.68146
[39] T. Genet, Contraintes d’ordre et automates d’arbres pour les preuves de terminaison, Ph.D. Thesis, Universié Henri Poincaré - Nancy I, 1998.; T. Genet, Contraintes d’ordre et automates d’arbres pour les preuves de terminaison, Ph.D. Thesis, Universié Henri Poincaré - Nancy I, 1998.
[40] Gordon, M.; Milner, A.; Wadsworth, C., Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science, Vol. 78 (1979), Springer: Springer New York (NY, USA) · Zbl 0421.68039
[41] B. Gramlich, On proving termination by innermost termination, in: H. Ganzinger, Proc. 7th Conf. on Rewriting Techniques and Applications, New Brunswick, NJ, USA, Lecture Notes in Computer Science, Vol. 1103, Springer, Berlin, July 1996, 93-107.; B. Gramlich, On proving termination by innermost termination, in: H. Ganzinger, Proc. 7th Conf. on Rewriting Techniques and Applications, New Brunswick, NJ, USA, Lecture Notes in Computer Science, Vol. 1103, Springer, Berlin, July 1996, 93-107.
[42] J.-M. Hullot, Associative-commutative pattern matching, in: Proc. 9th International Joint Conference on Artificial Intelligence, Tokyo, Japan, 1979.; J.-M. Hullot, Associative-commutative pattern matching, in: Proc. 9th International Joint Conference on Artificial Intelligence, Tokyo, Japan, 1979.
[43] J.-M. Hullot, Compilation de Formes Canoniques dans les Théories équationelles, Thèse de Doctorat de Troisième Cycle, Université de Paris Sud, Orsay, France, 1980.; J.-M. Hullot, Compilation de Formes Canoniques dans les Théories équationelles, Thèse de Doctorat de Troisième Cycle, Université de Paris Sud, Orsay, France, 1980.
[44] Jaffar, J.; Maher, M., Constraint logic programminga survey, J. Logic Programming, 19-20, 503-582 (1994)
[45] J.-P. Jouannaud, H. Kirchner, Completion of a set of rules modulo a set of equations, SIAM J. Comput. 15(4) (1986) 1155-1194. Preliminary version in Proc. 11th ACM Symp. on Principles of Programming Languages, Salt Lake City, USA, 1984.; J.-P. Jouannaud, H. Kirchner, Completion of a set of rules modulo a set of equations, SIAM J. Comput. 15(4) (1986) 1155-1194. Preliminary version in Proc. 11th ACM Symp. on Principles of Programming Languages, Salt Lake City, USA, 1984. · Zbl 0665.03005
[46] Jouannaud, J.-P.; Kirchner, C., Solving equations in abstract algebrasa rule-based survey of unification, (Lassez, J.-L.; Plotkin, G., Computational Logic. Essays in honor of Alan Robinson (1991), The MIT Press: The MIT Press Cambridge, MA, USA), 257-321, (Chapter 8)
[47] Kirchner, H., Some extensions of rewriting, (Comon, H.; Jouannaud, J.-P., Term Rewriting, Lecture Notes in Computer Science, Vol. 909 (1995), Springer: Springer Berlin), 54-73
[48] C. Kirchner, H. Kirchner, Rewriting, Solving, Proving, A preliminary version of a book available at \(^∼\); C. Kirchner, H. Kirchner, Rewriting, Solving, Proving, A preliminary version of a book available at \(^∼\)
[49] Kirchner, C.; Kirchner, H.; Vittek, M., Designing constraint logic programming languages using computational systems, (Van Hentenryck, P.; Saraswat, V., Principles and Practice of Constraint Programming, The Newport Papers (1995), The MIT Press: The MIT Press Cambridge, MA), 131-158, (Chapter 8)
[50] Kirchner, H.; Moreau, P.-E., Prototyping completion with constraints using computational systems, (Hsiang, J., Proc. 6th Conf. on Rewriting Techniques and Applications, Kaiserslautern, Germany, Lecture Notes in Computer Science, Vol. 914 (1995), Springer: Springer Berlin), 438-443
[51] Kirchner, H.; Moreau, P.-E., Promoting rewriting to a programming language: a compiler for non-deterministic rewrite programs in associative-commutative theories, J. Functional Programming, 11, 2, 207-251 (2001) · Zbl 0979.68055
[52] C. Kirchner, Z. Qian, P.-K. Singh, J. Stuber, XemanticsELAN; C. Kirchner, Z. Qian, P.-K. Singh, J. Stuber, XemanticsELAN
[53] Kirchner, C.; Ringeissen, C., Rule-based constraint programming, Fundamenta Informaticae, 34, 3, 225-262 (1998) · Zbl 0943.68094
[54] Klint, P., A meta-environment for generating programming environments, ACM Trans. Software Engng. Methodol., 2, 176-201 (1993)
[55] Kounalis, E.; Lugiez, D., Compilation of pattern matching with associative commutative functions, (16th Colloquium on Trees in Algebra and Programming, Lecture Notes in Computer Science, Vol. 493 (1991), Springer: Springer Berlin), 57-73 · Zbl 0967.68505
[56] Lugiez, D.; Moysset, J.-L., Tree automata help one to solve equational formulae in AC-theories, J. Symbolic Comput., 18, 4, 297-318 (1994) · Zbl 0827.68041
[57] C. Marché, Normalised rewriting and normalised completion, in: S. Abramsky (Ed.), Proc. 9th IEEE Symp. on Logic in Computer Science, Paris, France, 1994, pp. 394-403.; C. Marché, Normalised rewriting and normalised completion, in: S. Abramsky (Ed.), Proc. 9th IEEE Symp. on Logic in Computer Science, Paris, France, 1994, pp. 394-403.
[58] N. Martı́-Oliet, J. Meseguer, Rewriting logic as a logical and semantic framework, Technical Report SRI-CSL-93-05, SRI International, Computer Science Laboratory, 2001. To appear in: D. Gabbay (Ed.), Handbook of Philosophical Logic, Vol. 9, Kluwer Academic Publishers, Dordrecht.; N. Martı́-Oliet, J. Meseguer, Rewriting logic as a logical and semantic framework, Technical Report SRI-CSL-93-05, SRI International, Computer Science Laboratory, 2001. To appear in: D. Gabbay (Ed.), Handbook of Philosophical Logic, Vol. 9, Kluwer Academic Publishers, Dordrecht.
[59] Meijer, E.; Johan, J., Merging monads and folds for functional programming, (Meijer, E.; Johan, J., Proc. Advanced Functional Programming, Lecture Notes in Computer Science, Vol. 925 (1995), Springer: Springer Berlin), 228-266
[60] J. Meseguer, General logics, in: H.-D.E. et al. (Eds.), Logic Colloquium’87, Elsevier Science Publishers BV, North-Holland, Amsterdam, 1989, pp. 275-329.; J. Meseguer, General logics, in: H.-D.E. et al. (Eds.), Logic Colloquium’87, Elsevier Science Publishers BV, North-Holland, Amsterdam, 1989, pp. 275-329. · Zbl 0691.03001
[61] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoret. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043
[62] P.-E. Moreau, H. Kirchner, A compiler for rewrite programs in associative-commutative theories, in: Principles of Declarative Programming, Lecture Notes in Computer Science, Vol. 1490, Springer, Berlin, September 1998, pp. 230-249.; P.-E. Moreau, H. Kirchner, A compiler for rewrite programs in associative-commutative theories, in: Principles of Declarative Programming, Lecture Notes in Computer Science, Vol. 1490, Springer, Berlin, September 1998, pp. 230-249.
[63] Q.-H. Nguyen, Certifying term rewriting proof in ELAN; Q.-H. Nguyen, Certifying term rewriting proof in ELAN
[64] Nivela, P.; Nieuwenhuis, R., Saturation of first-order (constrained) clauses with the saturate system, (Kirchner, C., Proc. 5th Conf. on Rewriting Techniques and Applications, Montreal, Canada, Lecture Notes in Computer Science, Vol. 690 (1993), Springer: Springer Berlin), 436-440
[65] Peterson, G.; Stickel, M. E., Complete sets of reductions for some equational theories, J. ACM, 28, 233-264 (1981) · Zbl 0479.68092
[66] Ringeissen, C., Prototyping combination of unification algorithms with the ELAN rule-based programming language, (Proc. 8th Conf. on Rewriting Techniques and Applications, Sitges, Spain, Lecture Notes in Computer Science, Vol. 1232 (1997), Springer: Springer Berlin), 323-326 · Zbl 1379.68204
[67] Rusinowitch, M.; Vigneron, L., Automated deduction with associative-commutative operators, Appl. Algebra Engng., Commun. Comput., 6, 1, 23-56 (1995) · Zbl 0823.68096
[68] J. Stuber, Experiments with an implementation of extended narrowing and resolution in the rewriting language ELAN; J. Stuber, Experiments with an implementation of extended narrowing and resolution in the rewriting language ELAN
[69] L. Vigneron, Déduction automatique avec contraintes symboliques dans les théories équationnelles, Thèse de Doctorat d’Université, Université Henri Poincaré - Nancy 1, November 1994.; L. Vigneron, Déduction automatique avec contraintes symboliques dans les théories équationnelles, Thèse de Doctorat d’Université, Université Henri Poincaré - Nancy 1, November 1994.
[70] P. Viry, Input/Output for ELANin: J. Meseguer, Proc. 1st International Workshop on Rewriting Logic and its Applications, WRLA’96, Electronic Notes in Theoretical Computer Science, Vol. 4, Asilomar, California, September 1996.; P. Viry, Input/Output for ELANin: J. Meseguer, Proc. 1st International Workshop on Rewriting Logic and its Applications, WRLA’96, Electronic Notes in Theoretical Computer Science, Vol. 4, Asilomar, California, September 1996.
[71] Visser, E., The Stratego Tutorial (1999), Department of Computer Science, Universiteit Utrecht: Department of Computer Science, Universiteit Utrecht Utrecht, The Netherlands
[72] M. Vittek, ELAN; M. Vittek, ELAN
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.