Abstract
This paper is part of a long-term effort to increase expressiveness 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, where they 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 order-sorted 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.
Supported by Office of Naval Research contracts N00014-95-C-0225 and N00014-96-C-0114, by the Information Technology Promotion Agency, Japan, and by the Centre National de la Recherche Scientifique, France
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Adel Bouhoula. Automated Theorem Proving by Test Set Induction. Journal of Symbolic Computation, to appear.
Adel Bouhoula and Jean-Pierre Jouannaud. Automata-driven automated induction. submitted, 1996.
Adel Bouhoula, Jean-Pierre Jouannaud, and José Meseguer. Specification and proof in membership equational logic. Draft, 1996.
A-C. Caron, J.-L. Coquidé, and M. Dauchet. Encompassment properties and automata with constraints. In Proc. 5th RTA, Montréal, LNCS 690, 1993.
Hubert Comon. Inductive proofs by specifications transformation. In Proc. 3rd RTA, Chapel Hill, LNCS 355, 1989.
Hubert Comon. Completion of rewrite systems with membership constraints. In Proc. 19th ICALP, Vienna, LNCS 623, 1992.
Hubert Comon and Catherine Delor. Equational formulae with membership constraints. Information and Computation, 112(2):167–216, 1994.
Hubert Comon and Florent Jacquemard. Ground reducibility and automata with disequality constraints. In Proc. 11th STACS, Caen, 1994.
Nachum Dershowitz and Mitsuhiro Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111–138, 1990.
Kokichi Futatsugi, Joseph Goguen, Jean-Pierre Jouannaud, and Jose Meseguer. Principles of OBJ2. In Proc. 12th ACM POPL, 1985.
P. Gabriel and F. Ulmer. Lokal präsentierbare Kategorien. Springer Lecture Notes in Mathematics No. 221, 1971.
J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In Current Trends in Programming Methodology, vol. 4, pages 80–149, 1978.
Joseph Goguen, Jean-Pierre Jouannaud, and José Meseguer. Operational semantics for order-sorted algebra. In Proc. 12th ICALP, LNCS 194, 1985.
Joseph Goguen and José Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 105:217–273, 1992.
Claus Hintermeier, Claude Kirchner, and Hélène Kirchner. Dynamically-typed computations for order-sorted equational presentations. Proc. 20th ICALP, Jerusalem, LNCS 700, 1994.
Jean-Pierre Jouannaud, Claude Kirchner, Hélène Kirchner, and Aristide Megrelis. OBJ: Programming with equalities, subsorts, overloading and parametrization. Journal of Logic Programming, 12:257–279, 1992.
Jean-Pierre Jouannaud and B. Waldmann. Reductive conditional term rewriting systems. In Proc. Third IFIP Working Conference on Formal Description of Programming Concepts, Ebberup, Denmark, 1986.
Stephane Kaplan. Conditional rewrite rules. Theoretical Computer Science, 33:175–193, 1984.
Denis Lugiez and Jean-Luc Moysset. Tree automata help one to solve equational formulae in ac-theories. Journal of Symbolic Computation, 18(4):297–318, 1994.
M. Clavel, S. Eker, P. Lincoln and J. Meseguer. Principles of Maude. In Proceedings of the 1st International Workshop on Rewriting Logic and its Applications, Electronic Notes in Theoretical Computer Science 4, 1996.
José Meseguer. Membership algebra, 1996. Lecture at the Dagstuhl Seminar on Specification and Semantics, Report 151, 9628, 19–21, 1996.
Jose Méseguer and Timothy Winkler. Parallel programming in Maude. In J.B. Banâtre and D. Le Métayer, editors, Research Directions in High-Level Parallel Programming Languages, pages 253–293. Springer-Verlag, June 1991.
T. Mossakowski. Equivalences among various logical frameworks of partial algebras. In Proc. 9th CSL, Paderborn, 1995, LNCS 1092, 1996.
H. Reichel. Initial Computability, Algebraic Specifications, and Partial Algebras. Oxford University Press, 1987.
Gert Smolka. Order-sorted Horn logic: Semantics and deduction. Research Report SR-86-17, Univ. Kaiserslautern, October 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouhoula, A., Jouannaud, JP., Meseguer, J. (1997). Specification and proof in membership equational logic. In: Bidoit, M., Dauchet, M. (eds) TAPSOFT '97: Theory and Practice of Software Development. CAAP 1997. Lecture Notes in Computer Science, vol 1214. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0030589
Download citation
DOI: https://doi.org/10.1007/BFb0030589
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62781-4
Online ISBN: 978-3-540-68517-3
eBook Packages: Springer Book Archive