×

Ground term rewriting rules for the word problem of ground term equations. (English) Zbl 0757.68069

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\).

MSC:

68Q42 Grammars and rewriting systems
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite