TY - JOUR

T1 - Rewriting Logic as a Logical and Semantic Framework This paper is a short version of [36], where the reader can find more examples and details not discussed here.

AU - Martí-Oliet, Narciso

AU - Meseguer, José

N1 - Copyright:
Copyright 2014 Elsevier B.V., All rights reserved.

PY - 1996

Y1 - 1996

N2 - Rewriting logic [40] 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 [39], 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 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 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. 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.

AB - Rewriting logic [40] 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 [39], 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 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 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. 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.

UR - http://www.scopus.com/inward/record.url?scp=18944373994&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=18944373994&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)00040-4

DO - 10.1016/S1571-0661(04)00040-4

M3 - Article

AN - SCOPUS:18944373994

VL - 4

SP - 190

EP - 225

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - C

ER -