Solving disequations modulo some class of rewrite systems
The authors discuss the problem of solving disequations, i.e. formulas of the form \(s \not= t\) modulo a theory that is given by a set of equations \(E\). They show that the problem is decidable, provided the equations in \(E\) can be organised as a rewrite system that is both confluent and constructor based and furthermore satisfies the following restrictions: 1. The rewrite rules have to be linear. 2. If a subterm \(r\) of the right hand side of a rewrite rule unifies with the left hand side \(l\) of a rewrite rule, the most general unifier \(\mu\) of \(l\) and \(r\) must be a renaming of the variables occurring in \(l\). 3. There may be no nested occurrences of defined function symbols on the right hand side of a rewrite rule. 4. The disequations to be solved have to be linear. The present paper is a continuation of the paper ``E-unification by means of tree tuple synchronized grammars [Discrete Math. Theor. Comput. Sci. 1, 69-98 (1997)], which is written by the same authors. In that paper it is shown that the problem of solving an equation modulo a rewrite system is decidable, provided the above conditions are satisfied. Furthermore, it is shown there that the problem gets undecidable if any one of the above conditions is dropped. Unfortunately, the authors do not discuss the above conditions and they do not give any examples of ``natural term rewrite systems satisfying these conditions. The authors achieve their result by encoding term rewrite systems by means of tree tuple synchronised grammars (TTSG's). This development is technically quite involved, hence difficult to follow. For the entire collection see [Zbl 0888.00017].
This page was built for publication: Solving disequations modulo some class of rewrite systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3838765)
