On conditional rewrite systems with extra variables and deterministic logic programs

  • Jürgen Avenhaus
  • Carlos Loría-Sáenz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 822)


We study deterministic conditional rewrite systems, i.e. conditional rewrite systems where the extra variables are not totally free but ’input bounded’. If such a system R is quasi-reductive then → r is decidable and terminating. We develop a critical pair criterion to prove confluence if R is quasi-reductive and strongly deterministic. We apply our results to prove Horn clause programs to be uniquely terminating.


Induction Hypothesis Logic Program Predicate Symbol Critical Pair Output Position 
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. [AL93]
    Avenhaus, J., Loría-Sáenz, C.: Canonical conditional rewrite systems containing extra variables, SEKI-Report SR-93-03, Univ. Kaiserslautern (1993).Google Scholar
  2. [AM90]
    Avenhaus, J., Madlener, K.: Term rewriting and equational reasoning, in: R.B. Banerji, ed., Formal Techniques in Artifical Intelligence, North Holland, Amsterdam (1990), pp. 1–43.Google Scholar
  3. [BG89]
    Bertling, H., Ganzinger, H.: Completion-time optimization of rewrite-time goal solving, 3rd RTA (1989), LNCS 355, pp. 45–58.Google Scholar
  4. [CO90]
    Comon, H.: Solving inequations in term algebras, 5th IEEE Symposium on Logic in Computer Science, LICS (1990), pp. 62–69.Google Scholar
  5. [De87]
    Dershowitz, N.: Termination, 1st RTA (1985), LNCS 202, pp. 180–224 and J. Symbolic Comp. 3 (1987), pp. 69–116.Google Scholar
  6. [De91]
    Dershowitz, N.: Ordering-based strategies for Horn-clauses, 12th IJCAI (1991), pp. 118–124.Google Scholar
  7. [DJ90]
    Dershowitz, N., Jouannaud, J.P.: Rewriting systems, in J. van Leeuwen, ed., Handbook of Theoretical Computer Science, Vol. B, Elsevier, Amsterdam (1990), pp. 241–320.Google Scholar
  8. [DO90]
    Dershowitz, N., Okada, M.: A rationale for conditional equational programming, TCS 75 (1990), pp. 111–138.Google Scholar
  9. [DOS88]
    Dershowitz, N., Okada, M., Sivakumar, G.: Confluence of conditional rewrite systems, 1st CTRS (1988), LNCS 308, pp. 31–44.Google Scholar
  10. [Ga91]
    Ganzinger, H.: Order-sorted completion: the many-sorted way, TCS 89 (1991), pp. 3–32.Google Scholar
  11. [Ge92]
    Geser, A.: On a monotonic semantic path ordering, Ulmer Informatik-Berichte No. 92-13, Universität Ulm (1992).Google Scholar
  12. [GW92]
    Ganzinger, H., Waldmann, U.: Termination proofs of well-moded logic programs via conditional rewrite systems, 3rd CTRS (1992), LNCS 656, pp. 430–437.Google Scholar
  13. [HA85]
    Heck, N., Avenhaus, J.: On logic programs with data-driven computations, EUROCAL-85 (1985), LNCS 204, pp. 433–443.Google Scholar
  14. [Hu80]
    Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems, J. ACM 27 (1980), pp. 797–821.Google Scholar
  15. [Ka87]
    Kaplan, S.: Simplifying conditional term rewriting systems: Unification, termination and confluence, JSC (1987), pp. 295–334.Google Scholar
  16. [LS93]
    Loría-Sáenz, C.: A theoretical framework for reasoning about program construction based on extensions of rewrite systems, Dissetation, Univ. Kaiserslautern, 1993.Google Scholar
  17. [St93]
    Steinbach, J.: Private communication.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Jürgen Avenhaus
    • 1
  • Carlos Loría-Sáenz
    • 1
  1. 1.Fachbereich InformatikUniversität KaiserslauternKaiserslauternGermany

Personalised recommendations