Durand, Irène Autowrite: A tool for checking properties of term rewriting systems. (English) Zbl 1045.68579 Tison, Sophie (ed.), Rewriting techniques and applications. 13th international conference, RTA 2002, Copenhagen, Denmark, July 22–24, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43916-1). Lect. Notes Comput. Sci. 2378, 371-375 (2002). Summary: Huet and Lévy have shown that for the class of orthogonal term rewriting systems (TRSs) every term not in normal form contains a needed redex (i.e., a redex contracted in every normalizing rewrite sequence) and that repeated contraction of needed redexes results in a normal form if it exists. However, neededness is in general undecidable. In order to obtain a decidable approximation to neededness Huet and Lévy introduced the subclass of strongly sequential TRSs and showed that strong sequentiality is a decidable property of orthogonal TRSs.For the entire collection see [Zbl 0992.00043]. Cited in 2 Documents MSC: 68Q42 Grammars and rewriting systems Software:Autowrite PDFBibTeX XMLCite \textit{I. Durand}, Lect. Notes Comput. Sci. 2378, 371--375 (2002; Zbl 1045.68579) Full Text: Link