zbMATH — the first resource for mathematics

Logicality of conditional rewrite systems. (English) Zbl 0938.68050
Summary: A conditional term rewriting system is called logical if it has the same logical strength as the underlying conditional equational system. In this paper we summarize known logicality results and we present new sufficient conditions for logicality of the important class of oriented conditional term rewriting systems.

68Q42 Grammars and rewriting systems
Full Text: DOI
[1] J. Avenhaus, C. Lorı́a-Sáenz, Canonical conditional rewrite systems containing extra variables, SEKI-Report SR-93-03, Universität Kaiserslautern, 1993.
[2] J. Avenhaus, C. Lorı́a-Sáenz, On conditional rewrite systems with extra variables and deterministic logic programs, Proc. 5th Internat. Conf. on Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 822, Springer, Berlin, 1994, pp. 215-229.
[3] Bergstra, J.A.; Klop, J.W., Conditional rewrite rules: confluence and termination, J. comput. system sci., 32, 323-362, (1986) · Zbl 0658.68031
[4] H. Bertling, H. Ganzinger, Completion-time optimization of rewrite-time goal solving, Proc. 3rd Internat. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 355, Springer, Berlin, 1989, pp. 45-58.
[5] Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, (), 243-320 · Zbl 0900.68283
[6] N. Dershowitz, J.-P. Jouannaud, J.W. Klop, Open problems in rewriting, Proc. 4th Internat. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 488, Springer, Berlin, 1991, pp. 445-456.
[7] Dershowitz, N.; Okada, M., A rationale for conditional equational programming, Theoret. comput. sci., 75, 111-138, (1990) · Zbl 0702.68034
[8] N. Dershowitz, M. Okada, G. Sivakumar, Canonical conditional rewrite systems, in: Proc. 9th Conf. on Automated Deduction, Lecture Notes in Computer Science, vol. 310, Springer, Berlin, 1988, pp. 538-549. · Zbl 0667.68043
[9] H. Ganzinger, U. Waldmann, Termination proofs of well-moded logic programs via conditional rewrite systems, Proc. 3rd Internat. Workshop on Conditional Term Rewriting Systems, Lecture Notes in Computer Science, vol. 656, Springer, Berlin, 1992, pp. 430-437.
[10] E. Giovannetti, C. Moiso, A completeness result for \(E\)-unification algorithms based on conditional narrowing, Proc. Workshop on Foundations of Logic and Functional Programming, Lecture Notes in Computer Science, vol. 306, Springer, Berlin, 1986, pp. 157-167. · Zbl 0645.68043
[11] Hamana, M., Equivalence of the quotient term model and the least complete Herbrand model for a functional logic language, J. funct. logic programm., 1, 1-22, (1997) · Zbl 0924.68048
[12] M. Hanus, On extra variables in (Equational) logic programming, in: Proc. 12th Internat. Conf. on Logic Programming, MIT Press, Cambridge, 1995, pp. 665-679.
[13] Kaplan, S., Conditional rewrite rules, Theoret. comput. sci., 33, 175-193, (1984) · Zbl 0577.03013
[14] Klop, J.W., Term rewriting systems, (), 1-116
[15] Middeldorp, A.; Hamoen, E., Completeness results for basic narrowing, Appl. algebra eng. comm. comput., 5, 213-253, (1994) · Zbl 0810.68088
[16] Meinke, K.; Tucker, J.V., Universal algebra, (), 189-411
[17] Selman, A., Completeness of calculii for axiomatically defined classes of algebras, Algebra univ., 2, 20-32, (1972) · Zbl 0251.08005
[18] T. Suzuki, Studies on conditional narrowing for rewrite systems with extra variables, Ph.D. Thesis, University of Tokyo, 1998.
[19] T. Suzuki, A. Middeldorp, T. Ida, Level-confluence of conditional rewrite systems with extra variables in right-hand sides, Proc. 6th Internat. Conf. on Rewriting Techniques and Applications, Lecture Notes in Computer Science, vol. 914, Springer, Berlin, 1995, pp. 179-193. · Zbl 0939.68679
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.