On the Construction of Unifying Terms Modulo a Set of Substitutions
S Langet · 1991
Abstract The aim of this paper is to provide a mathematical problem which is of interest for getting practicable methods in the field of inductive program synthesis. The problem we have in mind is obviously a dualism to the unification problem in some equational theory. We consider two terms t 1, t2 and two possibly different substitutions b 1, b2 for each of them. The problem is to find a unique term t for both terms such that t and t I as well as t and t2are unifiable with respect to the underlying equational theory by using b1 or b2as a unifier. The problem is trivially decidable in free-term algebra. It is undecidable in the general case. Moreover, even if the underlying equational theory is decidable, then the problem we have in mind may be undecidable, too. Finally, we derive sufficient pre conditions for proving its decidability.