Abstract
We present a general translation of term rewrite systems (TRS) to logic programs such that basic rewriting derivations become logic deductions. Certain TRS result in so-called cs-programs, which were originally studied in the context of constraint systems and tree tuple languages. By applying decidability and computability results of cs-programs we obtain new classes of TRS that have nice properties like decidability of unification, regular sets of descendants or finite representations of R-unifiers. Our findings generalize former results in the field of term rewriting.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Comon, H., Dauchet, M., Gilleron, R., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (TATA)(1997), http://www.grappa.univ-lille3.fr/tata
Gyenizse, P., Vágvölgyi, S.: Linear generalized semi-monadic rewrite systems effectively preserve recognizability. Theoretical Computer Science 194, 87–122 (1998)
Limet, S., Réty, P.: E-unification by means of tree tuple synchronized grammars. Discrete Mathematics and Theoretical Computer Science 1, 69–98 (1997)
Limet, S., Salzer, G.: Manipulating tree tuple languages by transforming logic programs. In: Dahn, I., Vigneron, L. (eds.) Electronic Notes in Theoretical Computer Science, vol. 86, Elsevier, Amsterdam (2003)
Limet, S., Salzer, G.: Proving properties of term rewrite systems via logic programs. Technical report, RR-2004-5, LIFO Université d’Orléans (2004), www.univorleans.fr/SCIENCES/LIFO/prodsci/publications/lifo2004.htm.en
Lloyd, J.W.: Foundations of Logic Programming. Springer, Heidelberg (1984)
Lugiez, D., Schnoebelen, P.: The regular viewpoint on pa-processes. Theoretical Computer Science 274(1-2), 89–115 (2002)
Proietti, M., Pettorossi, A.: Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theoretical Computer Science 142(1), 89–124 (1995)
Réty, P.: Regular sets of descendants for constructor-based rewrite systems. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705, Springer, Heidelberg (1999)
Seki, H., Takai, T., Fujinaka, Y., Kaji, Y.: Layered transducing term rewriting system and its recognizability preserving property. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, p. 98. Springer, Heidelberg (2002)
Takai, T., Kaji, Y., Seki, H.: Right-linear finite path overlapping term rewriting systems effectively preserve recognizability. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 270–273. Springer, Heidelberg (2000)
Tamaki, H., Sato, T.: Unfold/fold transformation of logic programs. In: Tärnlund, S. (ed.) Proc. 2nd Int. Logic Programming Conf (ICLP), University of Uppsala, Sweden, pp. 127–138 (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Limet, S., Salzer, G. (2004). Proving Properties of Term Rewrite Systems via Logic Programs. In: van Oostrom, V. (eds) Rewriting Techniques and Applications. RTA 2004. Lecture Notes in Computer Science, vol 3091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25979-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-25979-4_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22153-1
Online ISBN: 978-3-540-25979-4
eBook Packages: Springer Book Archive