Is the validity of some instance of an equational problem decidable?
-
16-10-2019 - |
Question
Is the following FOL-problem (equality is a logical symbol) effectively decidable?
Given. A finite equation system $E$ and an equation $s = t$.
Question. Is there a substitution $\sigma$, such that $\sigma(E) \models \sigma(s = t)$?
Some useful information.
Obviously one can restrict $\sigma$ to be a ground substitution.
This problem is decidable: Given a finite system $E$ of
ground equations and a ground equation $s = t$, does $E \models s = t$
hold? (c.f. [1: Corollary 4.3.6])
References
[1] Franz Baader, Tobias Nipkow: Term Rewriting and All That, © 1998 Cambridge University Press.
Solution
This problem is known as rigid E-unification. This problem is NP-complete. The first proof was given by Gallier, Narendran, Plaisted and Snyder [1].
However a related problem, the Simultaneous rigid E-unification that is to find a substitution that simultaneously satisfies several instances of rigid E-unification is undecidable. This result was proved by Degtyarev and Voronkov [2].
References
Jean H. Gallier, Paliath Narendran, David A. Plaisted, Wayne Snyder: Rigid E-Unification: NP-Completeness and Applications to Equational Matings Inf. Comput. 87(1/2): 129-195 (1990)
Anatoli Degtyarev, Andrei Voronkov: The Undecidability of Simultaneous Rigid E-Unification. Theor. Comput. Sci. 166(1&2): 291-300 (1996)