Rewriting logic as a logical and semantic framework.

*(English)*Zbl 0912.68096
Meseguer, J. (ed.), Rewriting logic and its applications. Proceedings of the 1st international workshop, Pacific Grove, CA, USA, September 3–6, 1996. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 4, 36 p. (1996).

Summary: Rewriting logic is proposed as a logical framework in which other logics can be represented, and as a semantic framework for the specification of languages and systems. Using concepts from the theory of general logics, representations of an object logic \(\mathcal L\) in a framework logic \(\mathcal F\) are understood as mappings \(\mathcal L \rightarrow \mathcal F\) that translate one logic into the other in a conservative way. The ease with which such maps can be defined is discussed in detail for the cases of linear logic, logics with quantifiers, and any sequent calculus presentation of a logic for a very general notion of “sequent”. Using the fact that rewriting logic is reflective, it is often possible to reify inside rewriting logic itself a representation map \(\mathcal L \rightarrow RWLogic\) for the finitely presentable theories of \(\mathcal L\). Such a reification takes the form of a map between the abstract data types representing the finitary theories of \(\mathcal L\) and of RWLogic. Regarding the different but related use of rewriting logic as a semantic framework, the straightforward way in which very diverse models of concurrency can be expressed and unified within rewriting logic is illustrated with CCS. In addition, the way in which constraint solving fits within the rewriting logic framework is briefly explained.

For the entire collection see [Zbl 0903.00068].

For the entire collection see [Zbl 0903.00068].

##### Keywords:

rewriting logic
PDF
BibTeX
XML
Cite

\textit{N. Martí-Oliet} and \textit{J. Meseguer}, in: Rewriting logic and its applications. Proceedings of the 1st international workshop, Pacific Grove, CA, USA, September 3--6, 1996. Amsterdam: Elsevier. 36 p. (1996; Zbl 0912.68096)

Full Text:
Link

##### References:

[1] | Abadi, M.; Cardelli, L.; Curien, P. -L.; Lévy, J. -J.: Explicit substitutions. Journal of functional programming 1, No. 4, 375-416 (1991) · Zbl 0941.68542 |

[2] | L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder, Basic paramodulation and superposition, in: D. Kapur, ed., Proc. 11th. Int. Conf. on Automated Deduction, Saratoga Springs, NY (LNAI 607, Springer-Verlag, 1992) 462–476. · Zbl 0925.03052 |

[3] | Basin, D. A.; Constable, R. L.: Metalogical frameworks. Logical environments, 1-29 (1993) · Zbl 0922.03019 |

[4] | J. Bergstra and J. Tucker, Characterization of computable data types by means of a finite equational specification method, in: J. W. de Bakker and J. van Leeuwen, eds., Proc. 7th. Int. Colloquium on Automata, Languages and Programming (LNCS 81, Springer-Verlag, 1980) 76–90. · Zbl 0449.68003 |

[5] | P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau, and M. Vittek, ELAN: A logical framework based on computational systems, in: J. Meseguer, ed., Proc. First Int. Workshop on Rewriting Logic and its Applications (ENTCS 4, Elsevier, 1996) [This volume]. · Zbl 0912.68091 |

[6] | A. Bouhoula, J.-P. Jouannaud, and J. Meseguer, Specification and proof in membership equational logic, paper in preparation (1996). · Zbl 0938.68057 |

[7] | M. Cerioli and J. Meseguer, May I borrow your logic? (Transporting logical structure along maps), to appear in Theoretical Computer Science (1996). |

[8] | M. G. Clavel, S. Eker, P. Lincoln, and J. Meseguer, Principles of Maude, in: J. Meseguer, ed., Proc. First Int. Workshop on Rewriting Logic and its Applications (ENTCS 4, Elsevier, 1996) [This volume]. · Zbl 0912.68095 |

[9] | M. G. Clavel and J. Meseguer, Axiomatizing reflective logics and languages, in: G. Kiczales, ed., Proc. Reflection’96 (San Francisco, USA, April 1996) 263–288. |

[10] | M. G. Clavel and J. Meseguer, Reflection in rewriting logic, in: J. Meseguer, ed., Proc. First Int. Workshop on Rewriting Logic and its Applications (ENTCS 4, Elsevier, 1996) [This volume]. · Zbl 0917.68107 |

[11] | Cockett, J. R. B.; Seely, R. A. G.: Weakly distributive categories. Applications of categories in computer science, 45-65 (1992) · Zbl 0790.18004 |

