Projective Quantifier Elimination for Equational Constraint Solving

ABSTRACT. We deal with (general) equational constraints, that is, first-order formulas, with equality as its only predicate symbol, over a (finite or infinite) language $\Language$ of function symbols. As semantic domain, we consider the algebra of finite terms over L. Solving one of such constraints means to find all the solutions for (i.e. assignments to) its free variables. We present the Projective Quantifier Elimination (PQE) technique for solving equational constraints (in particular, deciding their satisfiability) that performs an algebraic-style transformation of expressions instead of handling first-order formulas. PQE is formulated on the basis of three algebraic operations on expressions: complement, intersection and projection. We aim to contribute not only a new style of quantifier elimination for constraint solving, but also a more efficient method for equational constraint solving. PQE avoids unnecessary applications of the costly Explosion Rule (ER) that are performed by traditional solving methods.