A polymorphic type system in logic programming

This paper is concerned with the design of type systems for logic programming so as to satisfy the requirements of modern logic programming. The design of type systems is based on the language Godel which has a strongly type system based on many-sorted logic with parametric polymorphism. The definitions of the basic logic programming concepts of terms, atoms, programs are given in the setting of polymorphic many-sorted logic. In particular, an unification algorithm for typed predicates is proposed for the compiler construction of Godel.