Skip to main content
SpringerLink
Log in

Handling function definitions through innermost superposition and rewriting

  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1985)

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

Included in the following conference series:

Abstract

This paper presents the operating principles of SLOG, a logic interpreter of equational clauses (Horn clauses where the only predicate is ‘=’). SLOG is based on an oriented form of paramodulation called superposition. Superposition is a complete inference rule for first-order logic with equality. SLOG uses only a strong restriction of superposition (innermost superposition) which is still complete for a large class of programs. Besides superposition, SLOG uses rewriting which provides eager evaluation and handling of negative knowledge. Rewriting combined with superposition improves terminability and control of equational logic programs.

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. Abramson, H., "A Prological Definition of HASL, a Purely Functional Language with Unification Based Conditional Binding Expressions" New Generation Computing 2:1, pp. 3–35, 1984.

    Google Scholar 

  2. Aida, H., Tanaka, H. & Moto-oka, T., "A Prolog Extension for Handling Negative Knowledge", New Generation Computing 1:1, pp. 87–91, 1983.

    Google Scholar 

  3. Bergstra, J & Klop, J., "Conditional Rewrite Rules: Confluency and Termination" Research Report IW 198/82, Mathematical Centre, Amsterdam, 1982.

    Google Scholar 

  4. Bidoit,M. & Choquer,M.A., "Preuves de Formules Conditionnelles par Recurrence", Proc. AFCET IA, Grenoble, Nov. 1985.

    Google Scholar 

  5. Bouge, L., Choquet, N., Fribourg, L. & Gaudel, M.C.G., "Application of Prolog to Test Sets Generation from Algebraic Specifications", Coll. on Software Engineering, LNCS 186, pp.261–275, March 1985.

    Google Scholar 

  6. Choquet, N., Fribourg, L. & Mauboussin A., "Runnable Protocol Specifications using the logic interpreter SLOG", 5th IFIP Workshop on Protocol Specification, Verification and Testing, Toulouse-Moissac, June 1985.

    Google Scholar 

  7. Colmerauer,A., "Prolog and Infinite Trees", in Logic Programming, K.L. Clark and S.A. Tarnlund (Eds.), Academic Press, 1982.

    Google Scholar 

  8. Deransart, P., "An Operational Algebraic Semantics of PROLOG programs", Proc. Programmation en Logique, Perros-Guirec, CNET-Lannion, March 1983.

    Google Scholar 

  9. Dershowitz,N. & Josephson N.A., "Logic Programming by Completion" 2nd International Logic Programming Conference, Upsala, pp. 313–320, 1984.

    Google Scholar 

  10. Dershowitz, N., "Orderings for Term-Rewriting Systems", TCS 17:3, pp.279–301, 1982.

    Google Scholar 

  11. Durand,J., "LOGRE: un Prototype de Systeme de Programmation en Logique Utilisant des Techniques de Reecriture", These 3eme cycle, U. of Nancy, 1984.

    Google Scholar 

  12. Fay,M., "First-Order Unification in an Equational Theory" Proc. 4th Workshop on Automated Deduction, pp. 161–167, Feb. 1979.

    Google Scholar 

  13. Fribourg, L., "Oriented Equational Clauses as a Programming Language", J. Logic Programming 1:2, pp. 165–177, August 1984.

    Google Scholar 

  14. Fribourg, L., "A Narrowing Procedure for Theories with Constructors", 7th Intl. Conf. on Automated Deduction, LNCS 170, pp. 259–281, 1984.

    Google Scholar 

  15. Goguen, J.A. & Meseguer J., "Equality,Types,Modules and Generics for Logic Programming", J. Logic Programming 1:2, pp. 179–210, August 1984.

    Google Scholar 

  16. Huet, G., "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems", J.ACM 27:4, pp. 797–821, Oct. 1980.

    Google Scholar 

  17. Huet,G. & Hullot,J.M., "Proofs by Induction in Equational Theories with Constructors", 21st FOCS, pp. 96–107, 1980.

    Google Scholar 

  18. Hullot, J.M., "Canonical Forms and Unification" 5th Intl. Conf. on Automated Deduction, LNCS 87, pp. 318–334, 1980.

    Google Scholar 

  19. Hussmann,H., "Unification in Conditional-Equational Theories" Technical Report MIP-8502, U. Passau, January 85. Short version in: Proc. EUROCAL 85 Conf., Linz.

    Google Scholar 

  20. Kaplan, S., "Conditional Rewrite Rules", TCS 33, pp. 175–193, 1984.

    Google Scholar 

  21. Kaplan,S., "Fair Conditional Term Rewriting Systems: Unification, Termination and Confluence", Technical Report 194, U. Orsay, November 1984.

    Google Scholar 

  22. Knuth, D.E. & Bendix P.B., "Simple Word Problems in Universal Algebras", in Computational Problems in Abstract Algebra, J. Leech (Ed.), Pergamon Press, New York, pp. 263–297, 1970.

    Google Scholar 

  23. Jouannaud,J.P., Lescanne,P. & Reinig,F. "Recursive Decomposition Ordering", in IFIP Working Conf. on Formal Description of Programming Concepts II, North-Holland, D. Bjorner (Ed.), 1983.

    Google Scholar 

  24. Lankford,D.S., "Canonical Inference", Technical Report ATP-32, Dept of Mathematics, U. of Texas, 1975.

    Google Scholar 

  25. Malachi,Y., Manna,Z. & Waldinger,R.J., "TABLOG: the Deductive Tableau Programming Language", ACM Lisp and Functional Programming Conf., pp. 323–330, 1984.

    Google Scholar 

  26. Naish,L., "automating Control for Logic Programs" Technical Report 83/6, Dept of Computer Science, U. Melbourne, 1984.

    Google Scholar 

  27. Paul,E., "On Solving the Equality Problem in Theories Defined by Horn Clauses" EUROCAL Conf., Linz, 1985 (to appear in LNCS).

    Google Scholar 

  28. Pletat, U., Engels, G., Ehrich, H.D., "Operational Semantics of Algebraic Specifications with Conditional Equations", Proc. 7th CAAP Conf., Lille, France, 1982.

    Google Scholar 

  29. Pereira, F.C.N., Warren, H.D., "Definite Clause Grammars for Language Analysis a Survey of the Formalism and a Comparison with Augmented Transition Networks", Artificial Intelligence 13, pp. 231–278, 1980.

    Google Scholar 

  30. Pereira,L.M., "Logic Control with Logic", 1st Intl. Logic Programming Conf., pp. 9–18, Marseille, 1982.

    Google Scholar 

  31. Reiter, R., "On Closed World Data Bases", in Logic and Databases, H. Gallaire and J. Minker (Eds.), Plenum Press, New York, pp. 55–76, 1980.

    Google Scholar 

  32. Remy, J.L., "Etude des Systemes de Reecriture Conditionnels et Application aux Types Abstraits Algebriques" Doctoral Thesis, J.N.P.L., Nancy, France, 1982.

    Google Scholar 

  33. Remy,J.L., Zang,H., "REVEUR4: A System to Proceed Experiments on Conditional Term Rewriting Systems", Proc. of 2th ECAI Conf., Pisa, 1984.

    Google Scholar 

  34. Slagle, J.R., "Automated Theorem Proving for Theories with Simplifiers, Commutativity and Associativity", J.ACM 21:4, pp. 622–642, Oct. 1974.

    Google Scholar 

  35. Tamaki,H., "Semantics of a Logic Programming Language with a Reducibility Predicate", IEEE Intl. Symp. on Logic Programming, Atlantic City, pp. 259–264, Feb. 1984.

    Google Scholar 

  36. You,J.H., "On the Completeness of First-Order Unification in Equational Theories", unpublished manuscript, 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. L.I.T.P., 2, Place Jussieu, 75005, Paris, France

    Laurent Fribourg

Authors
  1. Laurent Fribourg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jean-Pierre Jouannaud

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fribourg, L. (1985). Handling function definitions through innermost superposition and rewriting. In: Jouannaud, JP. (eds) Rewriting Techniques and Applications. RTA 1985. Lecture Notes in Computer Science, vol 202. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15976-2_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-15976-2_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-39679-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation