zbMATH — the first resource for mathematics

Rewriting logic and Maude: Concepts and applications. (English) Zbl 0964.68069
Bachmair, Leo (ed.), Rewriting techniques and applications. 11th international conference, RTA 2000, Norwich, GB, July 10-12, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1833, 1-26 (2000).
Summary: For the most part, rewriting techniques have been developed and applied to support efficient equational reasoning and equational specification, verification, and programming. Therefore, a rewrite rule \(t\to t'\) has been usually interpreted as a directed equation \(t=t'\). Rewriting logic is a substantial broadening of the semantics given to rewrite rules. The equational reading is abandoned, in favor of a more dynamic interpretation. There are now in fact two complementary readings of a rule \(t\to t'\), one computational, and another logical: (i) computationally, the rewrite rule \(t\to t'\) is interpreted as a local transition in a concurrent system; (ii) logically, the rewrite rule \(t\to t'\) is interpreted as an inference rule. The experience gained so far strongly suggest that rewriting is indeed a very flexible and general formalism for both computational and logical applications. This means that from the computational point of view rewriting logic is a very expressive semantic framework, in which many different models of concurrency, languages, and distributed systems can be specified and programmed; and that from a logical point of view is a general logical framework in which many different logics can be represented and implemented. This paper introduces the main concepts of rewriting logic and of the Maude rewriting logic language, and discusses a wide range of semantic framework and logical framework applications that have been developed in rewriting logic using Maude.
For the entire collection see [Zbl 0941.00035].

68Q42 Grammars and rewriting systems
Maude; ELAN; Nuprl