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$ ofground 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.
Is the validity of some instance of an equational problem decidable?
computability;logic;decision problem;equality
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].ReferencesJean 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)