Completion-time optimization of rewrite-time goal solving

  • Hubert Bertling
  • Harald Ganzinger
Regular Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 355)


Completion can be seen as a process that transforms proofs in an initially given equational theory to rewrite proofs in final rewrite rules. Rewrite proofs are the normal forms of proofs under these proof transformations. The purpose of this paper is to provide a framework in which one may further restrict the normal forms of proofs which completion is required to construct, thereby further decreasing the complexity of reduction and goal solving in completed systems.


Normal Form Logic Program Equational Theory Application Restriction Critical Pair 
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.

5 References

  1. [Bac87]
    Bachmair, L.: Proof methods for equational theories. PhD-Thesis, U. of Illinois, Urbana Champaign, 1987.Google Scholar
  2. [BDH86]
    Bachmair, L., Dershowitz, N. and Hsiang, J.: Proof orderings for equational proofs. Proc. LICS 86, 346–357.Google Scholar
  3. [BG89]
    Bertling, H. and Ganzinger, H.: Completion of Application-Restricted Equations. Report 289, FB Informatik, U. Dortmund, 1989.Google Scholar
  4. [BGM87]
    Bosco, P.G., Giovannetti, E. and Moiso, C.: Refined Strategies for Semantic Unification. TAP-SOFT 87, Springer LNCS 250, 276–290, 1987.Google Scholar
  5. [BGS88]
    Bertling, H., Ganzinger, H. and Schäfers, R.: CEC: A system for conditional equational completion. User Manual Version 1.4, PROSPECTRA-Report M.1.3-R-7.0, U. Dortmund, 1988.Google Scholar
  6. [BK82]
    Bergstra, J. and Klop, J.W.: Conditional Rewrite Rules: Confluence and Termination. Report IW198/82, Mathematisch Centrum, Amsterdam, 1982.Google Scholar
  7. [DOS88]
    Dershowitz, N., Okada, M. and Sivakumar, G.: Confluence of conditional rewrite systems. Proc. 1st Int'l Workshop on Conditional Term Rewriting, Orsay, 1987, Springer LNCS 308, 1988, 31–44.Google Scholar
  8. [DP85]
    Dershowitz, N. and Plaisted, D.A.: Logic Programming cum Applicative Programming. Proc. IEEE Symp. on Logic Programming, Boston 1985, 54–67, 1985.Google Scholar
  9. [DS88]
    Dershowitz, N. and Sivakumar, G.: Solving Goals in Equational Languages. Proc. 1st Int'l Workshop on Conditional Term Rewriting, Orsay, 1987, Springer LNCS 308, 1988, 45–55.Google Scholar
  10. [Fri85]
    Fribourg, L.: SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition. Proc. IEEE Symp. on Logic Programming, Boston 1985, 172–184, 1985.Google Scholar
  11. [Gan87]
    Ganzinger, H.: A Completion procedure for conditional equations. Report 234, U. Dortmund, 1987, also in: Proc. 1st Int'l Workshop on Conditional Term Rewriting, Orsay, 1987, Springer LNCS 308, 1988, 62–83 (revised version to appear in J. Symb. Computation).Google Scholar
  12. [Gan88a]
    Ganzinger, H.: Completion with History-Dependent Complexities for Generated Equations. In Sannella, Tarlecki (eds.): Recent Trends in Data Type Specifications. Springer LNCS 332, 1988, 73–91.Google Scholar
  13. [Gan88b]
    Ganzinger, H.: Order-Sorted Completion: The Many-Sorted Way. Report 274, FB Informatik, Univ. Dortmund, 1988, Extended abstract to appear in Proc. TAPSOFT(CAAP) '89, Barcelona.Google Scholar
  14. [GM88]
    Giovannetti, E. and Moiso, C.: A Completeness Result for E-Unification Algorithms Based on Narrowing. Proc. Workshop on Foundations of Logic and Functional Programming, Springer LNCS 306, 157–167, 1988.Google Scholar
  15. [GM84]
    Gouen, J.A. and Meseguer, J.: Eqlog: Equality, Types, and Generic Modules for Logic Programming. J. Logic Programming, 1,2, 179–210, 1984.Google Scholar
  16. [Höl87]
    Hölldobler, St.: From Paramodulation to Narrowing. Univ. der Bundeswehr, München, 1987.Google Scholar
  17. [Hul80]
    Hullot, J.M.: Canonical Forms and Unification. Proc. CADE 1980, 318–334, 1980.Google Scholar
  18. [Hus85]
    Hussmann, H.: Unification in Conditional-Equational Theories. Proc. EUROCAL, Springer LNCS 204, 543–553, 1985.Google Scholar
  19. [JW86]
    Jouannaud, J.P. and Waldmann, B.: Reductive conditional term rewriting systems. Proc. 3rd TC2 Working Conference on the Formal Description of Programming Concepts, Ebberup, Denmark, Aug. 1986, North-Holland.Google Scholar
  20. [Kap84]
    Kaplan, St.: Fair conditional term rewrite systems: unification, termination and confluence. Report 194, U. de Paris-Sud, Centre d'Orsay, Nov. 1984.Google Scholar
  21. [Kap87]
    Kaplan, St.: A compiler for conditional term rewriting. Proc. RTA 1987, LNCS 256, 1987, 25–41.Google Scholar
  22. [KR88]
    Kounalis, E. and Rusinowitch, M.: On word problems in Horn theories. Proc. 1st Int'l Workshop on Conditional Term Rewriting, Orsay, 1987, Springer LNCS 308, 1988, 144–160.Google Scholar
  23. [Pad88]
    Padawitz, P.: Computing in Horn Clause Theories. EATCS Monographs in Computer Science, 16, 1988.Google Scholar
  24. [RW69]
    Robinson, G.A. and Wos, L.: Paramodulation and Theorem Proving in First-Order Theories with Equality. In: Meltzer, Mitchie (Eds): Machine Intelligence 4, 1969.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • Hubert Bertling
    • 1
  • Harald Ganzinger
    • 1
  1. 1.Fachbereich InformatikUniversität DortmundDortmund. 50W. Germany

Personalised recommendations