Skip to main content
SpringerLink
Log in

A proof system for conditional algebraic specifications

  • Chapter 1 Theory Of Conditional And Horn Clause Systems
  • Conference paper
  • First Online:
Conditional and Typed Rewriting Systems (CTRS 1990)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 516))

Included in the following conference series:

Abstract

Algebraic specifications provide a formal basis for designing data-structures and reasoning about their properties. Sufficient-completeness and consistency are fundamental notions for building algebraic specifications in a modular way. We give in this paper effective methods for testing these properties for specifications with conditional axioms.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. N. Dershowitz. Computing with rewrite systems. Information and Control, 65(2/3):122–157, 1985.

    Google Scholar 

  2. N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1 & 2):69–116, 1987.

    Google Scholar 

  3. N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the Association for Computing Machinery, 22(8):465–476, 1979.

    Google Scholar 

  4. H. Ehrig, H. Kreowsky, and P. Padawitz. Stepwise specifications and implementation of adt. In Proceedings International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, volume 62, 1978.

    Google Scholar 

  5. H. Ganzinger. Ground term confluence in parametric conditional equational specifications. In F. Brandenburg, G. Vidal-Naquet, and M. Wirsing, editors, Proceedings STACS 87, pages 286–298. Springer-Verlag, 1987. Lecture Notes in Computer Science, volume 247.

    Google Scholar 

  6. 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 Yeh R., editor, Current Trends in Programming methodology IV: Data structuring, pages 80–144. Prentice Hall, 1978.

    Google Scholar 

  7. G. Huet and J-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25(2):239–266, October 1982. Preliminary version in Proceedings 21st Symposium on Foundations of Computer Science, IEEE, 1980.

    Google Scholar 

  8. J.-P. Jouannaud and E. Kounalis. Proof by induction in equational theories without constructors. In Proceedings 1st Symp. on Logic In Computer Science, pages 358–366, Boston (USA), 1986.

    Google Scholar 

  9. D. Kapur, P. Narendran, and H. Zhang. On sufficient completeness and related properties of term rewriting systems. Acta Informatica, 24:395–415, 1987.

    Google Scholar 

  10. H. Kirchner. A general inductive completion algorithm and application to abstract data types. In R. Shostak, editor, Proceedings 7th international Conference on Automated Deduction, pages 282–302. Springer-Verlag, Lecture Notes in Computer Science, 1984.

    Google Scholar 

  11. D.E. Knuth and P.B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, 1970.

    Google Scholar 

  12. E. Kounalis. Completeness in data type specifications. In B. Buchberger, editor, Proceedings EUROCAL Conference, pages 348–362, Linz (Austria), 1985. Springer-Verlag. Lecture Notes in Computer Science, volume 204.

    Google Scholar 

  13. E. Kounalis. Pumping lemmas for tree languages generated by rewrite systems. In Fifteenth International Symposium on Mathematical Foundations of Computer Science, Banská Bystrica (Czechoslovakia), 1990. Springer-Verlag. Lecture Notes in Computer Science.

    Google Scholar 

  14. E. Kounalis and Rusinowitch M. Mechanizing inductive reasoning. EATCS Bulletin, 41:216–226, 1990.

    Google Scholar 

  15. E. Kounalis and M. Rusinowitch. On word problem in Horn logic. In J.-P. Jouannaud and S. Kaplan, editors, Proceedings on the first international workshop on Conditional Term Rewriting, pages 144–160. Springer-Verlag, 1987. Lecture Notes in Computer Science, volume 308. See also the extended version published in Journal of Symbolic Computation, number 1 & 2, 1991.

    Google Scholar 

  16. E. Kounalis and M. Rusinowitch. Mechanizing inductive reasoning. In Proceedings of the AAAI Conference, pages 240–245, Boston, 1990. AAAI Press and the MIT Press.

    Google Scholar 

  17. D.R. Musser. On proving inductive properties of abstract data types. In Proceedings 7th ACM Symp. on Principles of Programming Languages, pages 154–162. Association for Computing Machinery, 1980.

    Google Scholar 

  18. Padawitz P. Reductive validity. In Proceedings 2nd International Workshop on Conditional Rewriting Systems, Montreal (Canada), 1990. S. Kaplan and M. Okada.

    Google Scholar 

  19. P. Padawitz. New results on completeness and consistency of abstract data types. Proceedings 9th Symposium on Mathematical Foundations of Computer Science, Springer Verlag, Lecture Notes in Computer Science, 88:460–473, 1980.

    Google Scholar 

  20. P. Padawitz. Computing in Horn Clause Theories. Springer-Verlag, 1988.

    Google Scholar 

  21. D. Plaisted. Semantic confluence tests and completion methods. In Journal Information and Control 65, pages 182–215, 1985.

    Google Scholar 

  22. J.-L. Rémy. Etude des systèmes de réécriture conditionnels et applications aux types abstraits algébriques. Thèse d'Etat de l'Institut National Polytechnique de Lorraine, Nancy (France), 1982.

    Google Scholar 

  23. M. Rusinowitch. Démonstration automatique par des techniques de réécriture. Thèse d'Etat de l'Université de Nancy I, 1987. Also published by InterEditions, Collection Science Informatique, directed by G. Huet, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIN, BP239, 54506, Vandœuvre-les-Nancy, France

    Emmanuel Kounalis & Michaël Rusinowitch

  2. INRIA Lorraine, BP 101, 54600, Villers-les-Nancy, France

    Emmanuel Kounalis & Michaël Rusinowitch

Authors
  1. Emmanuel Kounalis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michaël Rusinowitch
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

S. Kaplan M. Okada

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kounalis, E., Rusinowitch, M. (1991). A proof system for conditional algebraic specifications. In: Kaplan, S., Okada, M. (eds) Conditional and Typed Rewriting Systems. CTRS 1990. Lecture Notes in Computer Science, vol 516. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54317-1_80

Download citation

  • DOI: https://doi.org/10.1007/3-540-54317-1_80

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54317-6

  • Online ISBN: 978-3-540-47558-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation