Fülöp, Zoltán; Vágvölgyi, Sándor Ground term rewriting rules for the word problem of ground term equations. (English) Zbl 0757.68069 Bull. EATCS 45, 186-201 (1991). Summary: A simple and efficient algorithm is described which, given a finite set \(E\) of ground terms equations over a ranked alphabet \(\Sigma\), produces a reduced ground term rewriting system \(R\) over a ranked alphabet containing \(\Sigma\) with the property that \({* \atop{\leftrightarrow \atop E}}={* \atop{\leftrightarrow \atop R}}\cap T_ \Sigma\times T_ \Sigma\). Since \(R\) is canonical as well, two terms over \(\Sigma\) are congruent modulo \({* \atop{\leftrightarrow \atop E}}\) if and only if their \(R\)-normal forms coincide. The algorithm we give calls a congruence closure procedure over the subterm graph of \(E\) and runs in \(O(n\log n)\) time, where \(n\) is the size of \(E\). Cited in 8 Documents MSC: 68Q42 Grammars and rewriting systems 68Q05 Models of computation (Turing machines, etc.) (MSC2010) 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:Church-Rosser property; confluence; theory of equality; word problem; ground term rewriting system; congruence closure PDFBibTeX XMLCite \textit{Z. Fülöp} and \textit{S. Vágvölgyi}, Bull. EATCS 45, 186--201 (1991; Zbl 0757.68069)