Skip to main content
SpringerLink
Log in

Extensions of initial models and their second-order proof systems

  • Conference paper
  • First Online:
Higher-Order Algebra, Logic, and Term Rewriting (HOA 1993)

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

Abstract

Besides explicit axioms, an algebraic specification language contains model-theoretic constraints such as initiality. For proving properties of specifications and refining them to programs, an axiomatization of these constraints is needed; unfortunately, no effective, sound and complete proof system can be constructed for initial models, and a fortiori for their extensions.

In this paper, we construct non-effective second-order axiomatizations for the initiality constraint, and its recently proposed extensions (minimal, quasi-free and surjective models) designed to deal with disjunction and existential quantification.

This research was mostly carried out at Centre National de la Recherche Scientifique, Centre de Recherche en Informatique de Nancy.

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. M. Bidoit and G. Bernot. Proving correctness of algebraically specified software: Modularity and observability issues. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, AMAST'91, pages 139–161. Springer-Verlag, 1992.

    Google Scholar 

  2. M. Broy and al. The requirement and design specification language spectrum: an introduction. Technical Report TUM-I9140, Technische Universität München, 1991.

    Google Scholar 

  3. R. Burstall and J. Goguen. Semantics of CLEAR, a Specification Language. In D. Bjorner, editor, Abstract software specifications, Proc. 1979 Copenhagen Winter School, volume 86, pages 292–332. Springer, 1980.

    Google Scholar 

  4. CIP Language Group. The Munich Project CIP — Vol. I: The Language, volume 183 of Lecture Notes in Computer Science. Springer, 1985.

    Google Scholar 

  5. N. Denyer. Pure second-order logic. Notre-Dame Journal of Formal Logic, 33(2):220, 1992.

    Google Scholar 

  6. H. Ehrig and B. Mahr. Fundamentals of algebraic specification: Volume 1. Equations and initial semantics. Springer Verlag, 1985.

    Google Scholar 

  7. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 2: Module Specifications and Constraints, volume 21 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1990.

    Google Scholar 

  8. A. Schmidt, Die Zulässigkeit der Behandlung mehrsortiger Theorien mittels der üblichen einsortigen Prädikatenlogik, Math. Ann. 123, pages 187–200, 1951.

    Google Scholar 

  9. J. Goguen and R. Burstall. Institutions: Abstract model theory for specification and programming. J. ACM, 39(1):95–146, Jan. 1992.

    Google Scholar 

  10. S. Kaplan. Positive/negative conditional rewriting. In Conditional Term Rewriting, volume 308 of Lecture Notes in Computer Science. Springer, 1988.

    Google Scholar 

  11. D. MacQueen and D. Sannella. Completeness of proof systems for equational specifications. IEEE TSE, SE-11(5), May 1985.

    Google Scholar 

  12. P. Nivela and F. Orejas. Initial behaviour semantics for algebraic specifications. In Recent Trends in Data Type Specification, number 332 in Lecture Notes in Computer Science, pages 184–207. Springer-Verlag, 1987.

    Google Scholar 

  13. F. Nourani. On induction for programming logics: syntax, semantics, and inductive closure. EATCS Bulletin, 13:51–64, 1981.

    Google Scholar 

  14. P. Rathmann and M. Winslett. Circumscribing equality. In Proc. of the 8th Nat. Conf. on Art. Int. (AAAI-89), pages 468–473, 1989.

    Google Scholar 

  15. P.-Y. Schobbens. Surjective Circumscription Proc. Dutch/German Workshop on Non-Monotonic Logics, W. Nejdl ed., Aachen, Dec. 1993.

    Google Scholar 

  16. P.-Y. Schobbens. Second-Order Proof Systems for Algebraic Specification Languages Proc. 9th Workshop on Specification of Abstract Data Types, F. Orejas ed., to appear.

    Google Scholar 

  17. P.-Y. Schobbens. Exceptions for software specification: on the meaning of ”but”. Technical report, Univ. Cath. de Louvain, 1989.

    Google Scholar 

  18. M. Wirsing. Structured algebraic specifications: A kernel language. Theoretical Computer Science, 42:123–249, 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fac. Univ. Notre-Dame de la Paix, Institut d'Informatique, Rue Grandgagnage 21, B-5000, Namur

    Pierre-Yves Schobbens

Authors
  1. Pierre-Yves Schobbens
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jan Heering Karl Meinke Bernhard Möller Tobias Nipkow

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schobbens, PY. (1994). Extensions of initial models and their second-order proof systems. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds) Higher-Order Algebra, Logic, and Term Rewriting. HOA 1993. Lecture Notes in Computer Science, vol 816. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58233-9_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-58233-9_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58233-5

  • Online ISBN: 978-3-540-48579-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation