ABSTRACT

A unification problem arises when one wants to find out whether there is a substitution that makes an expression (usually an equality between the first order terms) true. An E-unification problem occurs if one wants to find out whether there is a substitution that makes a given goal true modulo an equational theory (e.g. axioms of an Abelian group). The first problem (without equational theory) is decidable and of linear complexity, whereas the second one is in general undecidable and for many particular theories even if it is decidable, it can have high complexity. We present a way to approximate any E-unification problem by transforming it into a simple form (polynomial time decidable). The transformation yields an E-unification procedure that is complete, but not sound. This means that the negative answers are correct, but in the case of a positive answer one has to check it with another method. Thus the approximation allows one to eliminate quickly the goals that are obviously not unifiable, without using more costly complete procedures.
 

Date: August 18, 2017  
Venue: 109, SEAS

Keywords: Research Seminar Series