Membership algebra as a logical framework for equational specification

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationRecent Trends in Algebraic Development Techniques - 12th International Workshop, WADT 1997, Selected Papers
EditorsFrancesco Parisi Presicce
PublisherSpringer-Verlag
Pages18-61
Number of pages44
ISBN (Print)3540642994, 9783540642992
DOIs
StatePublished - Jan 1 1998
Externally publishedYes
Event12th International Workshop on Algebraic Development Techniques, WADT 1997 - Tarquinia, Italy
Duration: Jun 3 1997Jun 7 1997

Publication series

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

Other

Other12th International Workshop on Algebraic Development Techniques, WADT 1997
CountryItaly
CityTarquinia
Period6/3/976/7/97

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

Cite this