Abstract
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.
This research was supported by the Deutsche Forschungsgemeinschaft, SFB 314, Project D4
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Avenhaus, J., Loría-Sáenz, C.: Canonical conditional rewrite systems containing extra variables, SEKI-Report SR-93-03, Univ. Kaiserslautern (1993).
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.
Bertling, H., Ganzinger, H.: Completion-time optimization of rewrite-time goal solving, 3rd RTA (1989), LNCS 355, pp. 45–58.
Comon, H.: Solving inequations in term algebras, 5th IEEE Symposium on Logic in Computer Science, LICS (1990), pp. 62–69.
Dershowitz, N.: Termination, 1st RTA (1985), LNCS 202, pp. 180–224 and J. Symbolic Comp. 3 (1987), pp. 69–116.
Dershowitz, N.: Ordering-based strategies for Horn-clauses, 12th IJCAI (1991), pp. 118–124.
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.
Dershowitz, N., Okada, M.: A rationale for conditional equational programming, TCS 75 (1990), pp. 111–138.
Dershowitz, N., Okada, M., Sivakumar, G.: Confluence of conditional rewrite systems, 1st CTRS (1988), LNCS 308, pp. 31–44.
Ganzinger, H.: Order-sorted completion: the many-sorted way, TCS 89 (1991), pp. 3–32.
Geser, A.: On a monotonic semantic path ordering, Ulmer Informatik-Berichte No. 92-13, Universität Ulm (1992).
Ganzinger, H., Waldmann, U.: Termination proofs of well-moded logic programs via conditional rewrite systems, 3rd CTRS (1992), LNCS 656, pp. 430–437.
Heck, N., Avenhaus, J.: On logic programs with data-driven computations, EUROCAL-85 (1985), LNCS 204, pp. 433–443.
Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems, J. ACM 27 (1980), pp. 797–821.
Kaplan, S.: Simplifying conditional term rewriting systems: Unification, termination and confluence, JSC (1987), pp. 295–334.
Loría-Sáenz, C.: A theoretical framework for reasoning about program construction based on extensions of rewrite systems, Dissetation, Univ. Kaiserslautern, 1993.
Steinbach, J.: Private communication.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Avenhaus, J., Loría-Sáenz, C. (1994). On conditional rewrite systems with extra variables and deterministic logic programs. In: Pfenning, F. (eds) Logic Programming and Automated Reasoning. LPAR 1994. Lecture Notes in Computer Science, vol 822. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58216-9_40
Download citation
DOI: https://doi.org/10.1007/3-540-58216-9_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58216-8
Online ISBN: 978-3-540-48573-5
eBook Packages: Springer Book Archive