[12] | H. Comon, Equational formulas in order-sorted algebras, in: M. S. Paterson, ed., Proc. 17th. Int. Colloquium on Automata, Languages and Programming, Warwick, England (LNCS 443, Springer-Verlag, 1990) 674–688. · Zbl 0774.68071 |

[13] | Comon, H.: Disunification: A survey. Computational logic: essays in honor of alan Robinson, 322-359 (1991) |

[14] | Dershowitz, N.; Jouannaud, J. P.: Rewrite systems. Handbook of theoretical computer science, vol. B: formal models and semantics, 243-320 (1990) · Zbl 0900.68283 |

[15] | Feferman, S.: Finitary inductively presented logics. Logic colloquium’88, 191-220 (1989) · Zbl 0682.03031 |

[16] | A. Felty and D. Miller, Encoding a dependent-type {\(\lambda\)}-calculus in a logic programming language, in: M. E. Stickel, ed., Proc. 10th. Int. Conf. on Automated Deduction, Kaiserslautern, Germany (LNAI 449, Springer-Verlag, 1990) 221–235. · Zbl 0708.68090 |

[17] | P. Gardner, Representing Logics in Type Theory, Ph.D. Thesis, Department of Computer Science, University of Edinburgh (1992). |

[18] | Girard, J. -Y.: Linear logic. Theoretical computer science 50, 1-102 (1987) · Zbl 0625.03037 |

[19] | J. A. Goguen and R. M. Burstall, Introducing institutions, in: E. Clarke and D. Kozen, eds., Proc. Logics of Programming Workshop (LNCS 164, Springer-Verlag, 1984) 221–256. · Zbl 0543.68021 |

[20] | Goguen, J. A.; Burstall, R. M.: Institutions: abstract model theory for specification and programming. Journal of the association for computing machinery 39, No. 1, 95-146 (1992) · Zbl 0799.68134 |

[21] | J. A. Goguen and J. Meseguer, Software for the rewrite rule machine, in: Proc. of the Int. Conf. on Fifth Generation Computer Systems (ICOT, Tokyo, Japan, 1988) 628–637. |

[22] | Goguen, J. A.; Meseguer, J.: Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions, and partial operations. Theoretical computer science 105, 217-273 (1992) · Zbl 0778.68056 |

[23] | Goguen, J. A.; Stevens, A.; Hobley, K.; Hilberdink, H.: 2OBJ: A meta-logical framework based on equational logic. Philosophical transactions of the royal society, series A 339, 69-86 (1992) |

[24] | J. A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud, Introducing OBJ, Technical report SRI-CSL-92-03, Computer Science Laboratory, SRI International (March 1992). To appear in J. A. Goguen and G. Malcolm, eds., Software Engineering with OBJ: Algebraic Specification in Practice (Cambridge University Press). |

[25] | Harper, R.; Honsell, F.; Plotkin, G.: A framework for defining logics. Journal of the association for computing machinery 40, No. 1, 143-184 (1993) · Zbl 0778.03004 |

[26] | R. Harper, D. Sannella, and A. Tarlecki, Structure and representation in LF, in: Proc. Fourth Annual IEEE Symp. on Logic in Computer Science (Asilomar, California, June 1989) 226–237. · Zbl 0716.68078 |

[27] | Hennessy, M.: The semantics of programming languages: an elementary introduction using structural operational semantics. (1990) · Zbl 0723.68067 |

[28] | Huet, G.: A unification algorithm for typed lambda calculus. Theoretical computer science 1, No. 1, 27-57 (1973) · Zbl 0332.02035 |

[29] | J. Jaffar and J. Lassez, Constraint logic programming, in: Proc. 14th. ACM Symp. on Principles of Programming Languages (Munich, Germany, 1987) 111–119. |

[30] | Jouannaud, J. -P.; Kirchner, C.: Solving equations in abstract algebra: A rule-based survey of unification. Computational logic: essays in honor of alan Robinson, 257-321 (1991) |

[31] | Kirchner, C.; Kirchner, H.; Rusinowitch, M.: Deduction with symbolic constraints. Revue francaise d’intelligence artificielle 4, No. 3, 9-52 (1990) |

[32] | Kirchner, C.; Kirchner, H.; Vittek, M.: Designing constraint logic programming languages using computational systems. Principles and practice of constraint systems: the newport papers, 133-160 (1995) |

[33] | C. Laneve and U. Montanari, Axiomatizing permutation equivalence in the {\(\lambda\)}-calculus, in: H. Kirchner and G. Levi, eds., Proc. Third Int. Conf. on Algebraic and Logic Programming, Volterra, Italy (LNCS 632, Springer-Verlag, 1992) 350–363. |

