Specification and proof in membership equational logic

21Citations
Citations of this article
9Readers
Mendeley users who have this article in their library.

This article is free to access.

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.

Cite

CITATION STYLE

APA

Bouhoula, A., Jouannaud, J. P., & Meseguer, J. (1997). Specification and proof in membership equational logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1214, pp. 67–92). Springer Verlag. https://doi.org/10.1007/bfb0030589

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free