Type inference in prolog and its application
Tadashi Kanamori, Kenji Horiuchi · International Joint Conference on Artificial Intelligence · 1985
In this paper we present a type inference method for Prolog programs. The new idea is to describe a superset of the success set by associating a type substitution (an assignment of sets of ground terms to variables) with each head of definite clause. This approach not only conforms to the style of definition inherent to Prolog but also gives some accuracy to the types infered. We show the basic computation method of the superset by sequential approximation as well as an incremental method to utilize already obtained results. We also show its application to verification of Prolog programs.