Skip to main content
SpringerLink
Log in

First order data types and first order logic

  • Conference paper
  • First Online:
Theoretical Aspects of Computer Software (TACS 1991)

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

Included in the following conference series:

Abstract

This paper concerns the relation between parameterized first order data types and first order logic. Augmenting first order logic by data type definitions yields in general a strictly stronger logic than first order logic. Some modeltheoretic properties of the new logic are investigated. While the new logic always fulfills the downward Skolem-Löwenheim property, compactness is fulfilled if and only if for the given data type definition the new logic has the same expressive power than first order logic. This last property is shown to be undecidable.

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. American National Standards Institute. The Programming Language Ada Reference Manual. LNCS vol. 155. Springer, 1983.

    Google Scholar 

  2. J. Bishop. Data Abstraction in Programming Languages. Addison-Wesley, 1986.

    Google Scholar 

  3. P. Buhmann. Disunifikation in modularen Termalgebren. Master's thesis, Universität des Saarlandes, 1991. In preparation.

    Google Scholar 

  4. R. M. Burstall and J. A. Goguen. Semantics of CLEAR, a specification language. In D. Björner, editor, Abstract Softare Specifications, pages 292–332. Springer LNCS, vol. 86, 1980.

    Google Scholar 

  5. C. C. Chang and H. J. Keisler. Model Theory. Studies in Logic and the Foundations of Mathematics, vol. 73. North-Holland Publishing Company, third edition, 1990.

    Google Scholar 

  6. H. Comon and P. Lescanne. Equational problems and disunification. Journal of Symbolic Computation, 7(3,4):371–425, 1989.

    Google Scholar 

  7. N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69–116, 1987.

    Google Scholar 

  8. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification, vol. 1. EATCS-Monographs on Theoretical Computer Science. Springer-Verlag, 1985.

    Google Scholar 

  9. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification, vol. 2. EATCS-Monographs on Theoretical Computer Science. Springer-Verlag, 1990.

    Google Scholar 

  10. H. B. Enderton. Mathematical Introduction to Logic. Academic Press, 1972.

    Google Scholar 

  11. S. A. Greibach. Theory of Program Structures: Schemes, Semantics, Verification. Lecture Notes in Computer Science, Vol. 35. Springer Verlag, 1975.

    Google Scholar 

  12. I. Guessarian. Algebraic Semantics. Lecture Notes in Computer Science, Vol. 99. Springer Verlag, 1979.

    Google Scholar 

  13. R. Harper, D. MacQueen, and R. Milner. Standard ML. Technical Report ECS-LFCS-86-2, Edinburgh University, 1986.

    Google Scholar 

  14. D. Kozen and J. Tiuryn. Logics of programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 14, pages 789–840. Elsevier Science Publishers, 1990.

    Google Scholar 

  15. T. Lehmann and J. Loeckx. The specification language of OBSCURE. In D. Sannella and A. Tarlecki, editors, 5th Workshop on Specification of Abstract Data Types, pages 131–153. Springer LNCS, vol. 332, 1987.

    Google Scholar 

  16. T. Lehmann and J. Loeckx. OBSCURE, a specification language for abstract data types. Technical Report A 19–90, Universität des Saarlandes, 1990. Submitted for publication.

    Google Scholar 

  17. P. Lindström. On extension of elementary logic. Theoria, 35:1–11, 1969.

    Google Scholar 

  18. B. Liskov and J. Guttag. Abstraction and Specification in Program Development. MIT press, 1986.

    Google Scholar 

  19. J. Loeckx. Algorithmic specifications: A constructive specification method for abstract data types. ACM Trans. Prog. Lang. Syst., 9(4), 1987.

    Google Scholar 

  20. J. Loeckx and K. Sieber. The Foundations of Program Verification. Wiley/Teubner, 2nd edition, 1987.

    Google Scholar 

  21. D. C. Luckham, D. M. R. Park, and M. S. Paterson. On formalized computer programs. J. Comput. Syst. Sci., 4:220–249, 1970.

    Google Scholar 

  22. D. MacQueen. Modules for standard ML. In [13], 1986.

    Google Scholar 

  23. M. J. Maher. Complete axiomatisations of the algebra of finite, rational and infinite trees. In Third Anual Symposium on Logic in Computer Science, pages 348–357, Edinburgh, Scotland, july 1988. IEEE.

    Google Scholar 

  24. J. D. Monk. Mathematical Logic. Graduate Texts in Mathematics, vol. 37. Springer, 1976.

    Google Scholar 

  25. M. Shaw, editor. Alphard: Form and Content. Springer, 1981.

    Google Scholar 

  26. J. Tiuryn. A survey of the logic of effective definitions. In E. Engeler, editor, Proceedings of the Workshop on Logics of Programs, pages 198–245. Springer LNCS, vol. 125, 1981.

    Google Scholar 

  27. R. Treinen. First order data types and first order logic. Interner Bericht A 01/91, Universität des Saarlandes, Jan. 1991.

    Google Scholar 

  28. D. A. Turner. Miranda: A non-strict functional language with polymorphic types. In J.-P. Jouannaud, editor, IFIP International Conference on Functional Programming Languages and Computer Architecture, pages 1–16. Springer LNCS, vol. 201, 1985.

    Google Scholar 

  29. J. Vuillemin. Correct and optimal implementations of recursion in a simple programming language. J. Comput. Syst. Sci., 9:332–354, 1974.

    Google Scholar 

  30. M. Wirsing, P. Pepper, H. Partsch, W. Dosch, and M. Broy. On hierarchies of abstract data types. Acta Informatica, 20:1–33, 1983.

    Article  Google Scholar 

  31. N. Wirth. Programming in MODULA-2. Springer, third edition, 1985.

    Google Scholar 

Download references

Author information

Author notes

  1. Ralf Treinen

    Present address: DFKI, Stuhlsatzenhausweg 3, W 6600, Saarbrücken, Germany

Authors and Affiliations

  1. FB14 — Dept. of Computer Science, Universität des Saarlandes, W6600, Saarbrücken, Germany

    Ralf Treinen

Authors
  1. Ralf Treinen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Takayasu Ito Albert R. Meyer

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Treinen, R. (1991). First order data types and first order logic. In: Ito, T., Meyer, A.R. (eds) Theoretical Aspects of Computer Software. TACS 1991. Lecture Notes in Computer Science, vol 526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54415-1_66

Download citation

  • DOI: https://doi.org/10.1007/3-540-54415-1_66

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54415-9

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation