On completeness of narrowing strategies

  • Rachid Echahed
Part of the Lecture Notes in Computer Science book series (LNCS, volume 299)


In this paper we propose some syntactical criteria on algebraic specifications that ensure completeness of narrowing strategies. We then prove a theorem relating narrowing and reduction relations. The completeness of narrowing strategies is proved and conditions for the computation of a "minimal" ground complete set of E-unifiers are given; as well as an algorithm transforming specifications satisfying Huet and Hullot's principle of definition, into specifications fulfilling the proposed criteria.


Normal Form Logic Programming Equational Theory Horn Clause Functional Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    K.R. Apt, M.H. Van Emden: Contributions to the Theory of Logic Programming. JACM, Vol. 29, no 3, July 1982, 841–862.Google Scholar
  2. [2]
    M. Bellia, G. Levi: The Relation between Logic and Functional Languages: Asurvey. J. Logic Programming, 217–236, 1986.Google Scholar
  3. [3]
    D. Bert, R. Echahed: Design and Implementation of a Generic, Logic and Functional Programming Language. Proc. of ESOP'86, LNCS no 213, Saarebrücken, March 1986 119–132.Google Scholar
  4. [4]
    P.G. Bosco, E. Giovannetti, C. Moiso: Refined Strategies for semantic unification. Proc. of TAPSOFT '87, LNCS no 250, Pisa, March 1987, 276–290.Google Scholar
  5. [5]
    N. Deshowitz, D.A. Plaisted: Logic Programming cum Applicative Programming. Proc. of SLP'85, July 1985, 54–66.Google Scholar
  6. [6]
    M.J. Fay: First Order Unification in an Equational Theory. Proc. of the 4th workshop on automated Deduction, Austin, Texas, February 1979, 161–167.Google Scholar
  7. [7]
    L. Fribourg: SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting. Proc. of SLP '85, Boston, July 1985, 172–184.Google Scholar
  8. [8]
    A. Geser, H. Hussmann: Experiences with the RAP system-a Specification interpreter combining term rewriting and resolution. Proc. of ESOP'86, LNCS no 213, Saarebrücken, March 1986, 339–350.Google Scholar
  9. [9]
    J.A. Goguen, J. Meseguer: Equality, Types, Modules and (why not?) generics for logic programming. J. Logic Programming, vol.1, 1984, 179–210.Google Scholar
  10. [10]
    H. Hussmann: Unification in Conditional Equational Theories. Proc. of EUROCAL'85, LNCS, no204, 1985,543–553.Google Scholar
  11. [11]
    G. Huet, J-M. Hullot: Proofs by Induction in Equational Theories with constructors. Proc. of 21st Annual Symposium on Foundationn of Computer Science, 1980, 96–107.Google Scholar
  12. [12]
    G. Huet, D.C. Oppen: Equations and Rewrite rules: a Survey. In "Formal Languages: Perspectives and Open problems". Ed. R.Book, Academic press, 1980.Google Scholar
  13. [13]
    J-M. Hullot: Canonical Forms and Unification. Proc.of 5th CADE, LNCS no 87, 1980, 318–334.Google Scholar
  14. [14]
    A. Josephson, N. Dershowitz: An Implementation of Narrowing: The RITE Way. Proc. of SLP'86, IEEE press, Salt lake city, Utah, 1986, 187–197.Google Scholar
  15. [15]
    J-P. Jouannaud, E. Kounalis: Automatic Proofs by Induction in Equational Theories without Constructors. Proc. of 1st IEEE Symposium on Logic in Computer Science, 1986.Google Scholar
  16. [16]
    S. Kaplan: Conditional Rewrite Rules. TCS, 33, 1984, 175–193.Google Scholar
  17. [17]
    J. Meseguer, J.A. Goguen: Initiality, Induction and Computability. In Algebraic Methods in Semantics, M.Nivat and J.C.Reynolds, Eds, Cambridge University Press, 1985, 459–541.Google Scholar
  18. [18]
    N.J. Nilsson: Principles of Artificial Intelligence. Springer-Verlag, 1980.Google Scholar
  19. [19]
    P. Padawitz: Strategy-Controlled Reduction and Narrowing. Proc. RTA'87, LNCS no 256, Bordeaux, May 1987, 242–255.Google Scholar
  20. [20]
    U.S. Reddy: Narrowing as the Operational Semantics of Functional Languages. In: Logic Programming: Relations, Functions, and Equations, D.DeGroot and G.Lindstrom, eds. Prentice Hall, Englewood Cliffs, NJ, 1985.Google Scholar
  21. [21]
    P. Réty: Improving Basic Narrowing Techniques. Proc. RTA'87, LNCS, no 256, Bordeaux, May 1987, 228–241.Google Scholar
  22. [22]
    J.R. Slagle: Automated Theorem Proving for Theories with Simplifiers, Commutativity, and Associativity. JACM, Vol. 21, no 4, October 1974, 622–642.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Rachid Echahed
    • 1
  1. 1.LIFIA(IMAG) Institut National Polytechnique de GrenobleGrenobleFrance

Personalised recommendations