[34] | Martelli, A.; Montanari, U.: An efficient unification algorithm. ACM transactions on programming languages and systems 4, No. 2, 258-282 (1982) · Zbl 0478.68093 |

[35] | Martí-Oliet, N.; Meseguer, J.: From Petri nets to linear logic through categories: A survey. International journal of foundations of computer science 2, No. 4, 297-399 (1991) · Zbl 0766.68100 |

[36] | N. Martí-Oliet and J. Meseguer, Rewriting logic as a logical and semantic framework, Technical report SRI-CSL-93-05, Computer Science Laboratory, SRI International (August 1993). To appear in D. M. Gabbay, ed., Handbook of Philosophical Logic (Kluwer Academic Publishers). |

[37] | Martí-Oliet, N.; Meseguer, J.: General logics and logical frameworks. What is a logical system?, 355-392 (1994) · Zbl 0817.03005 |

[38] | Matthews, S.; Smaill, A.; Basin, D.: Experience with FS0 as a framework theory. Logical environments, 61-82 (1993) |

[39] | Meseguer, J.: General logics. Logic colloquium’87, 275-329 (1989) |

[40] | Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical computer science 96, 73-155 (1992) · Zbl 0758.68043 |

[41] | Meseguer, J.: A logical theory of concurrent objects and its realization in the maude language. Research directions in object-based concurrency, 314-390 (1993) |

[42] | J. Meseguer, Rewriting logic as a semantic framework for concurrency: A progress report, in: Proc. CONCUR’96 (LNCS, Springer-Verlag, 1996). |

[43] | J. Meseguer, Membership algebra, Lecture at the Dagstuhl Seminar on Specification and Semantics (July 1996). Extended version in preparation. |

[44] | Meseguer, J.; Goguen, J. A.: Order-sorted algebra solves the constructor-selector, multiple representation and coercion problems. Information and computation 104, 114-158 (1993) · Zbl 0796.68144 |

[45] | Meseguer, J.; Goguen, J. A.; Smolka, G.: Order-sorted unification. Journal of symbolic computation 8, 383-413 (1989) · Zbl 0691.03002 |

[46] | Meseguer, J.; Winkler, T.: Parallel programming in maude. Research directions in high-level parallel programming languages, 253-293 (1992) |

[47] | Milner, R.: A calculus of communicating systems. (1980) · Zbl 0452.68027 |

[48] | Milner, R.: Communication and concurrency. (1989) · Zbl 0683.68008 |

[49] | Nadathur, G.; Miller, D.: An overview of \({\lambda}\)Prolog. Fifth int. Joint conf. And symp. On logic programming, 810-827 (1988) |

[50] | R. Nieuwenhuis and A. Rubio, Theorem proving with ordering constrained clauses, in: D. Kapur, ed., Proc. 11th. Int. Conf. on Automated Deduction, Saratoga Springs, NY (LNAI 607, Springer-Verlag, 1992) 477–491. · Zbl 0925.03076 |

[51] | Paulson, L.: The foundation of a generic theorem prover. Journal of automated reasoning 5, 363-397 (1989) · Zbl 0679.68173 |

[52] | F. Pfenning, Elf: A language for logic definition and verified metaprogramming, in: Proc. Fourth Annual IEEE Symp. on Logic in Computer Science (Asilomar, California, June 1989) 313–322. · Zbl 0716.68079 |

[53] | G. D. Plotkin, A structural approach to operational semantics, Technical report DAIMI FN-19, Computer Science Department, Aarhus University (September 1981). |

[54] | Schmidt-Schauss, M.: Computational aspects of order-sorted logic with term declarations. (1989) · Zbl 0689.68001 |

[55] | Seely, R. A. G.: Linear logic, \ast-autonomous categories and cofree coalgebras. Categories in computer science and logic, Boulder, June 1987, 371-382 (1989) |

[56] | Smullyan, R. M.: Theory of formal systems. (1961) · Zbl 0097.24503 |

[57] | Troelstra, A. S.: Lectures on linear logic. (1992) · Zbl 0942.03535 |

[58] | C. Walther, A classification of many-sorted unification theories, in: J. H. Siekmann, ed., Proc. 8th. Int. Conf. on Automated Deduction, Oxford, England (LNCS 230, Springer-Verlag, 1986) 525–537. · Zbl 0643.68139 |

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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.