Membership algebra as a logical framework for equational specification

José Meseguer

doi:10.1007/3-540-64299-4_26

Membership algebra as a logical framework for equational specification

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

This paper proposes membership equational logic-a Horn logic in which the basic predicates are equations t=t and membership assertions t: s stating that a term t belongs to a sort s-as a logical framework in which a very wide range of total and partial equational specification formalisms can be naturally represented. Key features of this logic include: simplicity, liberality and equational character; generality and expressiveness in supporting subsorts, overloading, errors and partiality; and efficient implementability in systems such as Maude. The paper presents the basic properties of the logic and its models, and discusses in detail how many total and partial equational specification formalisms, including order-sorted algebra and partial membership equational logic, can be represented in it, as well as the practical benefits in terms of tool reusability that this opens up for other languages, including CASL.

Original language	English (US)
Title of host publication	Recent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers
Editors	Francesco Parisi Presicce
Publisher	Springer-Verlag
Pages	18-61
Number of pages	44
ISBN (Print)	3540642994, 9783540642992
DOIs	https://doi.org/10.1007/3-540-64299-4_26
State	Published - Jan 1 1998
Externally published	Yes
Event	12th International Workshop on Algebraic Development Techniques, WADT 1997 - Tarquinia, Italy Duration: Jun 3 1997 → Jun 7 1997

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1376
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	12th International Workshop on Algebraic Development Techniques, WADT 1997
Country	Italy
City	Tarquinia
Period	6/3/97 → 6/7/97

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/3-540-64299-4_26

Fingerprint Dive into the research topics of 'Membership algebra as a logical framework for equational specification'. Together they form a unique fingerprint.

Cite this

Meseguer, J. (1998). Membership algebra as a logical framework for equational specification. In F. P. Presicce (Ed.), Recent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers (pp. 18-61). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1376). Springer-Verlag. https://doi.org/10.1007/3-540-64299-4_26

Membership algebra as a logical framework for equational specification. / Meseguer, José.

Recent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers. ed. / Francesco Parisi Presicce. Springer-Verlag, 1998. p. 18-61 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1376).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Meseguer, J 1998, Membership algebra as a logical framework for equational specification. in FP Presicce (ed.), Recent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1376, Springer-Verlag, pp. 18-61, 12th International Workshop on Algebraic Development Techniques, WADT 1997, Tarquinia, Italy, 6/3/97. https://doi.org/10.1007/3-540-64299-4_26

Meseguer J. Membership algebra as a logical framework for equational specification. In Presicce FP, editor, Recent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers. Springer-Verlag. 1998. p. 18-61. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-64299-4_26

Meseguer, José. / Membership algebra as a logical framework for equational specification. Recent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers. editor / Francesco Parisi Presicce. Springer-Verlag, 1998. pp. 18-61 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{42965bc2a3c54fa99b7409682f02afcb,

title = "Membership algebra as a logical framework for equational specification",

abstract = "This paper proposes membership equational logic-a Horn logic in which the basic predicates are equations t=t and membership assertions t: s stating that a term t belongs to a sort s-as a logical framework in which a very wide range of total and partial equational specification formalisms can be naturally represented. Key features of this logic include: simplicity, liberality and equational character; generality and expressiveness in supporting subsorts, overloading, errors and partiality; and efficient implementability in systems such as Maude. The paper presents the basic properties of the logic and its models, and discusses in detail how many total and partial equational specification formalisms, including order-sorted algebra and partial membership equational logic, can be represented in it, as well as the practical benefits in terms of tool reusability that this opens up for other languages, including CASL.",

author = "Jos{\'e} Meseguer",

year = "1998",

month = jan,

day = "1",

doi = "10.1007/3-540-64299-4_26",

language = "English (US)",

isbn = "3540642994",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer-Verlag",

pages = "18--61",

editor = "Presicce, {Francesco Parisi}",

booktitle = "Recent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers",

note = "12th International Workshop on Algebraic Development Techniques, WADT 1997 ; Conference date: 03-06-1997 Through 07-06-1997",

}

TY - GEN

T1 - Membership algebra as a logical framework for equational specification

AU - Meseguer, José

PY - 1998/1/1

Y1 - 1998/1/1

N2 - This paper proposes membership equational logic-a Horn logic in which the basic predicates are equations t=t and membership assertions t: s stating that a term t belongs to a sort s-as a logical framework in which a very wide range of total and partial equational specification formalisms can be naturally represented. Key features of this logic include: simplicity, liberality and equational character; generality and expressiveness in supporting subsorts, overloading, errors and partiality; and efficient implementability in systems such as Maude. The paper presents the basic properties of the logic and its models, and discusses in detail how many total and partial equational specification formalisms, including order-sorted algebra and partial membership equational logic, can be represented in it, as well as the practical benefits in terms of tool reusability that this opens up for other languages, including CASL.

AB - This paper proposes membership equational logic-a Horn logic in which the basic predicates are equations t=t and membership assertions t: s stating that a term t belongs to a sort s-as a logical framework in which a very wide range of total and partial equational specification formalisms can be naturally represented. Key features of this logic include: simplicity, liberality and equational character; generality and expressiveness in supporting subsorts, overloading, errors and partiality; and efficient implementability in systems such as Maude. The paper presents the basic properties of the logic and its models, and discusses in detail how many total and partial equational specification formalisms, including order-sorted algebra and partial membership equational logic, can be represented in it, as well as the practical benefits in terms of tool reusability that this opens up for other languages, including CASL.

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

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

U2 - 10.1007/3-540-64299-4_26

DO - 10.1007/3-540-64299-4_26

M3 - Conference contribution

AN - SCOPUS:84957873927

SN - 3540642994

SN - 9783540642992

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 18

EP - 61

BT - Recent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers

A2 - Presicce, Francesco Parisi

PB - Springer-Verlag

T2 - 12th International Workshop on Algebraic Development Techniques, WADT 1997

Y2 - 3 June 1997 through 7 June 1997

ER -