Equational Constraint Solving Via a Restricted Form of Universal Quantification

摘要

In this paper, we present a syntactic method for solving first-order equational constraints over term algebras. The presented method exploits a novel notion of quasi-solved form that we call answer. By allowing a restricted form of universal quantification, answers provide a more compact way to represent solutions than the purely existential solved forms found in the literature. Answers have been carefully designed to make satisfiability test feasible and also to allow for boolean operations, while maintaining expressiveness and user-friendliness. We present detailed algorithms for (1) satisfiability checking and for performing the boolean operations of (2) negation of one answer and (3) conjunction of n answers. Based on these three basic operations, our solver turns any equational constraint into a disjunction of answers. We have implemented a prototype that is available on the web.