Skip to main content
SpringerLink
Log in

Integrating logic programming and equational specification of abstract data types

  • Submitted Papers
  • Conference paper
  • First Online:
Algebraic and Logic Programming (ALP 1988)

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

Included in the following conference series:

  • 211 Accesses

Abstract

We discuss various semantics of many-sorted logic programs with equality both from the viewpoint of algebraic specifications as well as from the viewpoint of logic programming. We define model-theoretic semantics based on initial models, least generalized Herbrand models and a least fixpoint construction, and we investigate proof-theoretic semantics based on resolution and unification modulo a set of conditional equations. Generalizing ordinary SLD derivations, we introduce so-called SLDE derivations and SLDE trees and study their correctness and completeness properties. We define a translation of logic programs LPE with equality into equivalent logic programs LPø with empty equational part such that LPE satisfies a goal G if and only if LPø satisfies G.

(electronic mail on EARN/BITNET: BEIERLE at DSøLILOG, PLETAT at DSøLILOG)

The research reported here has been carried out within the international EUREKA Project PROTOS (EU 56).

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Apt, K. R. and van Emden, M. H.: Contributions to The Theory of Logic Programming. Journal of the ACM, Volume 29, Number 3, 1982.

    Google Scholar 

  2. Bosco, P. G., Giovannetti, K. and Moiso, C.: Refined Strategies for Semantic Unification. Proc. TAPSOFT-87, LNCS Vol 250, Springer Verlag, 1987.

    Google Scholar 

  3. Beierle, C. and Pletat, U.: Semantics of Logic Programs with Equational Abstract Data Type Specifications. LILOG Report 38, IBM Deutschland GmbH, Stuttgart, 1988.

    MATH  Google Scholar 

  4. Clocksin, W. F. and Mellish, C. S.: Programming in Prolog. Springer Verlag, Berlin 1982.

    MATH  Google Scholar 

  5. De Groot, D. and Lindstrom, G. (eds): Functional and Logic Programming, Prentice Hall, 1986.

    Google Scholar 

  6. van Emden, M. H. and Kowalski, R. A.: The Semantics of Predicate Logic as a Programming Language. Journal of the ACM, Volume 23, Number 4, 1976.

    Google Scholar 

  7. Ehrig, H. and Mahr, B.: Foundations of Algebraic Specification 1. Springer Verlag, Berlin 1985.

    Book  MATH  Google Scholar 

  8. Goguen, J. G. and Meseguer, J.: EQLOG: Equality. Types and Generic Modules for Logic Programming. In [DeGL 86].

    Google Scholar 

  9. Gallier, J. H. and Raatz, S.: SLD-Resolution Methods for Horn Clauses with Equality Based on K-Unification. In. Proc. 1986 Symposium on Logic Programming, Salt Lake City, IEEE Computer Society Press, 1986.

    Google Scholar 

  10. Goguen, J. A. and Thatcher, J. W. and Wagner, E. An Initial Algebra Approach to The Specification, Correctness and Implementation of Abstract Data Types. In: Current Trends in Programming Methodology, R. T. Yeh, (ed), Prentice-Hall, 1978.

    Google Scholar 

  11. Hölldobler, S.: Equational Logic Programming. Proc. Symposium on Logic Programming, 1987.

    Google Scholar 

  12. Hussmann, H.: Unification in Conditional-Equational Theories. Proc. EUROCAL 85, LNCS, Springer Verlag, 1985.

    Google Scholar 

  13. Jaffar, J., Lassez, J.-L., Maher, M.J.: A Theory of Complete Logic Programs with Equality. J. of Logic Programming, 1984, pp. 211–223.

    Google Scholar 

  14. Jaffar, J., Lassez, J.-L., Maher, M.J.: A Logic Programming Language scheme. In [DeGl 86].

    Google Scholar 

  15. Lloyd, J. W.: Foundations of Logic Programming. Springer Verlag, Berlin 1984.

    Book  MATH  Google Scholar 

  16. Martelli, A., Montanari, U.: An Efficient Unification Algorithm. ACM TOPLAS, Vol. 4(2), 1982, pp. 258–282.

    Article  MATH  Google Scholar 

  17. Mahr, B. and Makowsky, J. A.: Characterizing Specification Languages which Admit Initial Semantics. Theoretical Computer Science, Volume 31, North-Holland 1984.

    Google Scholar 

  18. Martelli, A., Moiso, C. and Rossi, G.F.: An Algorithm for Unification in Equational Theories. In: Proc. 1986 Symposium on Logic Programming, Salt Lake City, IEEE Computer Society Press, 1986.

    Google Scholar 

  19. Pletat, U., Beierle, C.: The Semantics of Asserting and Retracting Clauses to Logic Programs. LILOG Report 7, IBM Deutschland GmbH, Stuttgart 1987.

    MATH  Google Scholar 

  20. Rety, P., Kirchner, C., Kirchner, H. and Lescanne, P.: NARROWER: a new algorithm for unification and its application to Logic Programming. In: Proc. Term Rewriting Techniques and Applications, J. P. Jouannaud (ed), LNCS Vol. 202, Springer Verlag, Berlin 1985.

    Google Scholar 

  21. Siekmann, J.: Universal Unification. Proc. 7th International Conference on Automated Deduction, R. E. Shostak (ed), LNCS Vol. 170, Springer Verlag, Berlin 1984.

    Google Scholar 

  22. Broy, M. and Wirsing, M.: Abstract Data types as Lattices of Finitely Generated Models. Proc. 9th MFCS, Lecture Notes in Computer Science, Vol. 88, Springer Verlag, Berlin 1980.

    MATH  Google Scholar 

  23. Yamaoto, A.: A Theoretical Combination of SLD-Resolution and Narrowing. Proc. 4th Int. Conf. on Logic Programming, May 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IBM Deutschland GmbH Science and Technology - LILOG, P.O. Box 80 08 80, 7000, Stuttgart 80, W. Germany

    Christoph Beierle & Udo Pletat

Authors
  1. Christoph Beierle
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Udo Pletat
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. Grabowski P. Lescanne W. Wechler

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Akademie-Verlag Berlin

About this paper

Cite this paper

Beierle, C., Pletat, U. (1988). Integrating logic programming and equational specification of abstract data types. In: Grabowski, J., Lescanne, P., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1988. Lecture Notes in Computer Science, vol 343. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50667-5_59

Download citation

  • DOI: https://doi.org/10.1007/3-540-50667-5_59

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation