Specification and proof in membership equational logic

Adel Bouhoula, Jean Pierre Jouannaud, Josè Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper is part of a long-term effort to increase expressiv eness of algebraic specification languages while at the same time having a simple semantic basis on which efficient execution by rewriting and powerful theorem-proving tools can be based. In particular, our rewriting techniques provide semantic foundations for Maude's functional sublanguage, wherethey have been efficiently implemented. Membership equational logic is quite simple, and yet quite powerful. Its atomic formulae are equations and sort membership assertions, and its sentences are Horn clauses. It extends in a conservative way both ordersorted equational logic and partial algebra approaches, while Horn logic can be very easily encoded. After introducing the basic concepts of the logic, we give conditions and proof rules with which efficient equational deduction by rewriting can be achieved. We also give completion techniques to transform a specification into one meeting these conditions. We address the important issue of proving sufficient completeness of a specification. Using tree-automata techniques, we develop a test set based approach for proving inductive theorems about a specification. Narrowing and proof techniques for parameterized specifications are investigated as well. Finally, we discuss the generality of our approach and how it extends several previous approaches.

Original languageEnglish (US)
Title of host publicationTAPSOFT 1997
Subtitle of host publicationTheory and Practice of Software Development - 7th International Joint Conference CAAP/FASE, Proceedings
EditorsMichel Bidoit, Michel Bidoit, Max Dauchet, Max Dauchet
PublisherSpringer-Verlag Berlin Heidelberg
Pages67-92
Number of pages26
ISBN (Print)9783540627814, 9783540627814
DOIs
StatePublished - 1997
Externally publishedYes
Event7th International Joint Conference on Theory and Practice of Software Development, TAPSOFT 1997 - Lille, France
Duration: Apr 14 1997Apr 18 1997

Publication series

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

Other

Other7th International Joint Conference on Theory and Practice of Software Development, TAPSOFT 1997
CountryFrance
CityLille
Period4/14/974/18/97

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Specification and proof in membership equational logic'. Together they form a unique fingerprint.

Cite this