Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic

Manuel Clavel; José Meseguer; Miguel Palomino

doi:10.1016/j.tcs.2006.12.009

Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic

Manuel Clavel, José Meseguer, Miguel Palomino

Research output: Contribution to journal › Article › peer-review

Abstract

We show that the generalized variant of formal systems where the underlying equational specifications are membership equational theories, and where the rules are conditional and can have equations, memberships and rewrites in the conditions is reflective. We also show that membership equational logic, many-sorted equational logic, and Horn logic with equality are likewise reflective. These results provide logical foundations for reflective languages and tools based on these logics.

Original language	English (US)
Pages (from-to)	70-91
Number of pages	22
Journal	Theoretical Computer Science
Volume	373
Issue number	1-2
DOIs	https://doi.org/10.1016/j.tcs.2006.12.009
State	Published - Mar 22 2007

Keywords

Maude
Membership equational logic
Reflection
Reflective logics
Reflective programming languages
Rewriting logic
Universal theories

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1016/j.tcs.2006.12.009

Library availability

Discover UIUC Full Text

Cite this

@article{766b41a94e2447afa87d3ac97cc7259b,

title = "Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic",

abstract = "We show that the generalized variant of formal systems where the underlying equational specifications are membership equational theories, and where the rules are conditional and can have equations, memberships and rewrites in the conditions is reflective. We also show that membership equational logic, many-sorted equational logic, and Horn logic with equality are likewise reflective. These results provide logical foundations for reflective languages and tools based on these logics.",

keywords = "Maude, Membership equational logic, Reflection, Reflective logics, Reflective programming languages, Rewriting logic, Universal theories",

author = "Manuel Clavel and Jos{\'e} Meseguer and Miguel Palomino",

note = "Funding Information: IThis work is an extended and revised version of a paper presented at WRLA 2002, including the detailed proofs of all the results. Research was supported by ONR Grant N00014-02-1-0715, NSF Grant CCR-0234524, and by DARPA through Air Force Research Laboratory Contract F30602-02-C-0130; and by the Spanish projects MELODIAS TIC 2002-01167 and MIDAS TIC 2003-0100. ∗Corresponding author. Tel.: +34 913947555; fax: +34 913947529. E-mail addresses: [email protected] (M. Clavel), [email protected] (J. Meseguer), [email protected] (M. Palomino).",

year = "2007",

month = mar,

day = "22",

doi = "10.1016/j.tcs.2006.12.009",

language = "English (US)",

volume = "373",

pages = "70--91",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier B.V.",

number = "1-2",

}

TY - JOUR

T1 - Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic

AU - Clavel, Manuel

AU - Meseguer, José

AU - Palomino, Miguel

N1 - Funding Information: IThis work is an extended and revised version of a paper presented at WRLA 2002, including the detailed proofs of all the results. Research was supported by ONR Grant N00014-02-1-0715, NSF Grant CCR-0234524, and by DARPA through Air Force Research Laboratory Contract F30602-02-C-0130; and by the Spanish projects MELODIAS TIC 2002-01167 and MIDAS TIC 2003-0100. ∗Corresponding author. Tel.: +34 913947555; fax: +34 913947529. E-mail addresses: [email protected] (M. Clavel), [email protected] (J. Meseguer), [email protected] (M. Palomino).

PY - 2007/3/22

Y1 - 2007/3/22

N2 - We show that the generalized variant of formal systems where the underlying equational specifications are membership equational theories, and where the rules are conditional and can have equations, memberships and rewrites in the conditions is reflective. We also show that membership equational logic, many-sorted equational logic, and Horn logic with equality are likewise reflective. These results provide logical foundations for reflective languages and tools based on these logics.

AB - We show that the generalized variant of formal systems where the underlying equational specifications are membership equational theories, and where the rules are conditional and can have equations, memberships and rewrites in the conditions is reflective. We also show that membership equational logic, many-sorted equational logic, and Horn logic with equality are likewise reflective. These results provide logical foundations for reflective languages and tools based on these logics.

KW - Maude

KW - Membership equational logic

KW - Reflection

KW - Reflective logics

KW - Reflective programming languages

KW - Rewriting logic

KW - Universal theories

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

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

U2 - 10.1016/j.tcs.2006.12.009

DO - 10.1016/j.tcs.2006.12.009

M3 - Article

AN - SCOPUS:33847315579

SN - 0304-3975

VL - 373

SP - 70

EP - 91

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 1-2

ER -

Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic

Abstract

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this