Autowrite: A tool for checking properties of term rewriting systems 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.
Keywords for this software
References in zbMATH (referenced in 8 articles , 2 standard articles )
Showing results 1 to 8 of 8.
- Langer, Alexander; Reidl, Felix; Rossmanith, Peter; Sikdar, Somnath: Practical algorithms for MSO model-checking on tree-decomposable graphs (2014)
- Courcelle, Bruno; Durand, Irène: Automata for the verification of monadic second-order graph properties (2012)
- Courcelle, Bruno; Engelfriet, Joost: Graph structure and monadic second-order logic. A language-theoretic approach (2012)
- Courcelle, Bruno; Durand, Irène A.: Fly-automata, their properties and applications (2011)
- Courcelle, Bruno: Special tree-width and the verification of monadic second-order graph properties (2010)
- Durand, Irène: \textttAutowrite: a tool for term rewrite systems and tree automata (2005)
- Durand, Iréne; Middeldorp, Aart: Decidable call-by-need computations in term rewriting (2005)
- Durand, Irène: Autowrite: A tool for checking properties of term rewriting systems (2002)