Rewriting logic s 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 *L *in a framework logic *F *are understood as
mappings *L -> F *that translate one logic into the other in a conservative
way. The ease with which such maps can be defined for a number of
quite different logics of interest, including equational logic, Horn logic
with equality, linear logic, logics with quantifiers, and any sequent calculus
presentation of a logic for a very general notion of ``sequent,'' is discussed
in detail. Using the fact that rewriting logic is reflective, it is often
possible to reify inside rewriting logic itself a representation map *L
-> RWLogic *for the finitely presentable theories of *L*. Such
a reification takes the form of a map between the abstract data types representing
the finitary theories of *L* and of *RWLogic*. Representation
maps of this kind provide executable specifications of the corresponding
object logics within rewriting logic, which can be very useful for prototyping
purposes.

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 emphasized and illustrated with examples such as concurrent object-oriented programming and CCS. The relationship with structural operational semantics is discussed by means of examples. In addition, the way in which constraint solving fits within the rewriting logic framework is briefly explained. Finally, the use of rewriting logic as a logic of change that overcomes the frame problem in AI is also discussed.

(BibTeX entry) (gzip'ed Postscript)

back home Formal Methods and Declarative Languages Laboratory Computer Science Laboratory, SRI International