Replacing unification by constraint satisfaction to improve logic program expressiveness

Unification, the heart of resolution, was formulated to work in the Herbrand universe and hence does not incorporate any function evaluation. Matching is completely syntactic. In this paper, we study the replacement of unification by a constraints solver in automatic theorem proving systems using Prolog as our example. The generalization of unification into a constraint satisfaction algorithm allows the (limited) incorporation of function evaluation into unification. Constraints are also allowed as literals in the clause. We discuss the enhanced expressive power that results from incorporating an efficient constrained unifier into an automatic theorem proving system. An interpreter for the extended Prolog system (written in Prolog) incorporating a constraint solver is presented along with examples illustrating its capabilities.