The inhabitation problem for intersection types

In the system lambda ^ of intersection types, without w, the problem as to whether an arbitrary type has an inhabitant, has been shown to be undecidable by Urzyczyn in [9]. For one subsystem of lambda ^, that lacks the ^- introduction rule, the inhabitation problem has been shown to be decidable in Kurata and Takahashi [9]. The natural question that arises is: What other subsystems of lambda ^, have a decidable inhabitation problem? The work in [2], which classifies distinct and inhabitation-distinct subsystems of lambda ^, leads to the extension of the undecidability result to lambda ^ without the (n) rule. By new methods, this paper shows, for the remaining six (two of them trivial) distinct subsystems of lambda ^, that inhabitation is decidable. For the latter subsystems inhabitant finding algorithms are provided.