Hierarchical Constraint Satisfaction as a Model for Adding Types with Inheritance to Prolog

Prolog is a language based on first order logic. It uses resolution as a rule of inference, and unification is the heart of resolution. Prolog operates on the Herbrand universe, a single, unstructured domain. In problems with large structured domains, the number of resolution steps may become large. We have incorporated type inheritance into Prolog to exploit large structured domains to write more concise code and to obtain shorter proofs. Types are subuniverses corresponding to sets of objects. The subset of relation between types induces a hierarchy on the universe. We used the hierarchical constraint satisfaction concept to incorporate these extensions into Prolog. We also provide a formal proof that our typed unification extends standard Prolog and directly augments the Warren Abstract Machine (WAM) concept.