TY - GEN
T1 - Specification and proof in membership equational logic
AU - Bouhoula, Adel
AU - Jouannaud, Jean Pierre
AU - Meseguer, Josè
N1 - Funding Information:
(Supported by the ESPRIT Basic Research Working Group 22457 - Construction of Computational Logics II, the HCM Research Contract CONSOLE, the O ce of Naval Research Contracts N00014-95-C-0225 and N00014-96-C-0114, National Science Foundation Grant CCR-9633363, and by the Advanced Software Enrichment Project of the Information Technology Promotion Agency, Japan (IPA).
Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1997.
PY - 1997
Y1 - 1997
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84957029814&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84957029814&partnerID=8YFLogxK
U2 - 10.1007/bfb0030589
DO - 10.1007/bfb0030589
M3 - Conference contribution
AN - SCOPUS:84957029814
SN - 9783540627814
SN - 9783540627814
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 67
EP - 92
BT - TAPSOFT 1997
A2 - Bidoit, Michel
A2 - Bidoit, Michel
A2 - Dauchet, Max
A2 - Dauchet, Max
PB - Springer
T2 - 7th International Joint Conference on Theory and Practice of Software Development, TAPSOFT 1997
Y2 - 14 April 1997 through 18 April 1997
ER -