An efficient constraint language for polymorphic order-sorted resolution

Abstract

In recent years various sorted logics have been developed, mostly to facilitate knowledge representation and to speed up automated deduction. We present a polymorphic order-sorted logic that can be implemented efficiently. Because the polymorphism is almost unrestricted, it is possible for two terms to have an exponential number of maximally general unifiers. To guarantee a single most general unifier, we embed the sorted logic into a more general constraint logic and create a distinct constraint satisfaction search space. This separates the total search space into two orthogonal ones and facilitates many optimizations. The main complexity gains are that the unnecessary generation of unifiers can be avoided and that the primary resolution search space remains constant if the complexity of the unification grows.

Research carried out at the University of Illinois at Urbana-Champaign, USA.